diff --git a/cs3234/labs/week-04_backward-and-forward-proofs.v b/cs3234/labs/week-04_backward-and-forward-proofs.v new file mode 100644 index 0000000..df56f8a --- /dev/null +++ b/cs3234/labs/week-04_backward-and-forward-proofs.v @@ -0,0 +1,227 @@ +(* week-04_backward-and-forward-proofs.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 09 Feb 2024 *) + +(* ***********) + +(* Learning goals: + + * using apply among the assumptions + + * using assert to declare a new assumption + + * using split to prove conjunctions +*) + +(* ***********) + +Proposition identity : + forall A : Prop, + A -> A. +Proof. + intros A H_A. + apply H_A. +Qed. + +Proposition modus_ponens : + forall A B : Prop, + A -> (A -> B) -> B. +Proof. + intros A B H_A H_A_implies_B. + (* backward, from the goal: *) + apply H_A_implies_B. + apply H_A. + + Restart. + + intros A B H_A H_A_implies_B. + (* forward, from the initial hypothesis: *) + apply H_A_implies_B in H_A. + exact H_A. + + Restart. + + intros A B H_A H_A_implies_B. + (* forward, keeping in control of the naming: *) + assert (H_B := H_A_implies_B H_A). + exact H_B. +Qed. + +Proposition modus_ponens_and_more : + forall A B C : Prop, + A -> (A -> B) -> (B -> C) -> C. +Proof. + intros A B C H_A H_A_implies_B H_B_implies_C. + (* backward, from the goal: *) + apply H_B_implies_C. + apply H_A_implies_B. + apply H_A. + + Restart. + + intros A B C H_A H_A_implies_B H_B_implies_C. + (* forward, from the initial hypothesis: *) + Check (H_A_implies_B H_A). + assert (H_B := H_A_implies_B H_A). + Check (H_B_implies_C H_B). + exact (H_B_implies_C H_B). +Qed. + +Proposition modus_ponens_and_even_more : + forall A B C D : Prop, + A -> (A -> B) -> (B -> C) -> (C -> D) -> D. +Proof. + intros A B C D H_A H_A_implies_B H_B_implies_C H_C_implies_D. + (* backward, from the goal: *) + apply H_C_implies_D. + apply H_B_implies_C. + apply H_A_implies_B. + apply H_A. + + Restart. + + intros A B C D H_A H_A_implies_B H_B_implies_C H_C_implies_D. + (* forward, from the initial hypothesis: *) + assert (H_B := H_A_implies_B H_A). + assert (H_C := H_B_implies_C H_B). + Check (H_C_implies_D H_C). + exact (H_C_implies_D H_C). +Qed. + +(* ********** *) + +(* Prove foo: + + (1) backward, in a goal-directed way + + (2) forward, from the assumptions +*) + +Proposition foo : + forall P Q R1 R2 : Prop, + P -> (P -> Q) -> (Q -> R1) /\ (Q -> R2) -> R1 /\ R2. +Proof. +Abort. + +(* ********** *) + +(* Prove bar: + + (1) by using the split tactic as early as possible + + (2) by using the split tactic as late as possible +*) + +Proposition bar : + forall P1 P2 Q R1 R2 T1 T2 : Prop, + P1 -> (P1 -> P2) -> (P2 -> Q) -> (Q -> R1) -> (R1 -> T1) -> (Q -> R2) -> (R2 -> T2) -> T1 /\ T2. +Proof. + intros P1 P2 Q R1 R2 T1 T2. + intros H_P1 H_P1_implies_P2 H_P2_implies_Q H_Q_implies_R1 H_R1_implies_T1 H_Q_implies_R2 H_R2_implies_T2. + + (* Here, use the split tactic as early as possible. *) + + Restart. + + intros P1 P2 Q R1 R2 T1 T2. + intros H_P1 H_P1_implies_P2 H_P2_implies_Q H_Q_implies_R1 H_R1_implies_T1 H_Q_implies_R2 H_R2_implies_T2. + + (* Here, use the split tactic as late as possible. *) + +Abort. + +(* ********** *) + +(* Prove baz: + + (1) by using the split tactic as early as possible + + (2) by using the split tactic as late as possible +*) + +Proposition baz : + forall P Q R T U1 U2 : Prop, + P -> (P -> Q) -> (Q -> R) -> (R -> T) -> (T -> U1) -> (T -> U2) -> U1 /\ U2. +Proof. + intros P Q R T U1 U2. + intros H_P H_P_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U1 H_T_implies_U2. + + (* Here, use the split tactic as early as possible. *) + + Restart. + + intros P Q R T U1 U2. + intros H_P H_P_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U1 H_T_implies_U2. + + (* Here, use the split tactic as late as possible. *) + +Abort. + +(* ********** *) + +(* Complete the proofs of baz_dual, + and then compare them. +*) + +Proposition baz_dual_early : + forall P1 P2 Q R T U : Prop, + (P1 \/ P2) -> (P1 -> Q) -> (P2 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U. +Proof. + intros P1 P2 Q R T U. + intros H_P1_or_P2 H_P1_implies_Q H_P2_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U. + + (* use "destruct H_P1_or_P2 as [H_P1 | H_P2]." as early as you can *) + +Abort. + +Proposition baz_dual_late : + forall P1 P2 Q R T U : Prop, + (P1 \/ P2) -> (P1 -> Q) -> (P2 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U. +Proof. + intros P1 P2 Q R T U. + intros H_P1_or_P2 H_P1_implies_Q H_P2_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U. + + (* use "destruct H_P1_or_P2 as [H_P1 | H_P2]." as late as you can *) + +Abort. + +(* Complete the following proof. + What do you end up with? + A proof close to that of Proposition baz_dual_early, + or to that of Proposition baz_dual_late? + What do you conclude? +*) +Proposition baz_dual_early_or_late : + forall P1 P2 Q R T U : Prop, + (P1 \/ P2) -> (P1 -> Q) -> (P2 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U. +Proof. + intros P1 P2 Q R T U. + intros [H_P1 | H_P2] H_P1_implies_Q H_P2_implies_Q H_Q_implies_R H_R_implies_T H_T_implies_U. + +Abort. + +(* ********** *) + +(* How would you prove the following propositions? + Forward or backward? +*) + +Proposition ladidah : + forall P1 P2 P3 P4 Q R T U : Prop, + (P1 \/ P2) \/ (P3 \/ P4) -> (P1 -> Q) -> (P2 -> Q) -> (P3 -> Q) -> (P4 -> Q) -> (Q -> R) -> (R -> T) -> (T -> U) -> U. +Abort. + +Proposition toodeloo : + forall P Q R T U1 U2 U3 U4: Prop, + P -> (P -> Q) -> (Q -> R) -> (R -> T) -> (T -> U1) -> (T -> U2) -> (T -> U3) -> (T -> U4) -> (U1 /\ U2) /\ (U3 /\ U4). +Abort. + +(* How complex could the size of such proofs be + (relative to the number of hypotheses about P1, P2, P3, etc. + and to the number of conclusions about U1, U2, U3, etc.)? +*) + +(* ***********) + +(* end of week-04_backward-and-forward-proofs.v *) diff --git a/cs3234/labs/week-04_equational-reasoning-about-arithmetical-functions.v b/cs3234/labs/week-04_equational-reasoning-about-arithmetical-functions.v new file mode 100644 index 0000000..a9a547b --- /dev/null +++ b/cs3234/labs/week-04_equational-reasoning-about-arithmetical-functions.v @@ -0,0 +1,623 @@ +(* week-04_equational-reasoning-about-arithmetical-functions.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 09 Feb 2024 *) + +(* ********** *) + +(* 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. + +(* ********** *) + +(* Two implementations of the addition function *) + +(* ***** *) + +(* Unit tests *) + +Definition test_add (candidate: nat -> nat -> nat) : bool := + (candidate 0 0 =? 0) + && + (candidate 0 1 =? 1) + && + (candidate 1 0 =? 1) + && + (candidate 1 1 =? 2) + && + (candidate 1 2 =? 3) + && + (candidate 2 1 =? 3) + && + (candidate 2 2 =? 4) + (* etc. *) + . + +(* ***** *) + +(* Recursive implementation of the addition function *) + +Fixpoint add_v1 (i j : nat) : nat := + match i with + | O => + j + | S i' => + S (add_v1 i' j) + end. + +Compute (test_add add_v1). + +Lemma fold_unfold_add_v1_O : + forall j : nat, + add_v1 O j = + j. +Proof. + fold_unfold_tactic add_v1. +Qed. + +Lemma fold_unfold_add_v1_S : + forall i' j : nat, + add_v1 (S i') j = + S (add_v1 i' j). +Proof. + fold_unfold_tactic add_v1. +Qed. + +(* ***** *) + +(* Tail-recursive implementation of the addition function *) + +Fixpoint add_v2 (i j : nat) : nat := + match i with + | O => j + | S i' => add_v2 i' (S j) + end. + +Compute (test_add add_v2). + +Lemma fold_unfold_add_v2_O : + forall j : nat, + add_v2 O j = + j. +Proof. + fold_unfold_tactic add_v2. +Qed. + +Lemma fold_unfold_add_v2_S : + forall i' j : nat, + add_v2 (S i') j = + add_v2 i' (S j). +Proof. + fold_unfold_tactic add_v2. +Qed. + +(* ********** *) + +(* Equivalence of add_v1 and add_v2 *) + +(* ***** *) + +(* The master lemma: *) + +Lemma about_add_v2 : + forall i j : nat, + add_v2 i (S j) = S (add_v2 i j). +Proof +. + intro i. + induction i as [ | i' IHi']. + + - intro j. + rewrite -> (fold_unfold_add_v2_O j). + exact (fold_unfold_add_v2_O (S j)). + + - intro j. + rewrite -> (fold_unfold_add_v2_S i' (S j)). + rewrite -> (fold_unfold_add_v2_S i' j). + Check (IHi' (S j)). + exact (IHi' (S j)). +Qed. + +(* ***** *) + +(* The main theorem: *) + +Theorem equivalence_of_add_v1_and_add_v2 : + forall i j : nat, + add_v1 i j = add_v2 i j. +Proof. + intro i. + induction i as [ | i' IHi']. + + - intro j. + rewrite -> (fold_unfold_add_v2_O j). + exact (fold_unfold_add_v1_O j). + + - intro j. + rewrite -> (fold_unfold_add_v1_S i' j). + rewrite -> (fold_unfold_add_v2_S i' j). + rewrite -> (IHi' j). + symmetry. + exact (about_add_v2 i' j). +Qed. + +(* ********** *) + +(* Neutral (identity) element for addition *) + +(* ***** *) + +Property O_is_left_neutral_wrt_add_v1 : + forall y : nat, + add_v1 0 y = y. +Proof. + intro y. + exact (fold_unfold_add_v1_O y). +Qed. + +(* ***** *) + +Property O_is_left_neutral_wrt_add_v2 : + forall y : nat, + add_v2 0 y = y. +Proof. + exact (fold_unfold_add_v1_O). +Qed. + +(* ***** *) + +Property O_is_right_neutral_wrt_add_v1 : + forall x : nat, + add_v1 x 0 = x. +Proof. +Qed. + +Property O_is_right_neutral_wrt_add_v2 : + forall x : nat, + add_v2 x 0 = x. +Proof. +Qed. + +(* ********** *) + +(* Associativity of addition *) + +(* ***** *) + +Property add_v1_is_associative : + forall x y z : nat, + add_v1 x (add_v1 y z) = add_v1 (add_v1 x y) z. +Proof. +Qed. + +(* ***** *) + +Property add_v2_is_associative : + forall x y z : nat, + add_v2 x (add_v2 y z) = add_v2 (add_v2 x y) z. +Proof. +Qed. + +(* ********** *) + +(* Commutativity of addition *) + +(* ***** *) + +Property add_v1_is_commutative : + forall x y : nat, + add_v1 x y = add_v1 y x. +Proof. +Qed. + +(* ***** *) + +Property add_v2_is_commutative : + forall x y : nat, + add_v2 x y = add_v2 y x. +Proof. +Qed. + +(* ********** *) + +(* Four implementations of the multiplication function *) + +(* ***** *) + +(* Unit tests *) + +Definition test_mul (candidate: nat -> nat -> nat) : bool := + (candidate 0 0 =? 0) + && + (candidate 0 1 =? 0) + && + (candidate 1 0 =? 0) + && + (candidate 1 1 =? 1) + && + (candidate 1 2 =? 2) + && + (candidate 2 1 =? 2) + && + (candidate 2 2 =? 4) + && + (candidate 2 3 =? 6) + && + (candidate 3 2 =? 6) + && + (candidate 6 4 =? 24) + && + (candidate 4 6 =? 24) + (* etc. *) + . + +(* ***** *) + +(* Recursive implementation of the multiplication function, using add_v1 *) + +Fixpoint mul_v11 (x y : nat) : nat := + match x with + | O => + O + | S x' => + add_v1 (mul_v11 x' y) y + end. + +Compute (test_mul mul_v11). + +Lemma fold_unfold_mul_v11_O : + forall y : nat, + mul_v11 O y = + O. +Proof. + fold_unfold_tactic mul_v11. +Qed. + +Lemma fold_unfold_mul_v11_S : + forall x' y : nat, + mul_v11 (S x') y = + add_v1 (mul_v11 x' y) y. +Proof. + fold_unfold_tactic mul_v11. +Qed. + +(* ***** *) + +(* Recursive implementation of the multiplication function, using add_v2 *) + +Fixpoint mul_v12 (x y : nat) : nat := + match x with + | O => + O + | S x' => + add_v2 (mul_v12 x' y) y + end. + +Compute (test_mul mul_v11). + +Lemma fold_unfold_mul_v12_O : + forall y : nat, + mul_v12 O y = + O. +Proof. + fold_unfold_tactic mul_v12. +Qed. + +Lemma fold_unfold_mul_v12_S : + forall x' y : nat, + mul_v12 (S x') y = + add_v2 (mul_v12 x' y) y. +Proof. + fold_unfold_tactic mul_v12. +Qed. + +(* ***** *) + +(* Tail-recursive implementation of the multiplication function, using add_v1 *) + +(* +Definition mul_v21 (x y : nat) : nat := +*) + +(* ***** *) + +(* Tail-recursive implementation of the multiplication function, using add_v2 *) + +(* +Definition mul_v22 (x y : nat) : nat := +*) + +(* ********** *) + +(* Equivalence of mul_v11, mul_v12, mul_v21, and mul_v22 *) + +(* ***** *) + +Theorem equivalence_of_mul_v11_and_mul_v12 : + forall i j : nat, + mul_v11 i j = mul_v12 i j. +Proof. +Qed. + +(* ***** *) + +(* ... *) + +(* ***** *) + +(* ... *) + +(* ***** *) + +(* +Theorem equivalence_of_mul_v21_and_mul_v22 : + forall i j : nat, + mul_v21 i j = mul_v22 i j. +Proof. +Qed. +*) + +(* ********** *) + +(* 0 is left absorbing with respect to multiplication *) + +(* ***** *) + +Property O_is_left_absorbing_wrt_mul_v11 : + forall y : nat, + mul_v11 0 y = 0. +Proof. +Qed. + +(* ***** *) + +Property O_is_left_absorbing_wrt_mul_v12 : + forall y : nat, + mul_v12 0 y = 0. +Proof. +Qed. + +(* ***** *) + +(* +Property O_is_left_absorbing_wrt_mul_v21 : + forall y : nat, + mul_v21 0 y = 0. +Proof. +Qed. +*) + +(* ***** *) + +(* +Property O_is_left_absorbing_wrt_mul_v22 : + forall y : nat, + mul_v22 0 y = 0. +Proof. +Qed. +*) + +(* ********** *) + +(* 1 is left neutral with respect to multiplication *) + +(* ***** *) + +Property SO_is_left_neutral_wrt_mul_v11 : + forall y : nat, + mul_v11 1 y = y. +Proof. +Qed. + +(* ***** *) + +Property SO_is_left_neutral_wrt_mul_v12 : + forall y : nat, + mul_v12 1 y = y. +Proof. +Qed. + +(* ***** *) + +(* +Property SO_is_left_neutral_wrt_mul_v21 : + forall y : nat, + mul_v21 1 y = y. +Proof. +Qed. +*) + +(* ***** *) + +(* +Property SO_is_left_neutral_wrt_mul_v22 : + forall y : nat, + mul_v22 1 y = y. +Proof. +Qed. +*) + +(* ********** *) + +(* 0 is right absorbing with respect to multiplication *) + +(* ***** *) + +Property O_is_right_absorbing_wrt_mul_v11 : + forall x : nat, + mul_v11 x 0 = 0. +Proof. +Qed. + +(* ***** *) + +Property O_is_right_absorbing_wrt_mul_v12 : + forall x : nat, + mul_v12 x 0 = 0. +Proof. +Qed. + +(* ***** *) + +(* +Property O_is_right_absorbing_wrt_mul_v21 : + forall x : nat, + mul_v21 x 0 = 0. +Proof. +Qed. +*) + +(* ***** *) + +(* +Property O_is_right_absorbing_wrt_mul_v22 : + forall x : nat, + mul_v22 x 0 = 0. +Proof. +Qed. +*) + +(* ********** *) + +(* 1 is right neutral with respect to multiplication *) + +(* ***** *) + +Property SO_is_right_neutral_wrt_mul_v11 : + forall x : nat, + mul_v11 x 1 = x. +Proof. +Qed. + +(* ***** *) + +Property SO_is_right_neutral_wrt_mul_v12 : + forall x : nat, + mul_v12 x 1 = x. +Proof. +Qed. + +(* ***** *) + +(* +Property SO_is_right_neutral_wrt_mul_v21 : + forall x : nat, + mul_v21 x 1 = x. +Proof. +Qed. +*) + +(* ***** *) + +(* +Property SO_is_right_neutral_wrt_mul_v22 : + forall x : nat, + mul_v22 x 1 = x. +Proof. +Qed. +*) + +(* ********** *) + +(* Multiplication is right-distributive over addition *) + +(* ***** *) + +(* ... *) + +(* ********** *) + +(* Multiplication is associative *) + +(* ***** *) + +Property mul_v11_is_associative : + forall x y z : nat, + mul_v11 x (mul_v11 y z) = mul_v11 (mul_v11 x y) z. +Proof. +Qed. + +(* ***** *) + +Property mul_v12_is_associative : + forall x y z : nat, + mul_v12 x (mul_v12 y z) = mul_v12 (mul_v12 x y) z. +Proof. +Qed. + +(* ***** *) + +(* +Property mul_v21_is_associative : + forall x y z : nat, + mul_v21 x (mul_v21 y z) = mul_v21 (mul_v21 x y) z. +Proof. +Qed. +*) + +(* ***** *) + +(* +Property mul_v22_is_associative : + forall x y z : nat, + mul_v22 x (mul_v22 y z) = mul_v22 (mul_v22 x y) z. +Proof. +Qed. +*) + +(* ********** *) + +(* Multiplication is left-distributive over addition *) + +(* ***** *) + +(* ... *) + +(* ********** *) + +(* end of week-04_equational-reasoning-about-arithmetical-functions.v *) diff --git a/cs3234/labs/week-04_equational-reasoning.v b/cs3234/labs/week-04_equational-reasoning.v new file mode 100644 index 0000000..44bf52d --- /dev/null +++ b/cs3234/labs/week-04_equational-reasoning.v @@ -0,0 +1,533 @@ +(* week-04_equational-reasoning.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. + +(* ********** *) + +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)). + +Fixpoint add_v1 (i j : nat) : nat := + match i with + O => + j + | S i' => + S (add_v1 i' j) + end. + +Lemma fold_unfold_add_v1_O : + forall j : nat, + add_v1 O j = + j. +Proof. + fold_unfold_tactic add_v1. +Qed. + +Lemma fold_unfold_add_v1_S : + forall i' j : nat, + add_v1 (S i') j = + S (add_v1 i' j). +Proof. + fold_unfold_tactic add_v1. +Qed. + +Theorem add_v1_satisfies_the_recursive_specification_of_addition : + recursive_specification_of_addition add_v1. +Proof. + unfold recursive_specification_of_addition. + split. + + - exact fold_unfold_add_v1_O. + + - exact fold_unfold_add_v1_S. +Qed. + +(* ********** *) + +Definition specification_of_power (power : nat -> nat -> nat) := + (forall x : nat, + power x 0 = 1) + /\ + (forall (x : nat) + (n' : nat), + power x (S n') = x * power x n'). + +Definition test_power (candidate : nat -> nat -> nat) : bool := + (candidate 2 0 =? 1) && + (candidate 10 2 =? 10 * 10) && + (candidate 3 2 =? 3 * 3). + +Fixpoint power_v0 (x n : nat) : nat := + match n with + O => + 1 + | S n' => + x * power_v0 x n' + end. + +Compute (test_power power_v0). + +Lemma fold_unfold_power_v0_O : + forall x : nat, + power_v0 x O = + 1. +Proof. + fold_unfold_tactic power_v0. +Qed. + +Lemma fold_unfold_power_v0_S : + forall x n' : nat, + power_v0 x (S n') = + x * power_v0 x n'. +Proof. + fold_unfold_tactic power_v0. +Qed. + +(* ***** *) + +Fixpoint power_v1_aux (x n a : nat) : nat := + match n with + O => + a + | S n' => + power_v1_aux x n' (x * a) + end. + +Lemma fold_unfold_power_v1_aux_O : + forall x a : nat, + power_v1_aux x 0 a = + a. +Proof. + fold_unfold_tactic power_v1_aux. +Qed. + +Lemma fold_unfold_power_v1_aux_S : + forall x n' a : nat, + power_v1_aux x (S n') a = + power_v1_aux x n' (x * a). +Proof. + fold_unfold_tactic power_v1_aux. +Qed. + +Definition power_v1 (x n : nat) : nat := + power_v1_aux x n 1. + +Compute (test_power power_v1). + +Lemma power_v0_and_power_v1_are_equivalent_aux : + forall x n a : nat, + (power_v0 x n) * a = power_v1_aux x n a. +Proof. + intros x n. + induction n as [| n' IHx']. + - intro a. + rewrite -> (fold_unfold_power_v0_O x). + rewrite -> (fold_unfold_power_v1_aux_O x a). + exact (Nat.mul_1_l a). + - intro a. + rewrite -> (fold_unfold_power_v0_S x n'). + rewrite -> (fold_unfold_power_v1_aux_S x n' a). + rewrite <- (IHx' (x * a)). + rewrite -> (Nat.mul_comm x (power_v0 x n')). + symmetry. + exact (Nat.mul_assoc (power_v0 x n') x a). + +Qed. + +Theorem power_v0_and_power_v1_are_equivalent: + forall x n : nat, + power_v0 x n = power_v1 x n. +Proof. + intros x n. + unfold power_v1. + Check (power_v0_and_power_v1_are_equivalent_aux). + rewrite <- (Nat.mul_1_r (power_v0 x n)). + exact (power_v0_and_power_v1_are_equivalent_aux x n 1). +Qed. + + +(* ***** *) + +(* Eureka lemma: *) + +(* Lemma about_power_v0_and_power_v1_aux : *) +(* forall x n a : nat, *) +(* power_v0 x n * a = power_v1_aux x n a. *) +(* (* *) +(* power_v0 x n is x * x * ... * x n times *) + +(* power_v1_aux x n a is x * x * ... * x * a *) +(* *) *) +(* Proof. *) +(* intros x n. *) +(* induction n as [ | n' IHn']. *) +(* - intro a. *) +(* rewrite -> (fold_unfold_power_v0_O x). *) +(* rewrite -> (fold_unfold_power_v1_aux_O x a). *) +(* exact (Nat.mul_1_l a). *) +(* - intro a. *) +(* rewrite -> (fold_unfold_power_v0_S x n'). *) +(* rewrite -> (fold_unfold_power_v1_aux_S x n' a). *) +(* Check (IHn' (x * a)). *) +(* rewrite <- (IHn' (x * a)). *) +(* rewrite -> (Nat.mul_comm x (power_v0 x n')). *) +(* Check (Nat.mul_assoc). *) +(* symmetry. *) +(* exact (Nat.mul_assoc (power_v0 x n') x a). *) +(* Qed. *) + +(* Lemma that proves unnecessary: *) + +(* Lemma power_v0_and_power_v1_are_equivalent_aux : *) +(* forall x n : nat, *) +(* power_v0 x n = power_v1_aux x n 1. *) +(* Proof. *) +(* intros x n. *) +(* induction n as [ | n' IHn']. *) +(* - rewrite -> (fold_unfold_power_v0_O x). *) +(* rewrite -> (fold_unfold_power_v1_aux_O x 1). *) +(* reflexivity. *) +(* - rewrite -> (fold_unfold_power_v0_S x n'). *) +(* rewrite -> (fold_unfold_power_v1_aux_S x n' 1). *) +(* rewrite -> (Nat.mul_1_r x). *) +(* Check (about_power_v0_and_power_v1_aux x n' x). *) +(* rewrite <- (about_power_v0_and_power_v1_aux x n' x). *) +(* Check (Nat.mul_comm x (power_v0 x n')). *) +(* exact (Nat.mul_comm x (power_v0 x n')). *) +(* Qed. *) +(* + case n' as [ | n'']. + + rewrite -> (fold_unfold_power_v0_O x). + rewrite -> (fold_unfold_power_v1_aux_O x x). + exact (Nat.mul_1_r x). + + rewrite -> (fold_unfold_power_v0_S x n''). + rewrite -> (fold_unfold_power_v1_aux_S x n'' x). +*) + +(* Theorem power_v0_and_power_v1_are_equivalent : *) +(* forall x n : nat, *) +(* power_v0 x n = power_v1 x n. *) +(* Proof. *) +(* intros x n. *) +(* unfold power_v1. *) +(* Check (about_power_v0_and_power_v1_aux x n 1). *) +(* rewrite <- (Nat.mul_1_r (power_v0 x n)). *) +(* exact (about_power_v0_and_power_v1_aux x n 1). *) +(* Qed. *) + +(* ********** *) + +Fixpoint fib_v1 (n : nat) : nat := + match n with + 0 => + 0 + | S n' => + match n' with + 0 => + 1 + | S n'' => + fib_v1 n' + fib_v1 n'' + end + end. + +Lemma fold_unfold_fib_v1_O : + fib_v1 O = + 0. +Proof. + fold_unfold_tactic fib_v1. +Qed. + +Lemma fold_unfold_fib_v1_S : + forall n' : nat, + fib_v1 (S n') = + match n' with + 0 => + 1 + | S n'' => + fib_v1 n' + fib_v1 n'' + end. +Proof. + fold_unfold_tactic fib_v1. +Qed. + +Corollary fold_unfold_fib_v1_1 : + fib_v1 1 = + 1. +Proof. + rewrite -> (fold_unfold_fib_v1_S 0). + reflexivity. +Qed. + +Corollary fold_unfold_fib_v1_SS : + forall n'' : nat, + fib_v1 (S (S n'')) = + fib_v1 (S n'') + fib_v1 n''. +Proof. + intro n''. + rewrite -> (fold_unfold_fib_v1_S (S n'')). + reflexivity. +Qed. + +(* ********** *) + +Inductive binary_tree (V : Type) : Type := +| Leaf : V -> binary_tree V +| Node : binary_tree V -> binary_tree V -> binary_tree V. + +(* ***** *) + +Definition specification_of_mirror (mirror : forall V : Type, binary_tree V -> binary_tree V) : Prop := + (forall (V : Type) + (v : V), + mirror V (Leaf V v) = + Leaf V v) + /\ + (forall (V : Type) + (t1 t2 : binary_tree V), + mirror V (Node V t1 t2) = + Node V (mirror V t2) (mirror V t1)). + +(* ***** *) + +Fixpoint mirror (V : Type) (t : binary_tree V) : binary_tree V := + match t with + | Leaf _ v => Leaf V v + | Node _ t1 t2 => + Node V (mirror V t2) (mirror V t1) + end. + +Lemma fold_unfold_mirror_Leaf : + forall (V : Type) + (v : V), + mirror V (Leaf V v) = + Leaf V v. +Proof. + fold_unfold_tactic mirror. +Qed. + +Lemma fold_unfold_mirror_Node : + forall (V : Type) + (t1 t2 : binary_tree V), + mirror V (Node V t1 t2) = + Node V (mirror V t2) (mirror V t1). +Proof. + fold_unfold_tactic mirror. +Qed. + +(* ***** *) + +Proposition there_is_at_least_one_mirror_function : + specification_of_mirror mirror. +Proof. + unfold specification_of_mirror. + split. + - exact fold_unfold_mirror_Leaf. + - exact fold_unfold_mirror_Node. +Qed. + +(* ***** *) + +Theorem mirror_is_involutory : + forall (V : Type) + (t : binary_tree V), + mirror V (mirror V t) = t. +Proof. + intros V t. + induction t as [v | t1 IHt1 t2 IHt2]. + - rewrite -> (fold_unfold_mirror_Leaf V v). + exact (fold_unfold_mirror_Leaf V v). + - rewrite -> (fold_unfold_mirror_Node V t1 t2). + rewrite -> (fold_unfold_mirror_Node V (mirror V t2) (mirror V t1)). + rewrite -> IHt1. + rewrite -> IHt2. + reflexivity. +Qed. + +(* ********** *) + +(* Exercise 18 *) + +Require Import Bool. + +(* Inductive binary_tree (V : Type) : Type := *) +(* Leaf : V -> binary_tree V *) +(* | Node : binary_tree V -> binary_tree V -> binary_tree V. *) + +Definition test_mirrop (candidate : forall V : Type, (V -> V -> bool) -> binary_tree V -> binary_tree V -> bool) : bool := + (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Leaf nat 1)) true) + && + (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Leaf nat 2)) false) + && + (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Node nat (Leaf nat 2) (Leaf nat 3))) false) + && + (Bool.eqb (candidate nat Nat.eqb (Node nat (Leaf nat 1) (Leaf nat 2)) (Leaf nat 1)) false) + +. + +Fixpoint mirrorp (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : binary_tree V) : bool := + match t1 with + | Leaf _ v1 => + match t2 with + | Leaf _ v2 => eqb_V v1 v2 + | Node _ _ _ => false + end + | Node _ t11 t12 => + match t2 with + | Leaf _ _ => false + | Node _ t21 t22 => (mirrorp V eqb_V t11 t22) && (mirrorp V eqb_V t12 t21) + end + end. + +Compute (test_mirrop mirrorp). + +(* Taken from github.com/valiant-tCPA-learners/cs3234_week_04 *) +Definition improved_test_mirrop (candidate : forall V : Type, + (V -> V -> bool) -> binary_tree V -> binary_tree V -> bool) : bool := + (* Mirror over leaf nodes *) + (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Leaf nat 1)) true) + && + (Bool.eqb (candidate nat Nat.eqb (Leaf nat 1) (Leaf nat 2)) false) + && + (* Ensure that trees with non-equivalent structures are not considered mirrors*) + (Bool.eqb + (candidate nat Nat.eqb + (Leaf nat 1) + (Node nat (Leaf nat 2) (Leaf nat 3))) + false) + && + (Bool.eqb + (candidate nat Nat.eqb + (Node nat (Leaf nat 1) (Leaf nat 2)) + (Leaf nat 1)) + false) + && + (* Mirror over balanced trees of height 1 *) + (Bool.eqb + (candidate nat Nat.eqb + (Node nat (Leaf nat 1) (Leaf nat 2)) + (Node nat (Leaf nat 2) (Leaf nat 1))) + true) + && + (Bool.eqb + (candidate nat Nat.eqb + (Node nat (Leaf nat 1) (Leaf nat 2)) + (Node nat (Leaf nat 1) (Leaf nat 2))) + false) + && + (* Mirror over balanced trees of height 2 *) + (Bool.eqb + (candidate nat Nat.eqb + (Node nat + (Node nat (Leaf nat 1) (Leaf nat 2)) + (Node nat (Leaf nat 3) (Leaf nat 4))) + (Node nat + (Node nat (Leaf nat 4) (Leaf nat 3)) + (Node nat (Leaf nat 2) (Leaf nat 1)))) + true) + && + (Bool.eqb + (candidate nat Nat.eqb + (Node nat + (Node nat (Leaf nat 1) (Leaf nat 2)) + (Node nat (Leaf nat 3) (Leaf nat 4))) + (Node nat + (Node nat (Leaf nat 3) (Leaf nat 4)) + (Node nat (Leaf nat 1) (Leaf nat 2)))) + false). + +Compute (improved_test_mirrop mirrorp). + + +Lemma fold_unfold_mirrorp_Leaf : + forall (V : Type) (eqb_V: V -> V -> bool) (v1: V) (t2 : binary_tree V), + mirrorp V eqb_V (Leaf V v1) t2 = + match t2 with + | Leaf _ v2 => eqb_V v1 v2 + | Node _ _ _ => false + end. +Proof. + fold_unfold_tactic mirrorp. +Qed. + +Lemma fold_unfold_mirrorp_Node : + forall (V : Type) (eqb_V: V -> V -> bool) (t11 t12 t2 : binary_tree V), + mirrorp V eqb_V (Node V t11 t12) t2 = + match t2 with + | Leaf _ _ => false + | Node _ t21 t22 => (mirrorp V eqb_V t11 t22) && (mirrorp V eqb_V t12 t21) + end. +Proof. + fold_unfold_tactic mirrorp. +Qed. + + + +Proposition soundness_of_mirror_wrt_mirrorp : + forall (V : Type) + (eqb_V : V -> V -> bool), + (forall v v' : V, + v = v' -> + eqb_V v v' = true) -> + forall t1 t2 : binary_tree V, + mirror V t1 = t2 -> mirrorp V eqb_V t1 t2 = true. + Proof. + intros V eqb_V H_eqb_V t1. + induction t1 as [v1 | t11 IHt11 t12 IHt12]. + - intros t2 H_mirror. + rewrite -> (fold_unfold_mirrorp_Leaf V eqb_V v1 t2). + unfold mirror in H_mirror. + case t2 as [v2 | t21 t22]. + + injection H_mirror as H_v1_eq_v2. + apply (H_eqb_V v1 v2). + exact H_v1_eq_v2. + + discriminate H_mirror. + - intros t2 H_mirror. + rewrite -> (fold_unfold_mirrorp_Node V eqb_V t11 t12 t2). + case t2 as [v2 | t21 t22]. + + rewrite -> (fold_unfold_mirror_Node V t11 t12) in H_mirror. + discriminate H_mirror. + + rewrite -> (fold_unfold_mirror_Node V t11 t12) in H_mirror. + injection H_mirror as H_mirror_12 H_mirror_11. + Search (_ && _ = true). + rewrite -> (andb_true_iff (mirrorp V eqb_V t11 t22) (mirrorp V eqb_V t12 t21)). + split. + * apply (IHt11 t22). + exact H_mirror_11. + * apply (IHt12 t21). + exact H_mirror_12. + + (* * rewrite -> (IHt11 t22). *) + (* ** reflexivity. *) + (* * rewrite -> (IHt12 t21). *) + (* ** reflexivity. *) + (* ** exact H_mirror_12. *) + Qed. + + + +(* +Proposition completeness_of_mirror : + forall (V : Type) + (eqb_V : V -> V -> bool), + (forall v v' : V, + eqb_V v v' = true -> + v = v') -> + ... +*) + +(* ********** *) + +(* end of week-04_equational-reasoning.v *) diff --git a/cs3234/labs/week-04_more-about-soundness-and-completeness.v b/cs3234/labs/week-04_more-about-soundness-and-completeness.v new file mode 100644 index 0000000..5f25b82 --- /dev/null +++ b/cs3234/labs/week-04_more-about-soundness-and-completeness.v @@ -0,0 +1,363 @@ +(* week-04_more-about-soundness-and-completeness.v *) +(* LPP 2023 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 09 Feb 2024 *) + +(* ********** *) + +(* Paraphernalia: *) + +Require Import Arith. + +(* ********** *) + +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)). + +(* ********** *) + +Lemma about_a_recursive_addition : + forall add : nat -> nat -> nat, + recursive_specification_of_addition add -> + forall i j : nat, + add i j = i + j. +Proof. + intro add. + unfold recursive_specification_of_addition. + intros [S_add_O S_add_S] i. + induction i as [ | i' IHi']. + - intro j. + rewrite -> (Nat.add_0_l j). + exact (S_add_O j). + - intro j. + rewrite -> (S_add_S i' j). + Check (plus_Sn_m i' j). + rewrite -> (plus_Sn_m i' j). + rewrite -> (IHi' j). + reflexivity. +Qed. + +(* ********** *) + +Proposition soundness_of_recursive_addition : + forall add : nat -> nat -> nat, + recursive_specification_of_addition add -> + forall i j k : nat, + add i j = k -> + i + j = k. +Proof. + intros add S_add i j k H_k. + symmetry. + rewrite <- H_k. + exact (about_a_recursive_addition add S_add i j). +Qed. + +(* ********** *) + +Proposition completeness_of_recursive_addition : + forall add : nat -> nat -> nat, + recursive_specification_of_addition add -> + forall i j k : nat, + i + j = k -> + add i j = k. +Proof. + intros add S_add i j k H_k. + rewrite <- H_k. + exact (about_a_recursive_addition add S_add i j). +Qed. + +(* ********** *) + +Lemma about_decomposing_a_pair_using_the_injection_tactic : + forall i j : nat, + (i, j) = (0, 1) -> + i = 0 /\ j = 1. +Proof. + intros i j H_ij. + injection H_ij. + + Restart. + + intros i j H_ij. + injection H_ij as H_i H_j. + exact (conj H_i H_j). +Qed. + +Lemma about_decomposing_a_pair_using_the_injection_tactic' : + forall i j : nat, + (i, 1) = (0, j) -> + i = 0 /\ j = 1. +Proof. + intros i j H_ij. + injection H_ij as H_i H_j. + symmetry in H_j. + exact (conj H_i H_j). +Qed. + +Lemma about_decomposing_a_pair_of_pairs_using_the_injection_tactic : + forall a b c d: nat, + ((a, 1), (2, d)) = ((0, b), (c, 3)) -> + a = 0 /\ b = 1 /\ c = 2 /\ d = 3. +Proof. + intros a b c d H_abcd. + injection H_abcd as H_a H_b H_c H_d. + symmetry in H_b. + symmetry in H_c. + exact (conj H_a (conj H_b (conj H_c H_d))). +Qed. + +(* ********** *) + +Proposition true_is_not_false : + true <> false. +Proof. + unfold not. + intro H_absurd. + discriminate H_absurd. +Qed. + +(* ********** *) + +Proposition now_what : + (forall n : nat, n = S n) <-> 0 = 1. +Proof. + split. + + - intro H_n_Sn. + Check (H_n_Sn 0). + exact (H_n_Sn 0). + + - intro H_absurd. + discriminate H_absurd. + + Restart. + + split. + + - intro H_n_Sn. + Check (H_n_Sn 42). + discriminate (H_n_Sn 42). + + - intro H_absurd. + discriminate H_absurd. +Qed. + +Proposition what_now : + forall n : nat, + n = S n <-> 0 = 1. +Proof. + intro n. + split. + + - intro H_n. + Search (_ <> S _). + Check (n_Sn n). + assert (H_tmp := n_Sn n). + unfold not in H_tmp. + Check (H_tmp H_n). + contradiction (H_tmp H_n). + + - intro H_absurd. + discriminate H_absurd. +Qed. + +(* ********** *) + +Proposition soundness_of_recursive_addition_revisited : + forall add : nat -> nat -> nat, + recursive_specification_of_addition add -> + forall i j k : nat, + add i j = k -> + i + j = k. +Proof. + intro add. + unfold recursive_specification_of_addition. + intros [S_add_O S_add_S] i. + induction i as [ | i' IHi']. + - intros j k H_add. + rewrite -> (S_add_O j) in H_add. + rewrite -> H_add. + exact (Nat.add_0_l k). + - intros j k H_add. + rewrite -> (S_add_S i' j) in H_add. + case k as [ | k']. + + discriminate H_add. + + injection H_add as H_add. + Check (IHi' j k'). + Check (IHi' j k' H_add). + rewrite <- (IHi' j k' H_add). + Check plus_Sn_m. + exact (plus_Sn_m i' j). +Qed. + +(* ********** *) + +Proposition completeness_of_recursive_addition_revisited : + forall add : nat -> nat -> nat, + recursive_specification_of_addition add -> + forall i j k : nat, + i + j = k -> + add i j = k. +Proof. + intro add. + unfold recursive_specification_of_addition. + intros [S_add_O S_add_S] i j. + induction i as [ | i' IHi']. + - intros k H_k. + rewrite -> (Nat.add_0_l j) in H_k. + rewrite <- H_k. + exact (S_add_O j). + - intros k H_k. + rewrite -> (S_add_S i' j). + rewrite -> (plus_Sn_m i' j) in H_k. + case k as [ | k']. + + discriminate H_k. + + injection H_k as H_k. + Check (IHi' k'). + Check (IHi' k' H_k). + rewrite <- (IHi' k' H_k). + reflexivity. + + Restart. + + intro add. + unfold recursive_specification_of_addition. + intros [S_add_O S_add_S] i j. + induction i as [ | i' IHi']. + - intros k H_k. + rewrite -> (Nat.add_0_l j) in H_k. + rewrite <- H_k. + exact (S_add_O j). + - intros k H_k. + rewrite -> (S_add_S i' j). + rewrite -> (plus_Sn_m i' j) in H_k. + Check (IHi' (i' + j)). + Check (IHi' (i' + j) (eq_refl (i' + j))). + rewrite -> (IHi' (i' + j) (eq_refl (i' + j))). + exact H_k. +Qed. + +(* ********** *) + +Check Nat.add_assoc. + +Corollary associativity_of_recursive_addition : + forall add : nat -> nat -> nat, + recursive_specification_of_addition add -> + forall i j k : nat, + add i (add j k) = add (add i j) k. +Proof. + intros add S_add i j k. + rewrite -> (about_a_recursive_addition add S_add i (add j k)). + rewrite -> (about_a_recursive_addition add S_add j k). + rewrite -> (about_a_recursive_addition add S_add i j). + rewrite -> (about_a_recursive_addition add S_add (i + j) k). + exact (Nat.add_assoc i j k). + + Restart. + + intros add S_add i j k. + Check (soundness_of_recursive_addition add S_add i j (add i j) (eq_refl (add i j))). + rewrite <- (soundness_of_recursive_addition add S_add j k (add j k) (eq_refl (add j k))). + rewrite <- (soundness_of_recursive_addition add S_add i (j + k) (add i (j + k)) (eq_refl (add i (j + k)))). + Check (soundness_of_recursive_addition add S_add i j (add i j) (eq_refl (add i j))). + rewrite <- (soundness_of_recursive_addition add S_add i j (add i j) (eq_refl (add i j))). + Check (soundness_of_recursive_addition add S_add (i + j) k (add (i + j) k) (eq_refl (add (i + j) k))). + rewrite <- (soundness_of_recursive_addition add S_add (i + j) k (add (i + j) k) (eq_refl (add (i + j) k))). + exact (Nat.add_assoc i j k). +Qed. + +(* ********** *) + +Check Nat.add_comm. + +Lemma commutativity_of_recursive_addition : + forall add : nat -> nat -> nat, + recursive_specification_of_addition add -> + forall i j : nat, + add i j = add j i. +Proof. +Admitted. (* for the sake of the argument below *) + +Corollary commutativity_of_Nat_dot_add : + forall add : nat -> nat -> nat, + recursive_specification_of_addition add -> + forall i j : nat, + i + j = j + i. +Proof. + intros add S_add i j. + Check (about_a_recursive_addition add S_add i j). + rewrite <- (about_a_recursive_addition add S_add i j). + rewrite <- (about_a_recursive_addition add S_add j i). + Check (commutativity_of_recursive_addition add S_add i j). + exact (commutativity_of_recursive_addition add S_add i j). + + Restart. + + intros add S_add i j. + Check (completeness_of_recursive_addition add S_add i j (i + j) (eq_refl (i + j))). + rewrite <- (completeness_of_recursive_addition add S_add i j (i + j) (eq_refl (i + j))). + rewrite <- (completeness_of_recursive_addition add S_add j i (j + i) (eq_refl (j + i))). + exact (commutativity_of_recursive_addition add S_add i j). +Qed. + +(* ********** *) + +(* Exercise 07 *) + +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)). + +(* ***** *) + +Lemma about_a_tail_recursive_addition : + forall add : nat -> nat -> nat, + tail_recursive_specification_of_addition add -> + forall i j : nat, + add i j = i + j. +Proof. +Abort. + +(* ***** *) + +Proposition soundness_of_tail_recursive_addition : + forall add : nat -> nat -> nat, + tail_recursive_specification_of_addition add -> + forall i j k : nat, + add i j = k -> + i + j = k. +Proof. + (* first, as a corollary of about_a_tail_recursive_addition *) + + Restart. + + (* and second, by induction *) +Abort. + +(* ***** *) + +Proposition completeness_of_tail_recursive_addition : + forall add : nat -> nat -> nat, + tail_recursive_specification_of_addition add -> + forall i j k : nat, + i + j = k -> + add i j = k. +Proof. + (* first, as a corollary of about_a_tail_recursive_addition *) + + Restart. + + (* and second, by induction *) +Abort. + +(* ********** *) + +(* end of week-04_more-about-soundness-and-completeness.v *) diff --git a/cs3234/labs/week-04_proving-the-soundness-of-unit-tests.v b/cs3234/labs/week-04_proving-the-soundness-of-unit-tests.v new file mode 100644 index 0000000..df40c8f --- /dev/null +++ b/cs3234/labs/week-04_proving-the-soundness-of-unit-tests.v @@ -0,0 +1,167 @@ +(* week-04_proving-the-soundness-of-unit-tests.v *) +(* LPP 2024 - CS3234 2023-2024, Sem2 *) +(* Olivier Danvy *) +(* Version of 09 Feb 2024 *) + +(* ********** *) + +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)). + +(* ********** *) + +Check (Nat.eqb 1 2, 1 =? 2). + +Definition test_add (candidate : nat -> nat -> nat) := + (candidate 0 2 =? 2) && (candidate 2 0 =? 2) && (candidate 2 2 =? 4). + +(* ********** *) + +Theorem soundness_of_test_add_for_the_recursive_specification_of_addition : + forall add : nat -> nat -> nat, + recursive_specification_of_addition add -> + test_add add = true. +Proof. + intro add. + unfold recursive_specification_of_addition. + intros [H_add_O H_add_S]. + unfold test_add. + Check (H_add_O 2). + rewrite -> (H_add_O 2). + Search (_ =? _). + Check (beq_nat_refl 2). + rewrite <- (beq_nat_refl 2). + Search (true && _ = _). + Check (forall x y z : bool, x && (y && z) = (x && y) && z). + Check (andb_true_l (add 2 0 =? 2)). + rewrite -> (andb_true_l (add 2 0 =? 2)). + Check (H_add_S 1 0). + Check (H_add_S 1 2). + assert (H_add_2 : forall y : nat, add 2 y = S (S y)). + { intro y. + rewrite -> (H_add_S 1 y). + rewrite -> (H_add_S 0 y). + rewrite -> (H_add_O y). + reflexivity. } + Check (H_add_2 0). + rewrite -> (H_add_2 0). + rewrite <- (beq_nat_refl 2). + rewrite -> (andb_true_l (add 2 2 =? 4)). + rewrite -> (H_add_2 2). + rewrite <- (beq_nat_refl 4). + reflexivity. + + Restart. + + intro add. + unfold recursive_specification_of_addition. + intros [H_add_O H_add_S]. + unfold test_add. + rewrite -> (H_add_O 2). + assert (H_add_2 : forall y : nat, add 2 y = S (S y)). + { intro y. + rewrite -> (H_add_S 1 y). + rewrite -> (H_add_S 0 y). + rewrite -> (H_add_O y). + reflexivity. } + rewrite -> (H_add_2 0). + rewrite -> (H_add_2 2). + rewrite <- (beq_nat_refl 2). + rewrite -> (andb_true_l true). + rewrite -> (andb_true_l (4 =? 4)). + rewrite <- (beq_nat_refl 4). + reflexivity. + + Restart. + + intro add. + unfold recursive_specification_of_addition. + intros [H_add_O H_add_S]. + unfold test_add. + rewrite -> (H_add_O 2). + assert (H_add_2 : forall y : nat, add 2 y = S (S y)). + { intro y. + rewrite -> (H_add_S 1 y). + rewrite -> (H_add_S 0 y). + rewrite -> (H_add_O y). + reflexivity. } + rewrite -> (H_add_2 0). + rewrite -> (H_add_2 2). + compute. + reflexivity. + Restart. + + intro add. + unfold recursive_specification_of_addition. + intros [H_add_O H_add_S]. + unfold test_add. + compute. + (* Disaster city, that's what it is. *) + + Restart. + + intro add. + unfold recursive_specification_of_addition. + intros [H_add_O H_add_S]. + unfold test_add. + rewrite -> (H_add_O 2). + assert (H_add_2 : forall y : nat, add 2 y = S (S y)). + { intro y. + rewrite -> (H_add_S 1 y). + rewrite -> (H_add_S 0 y). + rewrite -> (H_add_O y). + reflexivity. } + rewrite -> (H_add_2 0). + rewrite -> (H_add_2 2). + unfold beq_nat. (* "e1 =? e2" is syntactic sugar for "beq_nat e1 e2" *) + unfold andb. (* "e1 && e2" is syntactic sugar for "andb e1 e2" *) + reflexivity. +Qed. + +(* ********** *) + +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 soundness_of_test_add_for_the_tail_recursive_specification_of_addition : + forall add : nat -> nat -> nat, + tail_recursive_specification_of_addition add -> + test_add add = true. +Proof. + intros add. + unfold tail_recursive_specification_of_addition. + intros [H_add_O H_add_S]. + unfold test_add. + rewrite -> (H_add_O 2). + + assert (H_add_2 : forall y : nat, add 2 y = S (S y)). + { intro y. + rewrite -> (H_add_S 1 y). + rewrite -> (H_add_S 0 (S y)). + rewrite -> (H_add_O (S (S y))). + reflexivity. + } + rewrite -> (H_add_2 0). + rewrite -> (H_add_2 2). + unfold beq_nat. + unfold andb. + reflexivity. +Qed. + +(* ********** *) + +(* end of week-04_proving-the-soundness-of-unit-tests.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 index ca0433b..7fd29b7 100644 --- a/cs3234/labs/week-04_specifications-that-depend-on-other-specifications.v +++ b/cs3234/labs/week-04_specifications-that-depend-on-other-specifications.v @@ -33,7 +33,13 @@ Theorem O_is_left_neutral_for_recursive_addition : recursive_specification_of_addition add -> forall n : nat, add 0 n = n. -Admitted. +Proof. + intros add. + unfold recursive_specification_of_addition. + intros [S_add_O S_add_S]. + exact (S_add_O). +Qed. + (* ********** *) @@ -79,6 +85,7 @@ Proof. Admitted. + Property O_is_left_absorbing_wrt_multiplication_alt : forall mul : nat -> nat -> nat, recursive_specification_of_multiplication mul -> @@ -190,6 +197,19 @@ Theorem addition_is_commutative : 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 : @@ -322,12 +342,60 @@ Proof. 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 -> @@ -344,7 +412,6 @@ Proof. 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. @@ -352,12 +419,49 @@ Proof. 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). - rewrite -> (IHx' y). - Check (multiplication_is_right_distributive_over_addition add S_add mul S_mul). + 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. + -Qed. (* <-- needed for later on *) (* ********** *)