(* week-03_formalizing-a-proof-in-tcpa.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 01 Feb 2025 with a solution for Exercise 03 *)
(* was: *)
(* Version of 31 Jan 2025 *)

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

Require Import Arith Bool.

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

Search (_ + 0 = _).

Check Nat.add_0_r.

Proposition first_formal_proof :
  forall n : nat,
    n + 0 = 0 + n.
Proof.
  intro n.
  Check (Nat.add_0_r n).
  rewrite -> (Nat.add_0_r n).
  Check (Nat.add_0_l n).
  rewrite -> (Nat.add_0_l n).
  reflexivity.
Qed.

Check first_formal_proof.

Proposition first_formal_proof' :
  forall n : nat,
    n + 0 = 0 + n.
Proof.
  intro n.
  rewrite -> (Nat.add_0_l n).
  rewrite -> (Nat.add_0_r n).
  reflexivity.
Qed.

Proposition first_formal_proof'' :
  forall n : nat,
    n + 0 = 0 + n.
Proof.
  intro n.
  rewrite -> (Nat.add_0_r n).
  rewrite -> (Nat.add_0_l n).
  reflexivity.

  Restart.

  intro n.
  rewrite -> (Nat.add_0_l n).
  rewrite -> (Nat.add_0_r n).
  reflexivity.
Qed.

