(* week-04_specifications-that-depend-on-other-specifications.v *)
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 09 Feb 2024 *)


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

(* ***** *)

Theorem O_is_left_neutral_for_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n : nat,
      add 0 n = n.
Proof.
  intros add.
  unfold recursive_specification_of_addition.
  intros [S_add_O S_add_S].
  exact (S_add_O).
Qed.


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

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_wrt_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_wrt_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.

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

Theorem O_is_left_neutral_wrt_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall y : nat,
      add 0 y = y.
Proof.
  intros add S_add.
  assert (S_tmp := S_add).
  unfold recursive_specification_of_addition in S_tmp.
  destruct S_tmp as [S_add_O _].
  exact S_add_O.
  Qed.


Property SO_is_left_neutral_wrt_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_wrt_addition add S_add y).
  exact (O_is_left_neutral_wrt_addition add S_add y).
Qed.

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

(* Exercise 01 *)

Theorem O_is_right_neutral_wrt_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall y : nat,
      add y 0 = y.
Proof.
  intros add S_add.
  assert (S_tmp := S_add).
  unfold recursive_specification_of_addition in S_tmp.
  destruct S_tmp as [S_add_O S_add_S].
  intro y.
  induction y as [| y' IHy'].
  - exact (S_add_O 0).
  - rewrite -> (S_add_S y' 0).
    rewrite -> IHy'.
    reflexivity.
  Qed.

Property O_is_right_absorbing_wrt_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_wrt_addition add S_add).
    exact (O_is_right_neutral_wrt_addition add S_add 0).
Qed.

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

(* Exercise 02 *)

Theorem addition_is_commutative :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n1 n2 : nat,
      add n1 n2 = add n2 n1.
