(* week-05_three-properties-of-Leibniz-equality.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 13 Feb 2025 *)

(* ********** *)

Require Import Arith Bool.

(* ********** *)

Check (eq_refl 2).
(* eq_refl : 2 = 2*)

(*
Definition negb (b : bool) : bool :=
  match b with
    true =>
    false
  | false =>
    true
  end.
*)

Proposition about_negb :
  forall x : bool,
    (forall y : bool,
        x = y -> negb (negb x) = y) ->
    negb (negb (negb x)) = negb x.
Proof.
  intros x H_x.
  Check (H_x x).
  Check (H_x x (eq_refl x)).
  rewrite -> (H_x x (eq_refl x)).
  reflexivity.

  Restart.

  intros x H_x.
  Check (H_x x).
  Check (H_x x (eq_refl x)).
  Check (eq_sym (H_x x (eq_refl x))).
  rewrite <- (eq_sym (H_x x (eq_refl x))).
  reflexivity.
Qed.

(* ***** *)

Check (Nat.add_0_l 2).
(* Nat.add_0_l 2 : 0 + 2 = 2 *)

Check (eq_sym (Nat.add_0_l 2)).
(* eq_sym (Nat.add_0_l 2) : 2 = 0 + 2 *)

(* ***** *)

Definition foo (n : nat) : nat :=
  S n.

Definition bar (n : nat) : nat :=
  1 + n.

Definition baz (n : nat) : nat :=
  n + 1.

Lemma equivalence_of_foo_and_bar :
  forall n : nat,
    foo n = bar n.
Admitted.

Lemma equivalence_of_bar_and_baz :
  forall n : nat,
    bar n = baz n.
Admitted.

Corollary equivalence_of_foo_and_baz :
  forall n : nat,
    foo n = baz n.
Proof.
  intro n.
  Check (eq_trans (equivalence_of_foo_and_bar n) (equivalence_of_bar_and_baz n)).
  (* eq_trans (equivalence_of_foo_and_bar n) (equivalence_of_bar_and_baz n)
          : foo n = baz n *)
  exact (eq_trans (equivalence_of_foo_and_bar n) (equivalence_of_bar_and_baz n)).
Qed.

(* ********** *)

(* end of week-05_three-properties-of-Leibniz-equality.v *)