Proposition first_formal_proof''' :
  forall n : nat,
    n + 0 = 0 + n.
Proof.
  intro n.
  Check (Nat.add_comm n 0).
  exact (Nat.add_comm n 0).

  Restart.

  intro n.
  Check (Nat.add_comm 0 n).
  symmetry.
  exact (Nat.add_comm 0 n).
Qed.

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

Search (_ + _ = _ + _).

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

Check (Nat.add_comm 2 3).

Proposition second_formal_proof :
(*
  forall x : nat,
    forall y : nat,
      forall y : nat,
        x + (y + z) = y + (x + z).
*)
  forall x y z : nat,
    x + (y + z) = y + (x + z).
Proof.
  intro x.
  intro y.
  intro z.

  Restart.

  intros x y z.
  Check (Nat.add_assoc x y z).
  rewrite -> (Nat.add_assoc x y z).    (* rewrite from left to right *)
  Check (Nat.add_comm x y).
  rewrite -> (Nat.add_comm x y).       (* rewrite from left to right *)
  Check (Nat.add_assoc y x z).
  rewrite <- (Nat.add_assoc y x z).    (* rewrite from right to left *)
  reflexivity.

  Restart.

  intros x y z.
  Check (Nat.add_assoc y x z).
  rewrite -> (Nat.add_assoc y x z).
  Check (Nat.add_comm y x).
  rewrite -> (Nat.add_comm y x).
  Check (Nat.add_assoc x y z).
  exact (Nat.add_assoc x y z).
Qed.

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

Proposition third_formal_proof :
  forall n : nat,
    n + 0 + 0 = 0 + 0 + n.
Proof.
  intro n.
  Check (Nat.add_0_r n).
  rewrite -> (Nat.add_0_r n).
  rewrite -> (Nat.add_0_r n).
(*
  rewrite -> (Nat.add_0_l n).
*)
  Check (Nat.add_0_l n).
  Check (Nat.add_0_l 0).
  rewrite -> (Nat.add_0_l 0).
  rewrite -> (Nat.add_0_l n).
  reflexivity.

  Restart.

  intro n.
  rewrite -> (Nat.add_0_r n).
  rewrite -> (Nat.add_0_r n).
  rewrite -> (Nat.add_0_l 0).
  symmetry.
  exact (Nat.add_0_l n).

  Restart.

  Check first_formal_proof.
  intro n.
  Check (first_formal_proof (n + 0)).
  rewrite -> (first_formal_proof (n + 0)).
  Check (first_formal_proof n).
  rewrite -> (first_formal_proof n).
  Check (Nat.add_assoc 0 0 n).
  exact (Nat.add_assoc 0 0 n).

  Restart.

  intro n.
  Check (Nat.add_0_l 0).
  rewrite -> (Nat.add_0_l 0).
  rewrite -> (Nat.add_0_r n).
  exact (first_formal_proof n).
Qed.

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

(* Exercise 03 *)

Check Nat.mul_1_l.

Search (0 * _ = _).
(* Nat.mul_0_l: forall n : nat, 0 * n = 0 *)

Search (S _ * _ = _ + _).
(* Nat.mul_succ_l: forall n m : nat, S n * m = n * m + m *)

Lemma mul_1_l :
  forall x : nat,
    1 * x = x.
Proof.
  intro x.
  Check (Nat.mul_succ_l 0 x).
  rewrite -> (Nat.mul_succ_l 0 x).
  Check (Nat.mul_0_l x).
  rewrite -> (Nat.mul_0_l x).
  Check (Nat.add_0_l x).
  exact (Nat.add_0_l x).
Qed.

Lemma twice :
  forall x : nat,
    x + x = 2 * x.
Proof.
  intro x.
  Check (Nat.mul_succ_l 1 x).
  rewrite -> (Nat.mul_succ_l 1 x).
  Check (mul_1_l x).
  rewrite -> (mul_1_l x).
  reflexivity.
Qed.

Lemma helpful :
  forall a b c : nat,
    a + b + b + c = a + 2 * b + c.
Proof.
  intros a b c.
  Check Nat.add_assoc.
  Check (Nat.add_assoc a b b).
  rewrite <- (Nat.add_assoc a b b).
  Check (twice b).
  rewrite -> (twice b).
  reflexivity.
Qed.

Theorem binomial_expansion_2 :
  forall x y : nat,
    (x + y) * (x + y) = x * x + 2 * (x * y) + y * y.
Proof.
  intros x y.
  Search ((_ + _) * _ = _).
  Check (Nat.mul_add_distr_r x y (x + y)).
  rewrite -> (Nat.mul_add_distr_r x y (x + y)).
  Search (_ * (_ + _) = _).
  Check (Nat.mul_add_distr_l x x y).
  rewrite -> (Nat.mul_add_distr_l x x y).
  Check (Nat.mul_add_distr_l y x y).
  rewrite -> (Nat.mul_add_distr_l y x y).
  Check Nat.add_assoc.
  Check (Nat.add_assoc (x * x + x * y) (y * x) (y * y)).
  rewrite -> (Nat.add_assoc (x * x + x * y) (y * x) (y * y)).
  Check Nat.mul_comm.
  Check (Nat.mul_comm y x).
  rewrite -> (Nat.mul_comm y x).
  Check (helpful (x * x) (x * y) (y * y)).
  exact (helpful (x * x) (x * y) (y * y)).
Qed.

(* ***** *)

(* Exercise 04 *)

Theorem binomial_expansion_2_alt :
  forall x y : nat,
    (x + y) * (x + y) = x * x + 2 * (x * y) + y * y.
Proof.
Abort.

(* ***** *)

(* Exercise 05 *)

Theorem foo :
  forall x : nat,
    (x + 1) * (x + 1) = x * x + 2 * x + 1.
Proof.
Abort.

Theorem bar :
  forall x : nat,
    S x * S x = S (x * x + 2 * x).
Proof.
Abort.

Theorem baz :
  forall x : nat,
    S x * S x = S (S (S x) * x).
Proof.
Abort.

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

(* Exercise 06 *)

Lemma add_shuffle0 :
  forall n m p : nat,
    n + m + p = n + p + m.
Proof.
  exact Nat.add_shuffle0.

  Restart.

  intros n m p.
Abort.

Lemma add_shuffle1 :
  forall n m p q : nat,
    n + m + (p + q) = n + p + (m + q).
Proof.
  exact Nat.add_shuffle1.

  Restart.

  intros n m p q.
Abort.

Lemma add_shuffle2 :
  forall n m p q : nat,
    n + m + (p + q) = n + q + (m + p).
Proof.
  exact Nat.add_shuffle2.

  Restart.

  intros n m p q.
Abort.

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

(* end of week-03_formalizing-a-proof-in-tcpa.v *)