Proof.
  intros add S_add.
  assert (S_tmp := S_add).
  unfold recursive_specification_of_addition in S_tmp.
  destruct S_tmp as [S_add_O S_add_S].
  intro x.
  induction x as [| x' IHx'].
  - intro y.
    rewrite -> (S_add_O y).
    rewrite -> (O_is_right_neutral_wrt_addition add S_add y).
    reflexivity.
  - intro y.
    rewrite -> (S_add_S x' y).
    rewrite -> (IHx' y).
Admitted.

Property SO_is_right_neutral_wrt_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.
  (* My implementation *)
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  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'.
    assert (S_tmp := S_add).
    destruct S_tmp as [S_add_O S_add_S].
    Check (addition_is_commutative add S_add x' 1).
    rewrite -> (addition_is_commutative add S_add x' 1).
    rewrite -> (S_add_S 0 x').
    rewrite -> (S_add_O x').
    reflexivity.

    Restart.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  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 (addition_is_commutative add S_add).
    Check (addition_is_commutative add S_add x' 1).
    rewrite -> (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 *)
Theorem associativity_of_recursive_addition :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall n1 n2 n3 : nat,
      add n1 (add n2 n3) = add (add n1 n2) n3.
Proof.
Admitted.

Property multiplication_is_right_distributive_over_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.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  destruct (S_tmp add S_add) as [S_mul_O S_mul_S].
  clear S_tmp.
  assert (S_tmp := S_add).
  unfold recursive_specification_of_addition in S_tmp.
  destruct S_tmp as [S_add_O S_add_S].
  intros x.

  induction x as [| x' IHx'].
  - intros y z.
    rewrite -> (S_add_O y).
    rewrite -> (S_mul_O z).
    rewrite -> (S_add_O (mul y z)).
    reflexivity.
  - intros y z.
    rewrite -> (S_add_S x' y).
    rewrite -> (S_mul_S (add x' y) z).
    rewrite -> (S_mul_S x' z).
    rewrite -> (IHx' y z).
    rewrite -> (addition_is_commutative add S_add (add (mul x' z) (mul y z)) z).
    rewrite -> (associativity_of_recursive_addition add S_add z (mul x' z) (mul y z)).
    rewrite -> (addition_is_commutative add S_add z (mul x' z)).
    reflexivity.
Qed. (* <-- needed for later on *)

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

(* Exercise 04 *)

Property 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.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  destruct (S_tmp add S_add) as [S_mul_O S_mul_S].
  clear S_tmp.
  intros x.
  induction x as [| x' IHx'].
  - intros y z.
    rewrite -> (S_mul_O (mul y z)).
    rewrite -> (S_mul_O y).
    rewrite -> (S_mul_O z).
    reflexivity.

  - intros y z.
    rewrite -> (S_mul_S x' (mul y z)).
    rewrite -> (IHx' y z).
    rewrite -> (S_mul_S x' y).
    Check (multiplication_is_right_distributive_over_addition add S_add mul S_mul).
    rewrite -> (multiplication_is_right_distributive_over_addition add S_add mul S_mul (mul x' y) y z).
    reflexivity.
    Show Proof.
Qed.

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

(* Exercise 05 *)

Check Nat.mul_0_r.

Theorem addition_is_associative :
  forall add : nat -> nat -> nat,
    recursive_specification_of_addition add ->
    forall x y z : nat,
      add (add x y) z = add x (add y z).
  Proof.
    Admitted.

Lemma commutativity_of_recursive_multiplication_S :
  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 (S y) = add (mul x y) x.
Proof.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  destruct (S_tmp add S_add) as [S_mul_O S_mul_S].
  clear S_tmp.
  assert (S_tmp := S_add).
  unfold recursive_specification_of_addition in S_tmp.
  destruct S_tmp as [S_add_O S_add_S].
  intro x.
  induction x as [| x' IHx'].
  - intro y.
    rewrite -> (S_mul_O (S y)).
    rewrite -> (S_mul_O y).
    rewrite -> (S_add_O 0).
    reflexivity.
  - intro y.
    rewrite -> (addition_is_commutative add S_add (mul (S x') y) (S x')).
    rewrite -> (S_add_S x' (mul (S x') y)).
    rewrite -> (S_mul_S x' y).
    rewrite -> (S_mul_S x' (S y)).
    rewrite -> (IHx' y).
    rewrite -> (addition_is_commutative add S_add (add (mul x' y) x') (S y)).
    rewrite -> (S_add_S y (add (mul x' y) x')).
    rewrite -> (addition_is_commutative add S_add (add (mul x' y) x') (S y)).
    rewrite -> (addition_is_associative )




Property 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.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  destruct (S_tmp add S_add) as [S_mul_O S_mul_S].
  clear S_tmp.
  assert (S_tmp := S_add).
  unfold recursive_specification_of_addition in S_tmp.
  destruct S_tmp as [S_add_O S_add_S].
  intro x.
  induction x as [| x' IHx'].
  - intro y.
    rewrite -> (S_mul_O y).
    rewrite -> (O_is_right_absorbing_wrt_multiplication add S_add mul S_mul y).
    reflexivity.
  - intro y.
    (* rewrite -> (S_mul_S x' y). *)
    (* rewrite ->  (addition_is_commutative add S_add (mul x' y) y). *)
    (* rewrite -> (IHx' y). *)
    (* rewrite <- (SO_is_right_neutral_wrt_multiplication add S_add mul S_mul x') at 1. *)
    (* rewrite -> (multiplication_is_associative add S_add mul S_mul y x' 1). *)
    (* rewrite <- (IHx' y). *)
    (* rewrite <- (multiplication_is_associative add S_add mul S_mul x' y 1). *)
    (* rewrite -> (SO_is_right_neutral_wrt_multiplication add S_add mul S_mul y). *)
    rewrite -> (S_mul_S x' y).
    Check (add (mul x' y) y).

    (* TODO FINISH THIS *)

Admitted. (* <-- needed for later on *)

Lemma S_mul_S_reversed :
  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 y (S x) = add (mul x y) y.
Proof.
  intros add S_add mul S_mul.
  assert (S_tmp := S_mul).
  unfold recursive_specification_of_multiplication in S_tmp.
  destruct (S_tmp add S_add) as [S_mul_O S_mul_S].
  clear S_tmp.
  assert (S_tmp := S_add).
  unfold recursive_specification_of_addition in S_tmp.
  destruct S_tmp as [S_add_O S_add_S].
  intro x.
  induction x as [| x' IHx'].
  - intro y.
    rewrite -> (S_mul_O y).
    rewrite -> (SO_is_right_neutral_wrt_multiplication add S_add mul S_mul y).
    rewrite -> (S_add_O y).
    reflexivity.
  - intro y.
    Abort.




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

(* Exercise 06 *)

Property multiplication_is_left_distributive_over_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 -> (multiplication_is_commutative add S_add mul S_mul z (add x y)).
  rewrite -> (multiplication_is_commutative add S_add mul S_mul z x).
  rewrite -> (multiplication_is_commutative add S_add mul S_mul z y).
  exact (multiplication_is_right_distributive_over_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-04_specifications-that-depend-on-other-specifications.v *)