Module Overloading_of_notations. Record myeq := Myeq { carrier : Set ; myequality : carrier -> carrier -> bool }. About myequality. (* take as a first argument a complete instance of a record myeq *) Notation "a '===' b" := (myequality _ a b) (at level 70). Fail Check (true === false). Require Bool. Print Bool.eqb. Check (Myeq bool Bool.eqb : myeq). (* register an instance of myeq for booleans as canonical: *) Canonical Structure myeq_bool := Myeq bool Bool.eqb. (* => Coq will insert Bool.eqb automatically based on type information *) Check (true === false). Unset Printing Notations. Check (true === false). Set Printing Notations. Eval compute in (true === false). (* the same with natural numbers *) Fail Check (O === 1). Require Arith. Check EqNat.beq_nat. (* exo22: register an instance of myeq for natual numbers as canonical and check that one can still use the notation "==" *) End Overloading_of_notations. Module Eqtype_example. (* overloading of notation + equivalence with Leibniz equality *) Record myeq := Eqtype { carrier : Set ; myequality : carrier -> carrier -> bool ; Hmyequality : forall x y : carrier, myequality x y = true <-> x = y }. Notation "a '===' b" := (myequality _ a b) (at level 70). Canonical Structure eqtypenat := Eqtype _ _ EqNat.beq_nat_true_iff. Canonical Structure eqtypebool := Eqtype _ _ Bool.eqb_true_iff. Check O : nat. Check (O : carrier _). Coercion is_true : bool >-> Sortclass. From Ssreflect Require Import ssreflect. Goal forall x y : bool, x === y -> x = y. move=> x y. by move/Bool.eqb_true_iff. Undo 1. move/Hmyequality. done. Qed. Goal forall x y : nat, x === y -> x = y. move=> x y. Fail by move/Bool.eqb_true_iff. by move/EqNat.beq_nat_true_iff. Undo 1. move/Hmyequality. done. Qed. (* -> we have the same proof for booleans and natural numbers *) End Eqtype_example. Module unicity_of_identity_proofs. (* in Coq, two proofs of the same Prop facts can be considered as equal (proof-irrelevance is admissible in Coq) *) Variable H1 : O < 3. Variable H2 : O < 3. Goal H1 = H2. Fail reflexivity. Require ProofIrrelevance. now apply ProofIrrelevance.proof_irrelevance. Qed. (* in Coq, we can prove the unicity of equality proofs when the type has a decidable equality, so that proof-irrelevance does not need to be admitted; for example, in the case of booleans: *) Lemma eq_symK : forall (A : Type) (a b : A) (e : a = b), eq_sym (eq_sym e) = e. Proof. intros A a b e. destruct e. simpl. reflexivity. Qed. Lemma buip : forall (b1 b2 : bool) (p1 p2 : (b1 = b2 : Prop)), p1 = p2. Proof. intros b1 b2 p1 p2. (*destruct p1. Fail destruct p2.*) pose (fun b (e : b1 = b) => match Bool.bool_dec b1 b with | left H => H | right _ => e end) as test_against_b1. cutrewrite (p1 = test_against_b1 b2 p1). cutrewrite (p2 = test_against_b1 b2 p2). unfold test_against_b1. destruct p1. destruct b1; simpl; reflexivity. destruct p2. unfold test_against_b1. destruct b1; simpl; reflexivity. destruct p1. unfold test_against_b1. destruct b1; simpl; reflexivity. Qed. Variable lt : nat -> nat -> bool. Check (lt 0 3) : bool. Variable H1' : lt O 3 = true. Variable H2' : lt O 3 = true. Goal H1' = H2'. Fail reflexivity. apply buip. Abort. End unicity_of_identity_proofs.