From 7ef2e570ea96255f7d6f8f7f93e70bd2d1650187 Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Wed, 14 Feb 2024 18:50:26 +0800 Subject: [PATCH] feat: 3234 week 4 wip --- ...ions-that-depend-on-other-specifications.v | 415 ++++++++++++++++++ 1 file changed, 415 insertions(+) create mode 100644 cs3234/labs/week-04_specifications-that-depend-on-other-specifications.v diff --git a/cs3234/labs/week-04_specifications-that-depend-on-other-specifications.v b/cs3234/labs/week-04_specifications-that-depend-on-other-specifications.v new file mode 100644 index 0000000..ca0433b --- /dev/null +++ b/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 *) +(* 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 *)