(* week-05_specifications-that-depend-on-other-specifications.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 14 Feb 2025 *)
(* was: *)
(* Version of 13 Feb 2025 *)

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

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

(* Name: 
   Student number: 
   Email address: 
*)

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

(* Paraphernalia: *)

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

Require Import Arith Bool.

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

Definition recursive_specification_of_addition (add : nat -> nat -> nat) :=
  (forall y : nat,
      add O y = y)
  /\
  (forall x' y : nat,
      add (S x') y = S (add x' y)).

Definition tail_recursive_specification_of_addition (add : nat -> nat -> nat) :=
  (forall y : nat,
      add O y = y)
  /\
  (forall x' y : nat,
      add (S x') y = add x' (S y)).

(* ***** *)

Property O_is_left_neutral_for_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n : nat,
      add 0 n = n.
Admitted.

Property O_is_right_neutral_for_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n : nat,
      add n 0 = n.
Admitted.

Theorem recursive_addition_is_commutative :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n1 n2 : nat,
      add n1 n2 = add n2 n1.
Admitted.

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

Definition recursive_specification_of_multiplication (mul : nat -> nat -> nat) :=
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    (forall y : nat,
        mul O y = 0)
    /\
    (forall x' y : nat,
        mul (S x') y = add (mul x' y) y).

(* ***** *)

Property O_is_left_absorbing_for_recursive_multiplication :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall mul : nat -> nat -> nat,
      recursive_specification_of_multiplication mul ->
      forall y : nat,
        mul 0 y = 0.
Proof.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  Check (S_tmp add S_add).
  destruct (S_tmp add S_add) as [S_mul_O _].
  clear S_tmp.
  exact S_mul_O.
Qed.

Fixpoint add_v1 (i j : nat) : nat :=
  match i with
    O =>
    j
  | S i' =>
    S (add_v1 i' j)
  end.

Theorem add_v1_satisfies_the_recursive_specification_of_addition :
  recursive_specification_of_addition add_v1.
Proof.
Admitted.


Property O_is_left_absorbing_for_recursive_multiplication_alt :
  forall mul : nat -> nat -> nat,
    recursive_specification_of_multiplication mul ->
    forall y : nat,
      mul 0 y = 0.
Proof.
  intros mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  Check (S_tmp add_v1).
  Check (S_tmp add_v1 add_v1_satisfies_the_recursive_specification_of_addition).
  destruct (S_tmp add_v1 add_v1_satisfies_the_recursive_specification_of_addition) as [S_mul_O _].
  clear S_tmp.
  exact S_mul_O.
Qed.

(* ***** *)

Property SO_is_left_neutral_for_recursive_multiplication :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall mul : nat -> nat -> nat,
      recursive_specification_of_multiplication mul ->
      forall y : nat,
        mul 1 y = y.
Proof.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  Check (S_tmp add S_add).
  destruct (S_tmp add S_add) as [S_mul_O S_mul_S].
  clear S_tmp.
  intro y.
  Check (S_mul_S 0 y).
  rewrite -> (S_mul_S 0 y).
  rewrite -> (S_mul_O y).
  Check (O_is_left_neutral_for_recursive_addition add S_add y).
  exact (O_is_left_neutral_for_recursive_addition add S_add y).
Qed.

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

(* Exercise 01 *)

Property O_is_right_absorbing_for_recursive_multiplication :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall mul : nat -> nat -> nat,
      recursive_specification_of_multiplication mul ->
      forall x : nat,
        mul x 0 = 0.
Proof.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  Check (S_tmp add S_add).
  destruct (S_tmp add S_add) as [S_mul_O S_mul_S].
  clear S_tmp.
  intro x.
  induction x as [ | x' IHx'].

  - exact (S_mul_O 0).

  - rewrite -> (S_mul_S x' 0).
    rewrite -> IHx'.
    Check (O_is_right_neutral_for_recursive_addition add S_add).
    exact (O_is_right_neutral_for_recursive_addition add S_add 0).
Qed.

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

(* Exercise 02 *)

Property SO_is_right_neutral_for_recursive_multiplication :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall mul : nat -> nat -> nat,
      recursive_specification_of_multiplication mul ->
      forall x : nat,
        mul x 1 = x.
Proof.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  Check (S_tmp add S_add).
  destruct (S_tmp add S_add) as [S_mul_O S_mul_S].
  clear S_tmp.
  intro x.
  induction x as [ | x' IHx'].

  - exact (S_mul_O 1).

  - rewrite -> (S_mul_S x' 1).
    rewrite -> IHx'.
    Check (recursive_addition_is_commutative add S_add).
    Check (recursive_addition_is_commutative add S_add x' 1).
    rewrite -> (recursive_addition_is_commutative add S_add x' 1).
    assert (S_tmp := S_add).
    unfold recursive_specification_of_addition in S_tmp.
    destruct S_tmp as [S_add_O S_add_S].
    rewrite -> (S_add_S 0 x').
    rewrite -> (S_add_O x').
    reflexivity.
Qed.

(* ***** *)

(* Exercise 03 *)

Property recursive_multiplication_is_right_distributive_over_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall mul : nat -> nat -> nat,
      recursive_specification_of_multiplication mul ->
      forall x y z : nat,
        mul (add x y) z = add (mul x z) (mul y z).
Proof.
Admitted. (* <-- needed for later on *)

(* ***** *)

(* Exercise 04 *)

Property recursive_multiplication_is_associative :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall mul : nat -> nat -> nat,
      recursive_specification_of_multiplication mul ->
      forall x y z : nat,
        mul x (mul y z) = mul (mul x y) z.
Proof.
Abort.

(* ***** *)

(* Exercise 05 *)

Property recursive_multiplication_is_commutative :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall mul : nat -> nat -> nat,
      recursive_specification_of_multiplication mul ->
      forall x y : nat,
        mul x y = mul y x.
Proof.
Admitted. (* <-- needed for later on *)

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

(* Exercise 06 *)

Property recursive_multiplication_is_left_distributive_over_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall mul : nat -> nat -> nat,
      recursive_specification_of_multiplication mul ->
      forall x y z : nat,
        mul x (add y z) = add (mul x y) (mul x z).
Proof.
  intros add S_add mul S_mul z x y.
  rewrite -> (recursive_multiplication_is_commutative add S_add mul S_mul z (add x y)).
  rewrite -> (recursive_multiplication_is_commutative add S_add mul S_mul z x).
  rewrite -> (recursive_multiplication_is_commutative add S_add mul S_mul z y).
  exact (recursive_multiplication_is_right_distributive_over_recursive_addition add S_add mul S_mul x y z).
Qed.

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

(* The resident McCoys: *)

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

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

Search (1 * _ = _).
(* Nat.mul_1_l: forall n : nat, 1 * n = n *)

Check Nat.mul_1_r.
(* Nat.mul_1_r : forall n : nat, n * 1 = n *)

Search ((_ + _) * _ = _).
(* Nat.mul_add_distr_r : forall n m p : nat, (n + m) * p = n * p + m * p
*)

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

Search ((_ * _) * _ = _).
(* mult_assoc_reverse: forall n m p : nat, n * m * p = n * (m * p) *)

Search (_ * (_ * _) = _).
(* Nat.mul_assoc: forall n m p : nat, n * (m * p) = n * m * p *)

Check Nat.mul_comm.
(* Nat.mul_comm : forall n m : nat, n * m = m * n *)

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

(* end of week-05_specifications-that-depend-on-other-specifications.v *)