(*** 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.