(* week-09_life-after-the-midterm-project.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 21 Mar 2025 *)

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

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

Require Import Arith Bool List.

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

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

Check Nat.add_assoc.
(* : forall n m p : nat, n + (m + p) = n + m + p *)

Proposition add_assoc :
  forall i j k : nat,
    i + (j + k) = (i + j) + k.
Proof.
  intros i j k.
  induction i as [ | i' IHi'].
  - rewrite -> (fold_unfold_add_O (j + k)).
    rewrite -> (fold_unfold_add_O j).
    reflexivity.
  - rewrite -> (fold_unfold_add_S i' (j + k)).
    rewrite -> (fold_unfold_add_S i' j).
    rewrite -> IHi'.
    rewrite -> (fold_unfold_add_S (i' + j) k).
    reflexivity.

  Restart.

  intros i j k.
  induction i as [ | i' IHi'].
  - rewrite -> fold_unfold_add_O.
    rewrite -> fold_unfold_add_O.
    reflexivity.

  Restart.

  intros i j k.
  induction i as [ | i' IHi'].
  - rewrite ->2 fold_unfold_add_O.
    reflexivity.
  - rewrite ->2 fold_unfold_add_S.
    rewrite -> IHi'.
    rewrite -> fold_unfold_add_S.
    reflexivity.

  Restart.

  intros i j k.
  induction i as [ | i' IHi'].
  - rewrite ->2 fold_unfold_add_O.
    reflexivity.
  - rewrite ->2 fold_unfold_add_S.
    rewrite -> IHi'.
    Check (fold_unfold_add_S (i' + j) k).
    Check (eq_sym (fold_unfold_add_S (i' + j) k)).
    exact (eq_sym (fold_unfold_add_S (i' + j) k)).
Qed.

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

(* end of week-09_life-after-the-midterm-project.v *)