feat: 3234 week 4 wip

cs3234/labs/week-04_specifications-that-depend-on-other-specifications.v

@@ -0,0 +1,415 @@
+(* 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.
+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_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.
+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.
+Qed.
+
+(* ********** *)
+
+(* Exercise 05 *)
+
+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 -> (IHx' y).
+    Check (multiplication_is_right_distributive_over_addition add S_add mul S_mul).
+
+
+Qed. (* <-- needed for later on *)
+
+(* ********** *)
+
+(* 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 *)