(* week-07_functional-equality.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 07 Mar 2025 *)

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

Require Import Arith.

Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.

Definition fold_unfold_add_O := Nat.add_0_l.
Definition fold_unfold_add_S := plus_Sn_m.

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

Check f_equal. (* : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y *)

Check Nat.add_0_r. (* : forall n : nat, n + 0 = n *)

Proposition add_0_r :
  forall n : nat,
    n + 0 = n.
Proof.
  intro n.
  induction n as [ | n' IHn'].
  - exact (fold_unfold_add_O 0).
  - rewrite -> (fold_unfold_add_S n' 0).
    (*
      n' : nat
      IHn' : n' + 0 = n'
      ============================
      S (n' + 0) = S n'
    *)
    rewrite -> IHn'.
    reflexivity.

  Restart.

  intro n.
  induction n as [ | n' IHn'].
  - exact (fold_unfold_add_O 0).
  - rewrite -> (fold_unfold_add_S n' 0).
    (*
      n' : nat
      IHn' : n' + 0 = n'
      ============================
      S (n' + 0) = S n'
    *)
    Search (_ = _ -> S _ = S _).
    (* eq_S: forall x y : nat, x = y -> S x = S y *)
    Check (eq_S (n' + 0) n').
    apply (eq_S (n' + 0) n').
    exact IHn'.

  Restart.

  intro n.
  induction n as [ | n' IHn'].
  - exact (fold_unfold_add_O 0).
  - rewrite -> (fold_unfold_add_S n' 0).
    (*
      n' : nat
      IHn' : n' + 0 = n'
      ============================
      S (n' + 0) = S n'
    *)
    Check f_equal. (* : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y *)
    Check (f_equal S). (* : forall x y : nat, x = y -> S x = S y *)
    Check (f_equal S IHn'). (* : S (n' + 0) = S n' *)
    exact (f_equal S IHn').
Qed.

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

(* end of week-07_functional-equality.v *)