(* week-04_structural-induction-over-Peano-numbers.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 07 Feb 2025 *)

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

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

(* name: 
   e-mail address: 
   student number: 
*)

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

Require Import Arith.

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

Definition specification_of_the_addition_function_1 (add : nat -> nat -> nat) :=
  (forall j : nat,
      add O j = j)
  /\
  (forall i' j : nat,
      add (S i') j = S (add i' j)).

Check nat_ind.
(*
nat_ind
     : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
*)

Proposition add_0_r_v0 :
  forall add : nat -> nat -> nat,
    specification_of_the_addition_function_1 add ->
    forall n : nat,
      add n 0 = n.
Proof.
  intro add.
  unfold specification_of_the_addition_function_1.
  intros [S_add_O S_add_S].
  Check (nat_ind
           (fun n => add n 0 = n)).
  Check (S_add_O 0).
  Check (nat_ind
           (fun n => add n 0 = n)
           (S_add_O 0)).
  apply (nat_ind
           (fun n => add n 0 = n)
           (S_add_O 0)).
  intro n'.
  intro IHn'.
  Check (S_add_S n' 0).
  rewrite -> (S_add_S n' 0).
  rewrite -> IHn'.
  reflexivity.
Qed.

Search (0 + _ = _).
(* plus_O_n: forall n : nat, 0 + n = n *)  
(* Nat.add_0_l: forall n : nat, 0 + n = n *)
Search (S _ + _ = _).
(* plus_Sn_m: forall n m : nat, S n + m = S (n + m) *)
(* Nat.add_succ_l: forall n m : nat, S n + m = S (n + m) *)

Proposition add_0_r_v1 :
  forall n : nat,
    n + 0 = n.
Proof.
  Check (nat_ind
           (fun n => n + 0 = n)).
  Check (Nat.add_0_l 0).
  Check (nat_ind
           (fun n => n + 0 = n)
           (Nat.add_0_l 0)).
  apply (nat_ind
           (fun n => n + 0 = n)
           (Nat.add_0_l 0)).
  intros n' IHn'.
  Check (Nat.add_succ_l n' 0).
  rewrite -> (Nat.add_succ_l n' 0).
  rewrite -> IHn'.
  reflexivity.

  Restart.

  intro n.
  induction n using nat_ind.
  - Check (Nat.add_0_l 0).
    exact (Nat.add_0_l 0).
  - revert n IHn.
    intros n' IHn'.
    Check (Nat.add_succ_l n' 0).
    rewrite -> (Nat.add_succ_l n' 0).
    rewrite -> IHn'.
    reflexivity.

  Restart.

  intro n.
  induction n as [ | n' IHn'] using nat_ind.
  - Check (Nat.add_0_l 0).
    exact (Nat.add_0_l 0).
  - Check (Nat.add_succ_l n' 0).
    rewrite -> (Nat.add_succ_l n' 0).
    rewrite -> IHn'.
    reflexivity.

  Restart.

  intro n.
  induction n as [ | n' IHn'].
  - Check (Nat.add_0_l 0).
    exact (Nat.add_0_l 0).
  - Check (Nat.add_succ_l n' 0).
    rewrite -> (Nat.add_succ_l n' 0).
    rewrite -> IHn'.
    reflexivity.
Qed.

Proposition add_0_r_v0_revisited :
  forall add : nat -> nat -> nat,
    specification_of_the_addition_function_1 add ->
    forall n : nat,
      add n 0 = n.
Proof.
  intro add.
  unfold specification_of_the_addition_function_1.
  intros [S_add_O S_add_S].
  intro n.
  induction n as [ | n' IHn'].
  - exact (S_add_O 0).
  - rewrite -> (S_add_S n' 0).
    rewrite -> IHn'.
    reflexivity.
Qed.

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

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 *)

Proposition mul_0_r_v1 :
  forall n : nat,
    n * 0 = 0.
Proof.
  intro n.
  induction n as [ | n' IHn'].
  - Check (Nat.mul_0_l 0).
    exact (Nat.mul_0_l 0).
  - Check (Nat.mul_succ_l n' 0).
    rewrite -> (Nat.mul_succ_l n' 0).
    rewrite -> IHn'.
    Check (Nat.add_0_l 0).
    exact (Nat.add_0_l 0).
Qed.

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

(* Exercise 02 *)

Definition specification_of_foo_in_Week_01 (foo : nat -> nat) :=
  (foo O = 0)
  /\
  (forall n' : nat,
    foo (S n') = S (S (foo n'))).

Lemma twice_S :
  forall n : nat,
    2 * S n = S (S (2 * n)).
Proof.
Abort.

Theorem about_foo :
  forall foo : nat -> nat,
    specification_of_foo_in_Week_01 foo ->
    forall a b : nat,
      foo a = b ->
      b = 2 * a.
Proof.
  intro foo.
  unfold specification_of_foo_in_Week_01.
  intros [S_foo_O S_foo_S].
  intros a b H_foo.
  rewrite <- H_foo.
Abort.

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

(* Exercise 03 *)

Definition specification_of_bar_in_Week_01 (bar : nat -> nat) :=
  (bar O = 0)
  /\
  (forall n' : nat,
    bar (S n') = S (S (S (bar n')))).

Lemma thrice_S :
  forall n : nat,
    3 * S n = S (S (S (3 * n))).
Proof.
Abort.

Theorem about_bar :
  forall bar : nat -> nat,
    specification_of_bar_in_Week_01 bar ->
    forall a b : nat,
      bar a = b ->
      b = 3 * a.
Proof.
Abort.

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

(* end of week-04_structural-induction-over-Peano-numbers.v *)