feat: 3234 week 4

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 <danvy@yale-nus.edu.sg> *)
+(* 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 *)

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 <danvy@yale-nus.edu.sg> *)
+(* 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 *)

cs3234/labs/week-04_equational-reasoning.v

@@ -0,0 +1,533 @@
+(* week-04_equational-reasoning.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.
+
+(* ********** *)
+
+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 *)

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 <danvy@yale-nus.edu.sg> *)
+(* 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 *)

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 <danvy@yale-nus.edu.sg> *)
+(* 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 *)

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