(*** Introductory illustration ***)
(* The difference between definitional equality (syntactic conversion)
and propositional equality (=). *)
Require Import Nat.
(* Define addition two ways, by recursion on either the first
or the second argument. *)
Fixpoint add' (m n : nat) :=
match m with
| 0 => n
| S k => S (add' k n)
end.
Fixpoint add'' (m n : nat) :=
match n with
| 0 => m
| S k => S (add'' m k)
end.
Notation "n +' m" := (add' n m) (at level 10).
Notation "n +'' m" := (add'' n m) (at level 10).
(* Different definitions give us different behavior on equality! *)
Goal 1 +' 2 = 2 +' 1.
Proof. unfold add'. reflexivity. Qed.
Lemma Eg1 m n: m +' n = n +' m.
Proof. unfold add'. assert_fails reflexivity. Abort.
Lemma Eg2 n: 0 +' n = n +' 0.
Proof. assert_fails reflexivity. Abort.
Lemma Eg3 n: 0 +' n = n +'' 0.
Proof. unfold add'. unfold add''. reflexivity. Qed.
Lemma Eg4 m n: m +' n = n +'' m.
Proof. unfold add'. unfold add''. assert_fails reflexivity. Abort.
(*** Equivalent formulations of equality ***)
(* Define eq' as an inductive type, as in the slides: *)
Inductive eq' {A: Type}: A -> A -> Type :=
refl a : eq' a a.
Notation "a =' b" := (eq' a b) (at level 70, no associativity).
(* Compare the induction principles of eq' and Coq's built-in eq: *)
Check eq'_rect. (* Compare this to the identity elimination rule on Slide 7 *)
Check eq_rect.
(* The two formulations are equivalent. *)
Lemma eq_imp_eq' (A: Type): forall a b: A, a = b -> a =' b.
Proof.
intros.
induction H.
exact (refl a). (* easy would work too *)
Qed.
Print eq_imp_eq'.
Lemma eq'_imp_eq (A: Type): forall a b: A, a =' b -> a = b.
Proof.
intros.
induction X.
exact (eq_refl a). (* this is essentially what `reflexivity` does *)
Qed.
Print eq'_imp_eq.
(*** Symmetry of equality ***)
Lemma eq'_sym (A: Type): forall a b: A, a =' b -> b =' a.
Proof.
intros.
induction X.
exact (refl a).
Qed.
Print eq'_sym.