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.