diff --git a/cs3234/labs/midterm_project.v b/cs3234/labs/midterm_project.v
new file mode 100644
index 0000000..f7ce432
--- /dev/null
+++ b/cs3234/labs/midterm_project.v
@@ -0,0 +1,1773 @@
+(* midterm-project.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 22 Feb 2024 *)
+
+(* ********** *)
+
+(* A study of polymorphic lists. *)
+
+(* members of the group:
+   date: 
+
+   please upload one .v file and one .pdf file containing a project report
+
+   desiderata:
+   - the file should be readable, i.e., properly indented and using items or {...} for subgoals
+   - each use of a tactic should achieve one proof step
+   - all lemmas should be applied to all their arguments
+   - there should be no occurrences of admit, Admitted, and Abort
+*)
+
+(* ********** *)
+
+(* Paraphernalia: *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Arith Bool List.
+
+(* ********** *)
+
+Definition make_singleton_list (V : Type) (v : V) : list V :=
+  v :: nil.
+
+(* ********** *)
+
+Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
+  match ov1 with
+    Some v1 =>
+    match ov2 with
+      Some v2 =>
+      eqb_V v1 v2
+    | None =>
+      false
+    end
+  | None =>
+    match ov2 with
+      Some v2 =>
+      false
+    | None =>
+      true
+    end
+  end.
+
+(* ********** *)
+
+Fixpoint eqb_list (V : Type) (eqb_V : V -> V -> bool) (v1s v2s : list V) : bool :=
+  match v1s with
+    nil =>
+    match v2s with
+      nil =>
+      true
+    | v2 :: v2s' =>
+      false
+    end
+  | v1 :: v1s' =>
+    match v2s with
+      nil =>
+      false
+    | v2 :: v2s' =>
+      eqb_V v1 v2 && eqb_list V eqb_V v1s' v2s'
+    end
+  end.
+
+Lemma fold_unfold_eqb_list_nil :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool)
+         (v2s : list V),
+    eqb_list V eqb_V nil v2s =
+    match v2s with
+      nil =>
+      true
+    | v2 :: v2s' =>
+      false
+    end.
+Proof.
+  fold_unfold_tactic eqb_list.
+Qed.
+
+Lemma fold_unfold_eqb_list_cons :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool)
+         (v1 : V)
+         (v1s' v2s : list V),
+    eqb_list V eqb_V (v1 :: v1s') v2s =
+    match v2s with
+      nil =>
+      false
+    | v2 :: v2s' =>
+      eqb_V v1 v2 && eqb_list V eqb_V v1s' v2s'
+    end.
+Proof.
+  fold_unfold_tactic eqb_list.
+Qed.
+
+(* ***** *)
+
+(* Task 1: *)
+
+Theorem soundness_of_equality_over_lists :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        eqb_V v1 v2 = true -> v1 = v2) ->
+    forall v1s v2s : list V,
+      eqb_list V eqb_V v1s v2s = true ->
+      v1s = v2s.
+Proof.
+  intros V eqb_V S_eqb_V v1s.
+  induction v1s as [ | v1 v1s' IHv1s'].
+  - intros v2s H_eqb.
+    case v2s as [ | v2 v2s'].
+    + reflexivity.
+    + rewrite -> (fold_unfold_eqb_list_nil V eqb_V (v2 :: v2s')) in H_eqb.
+      discriminate H_eqb.
+  - intros v2s H_eqb.
+    case v2s as [ | v2 v2s'].
+    + rewrite -> (fold_unfold_eqb_list_cons V eqb_V v1 v1s' nil) in H_eqb.
+      discriminate H_eqb.
+    + rewrite -> (fold_unfold_eqb_list_cons V eqb_V v1 v1s' (v2 :: v2s')) in H_eqb.
+      rewrite -> (andb_true_iff (eqb_V v1 v2) (eqb_list V eqb_V v1s' v2s')) in H_eqb.
+      destruct H_eqb as [H_eqb_V H_eqb_list].
+      rewrite -> (IHv1s' v2s' H_eqb_list).
+      rewrite -> (S_eqb_V v1 v2 H_eqb_V).
+      reflexivity.
+Qed.
+
+Theorem completeness_of_equality_over_lists :
+  forall (V : Type)
+         (eqb_V : V -> V -> bool),
+    (forall v1 v2 : V,
+        v1 = v2 -> eqb_V v1 v2 = true) ->
+    forall v1s v2s : list V,
+      v1s = v2s ->
+      eqb_list V eqb_V v1s v2s = true.
+Proof.
+  intros V eqb_V S_eqb_V v1s.
+  induction v1s as [ | v1 v1s' IHv1s'].
+  - intros v2s H_eqb.
+    case v2s as [ | v2 v2s'].
+    + reflexivity.
+    + discriminate H_eqb.
+  - intros v2s H_eqb.
+    case v2s as [ | v2 v2s'].
+    + discriminate H_eqb.
+    + rewrite -> (fold_unfold_eqb_list_cons V eqb_V v1 v1s' (v2 :: v2s')).
+      rewrite -> andb_true_iff.
+      injection H_eqb as H_eqb_V H_eqb_list.
+      split.
+      * exact (S_eqb_V v1 v2 H_eqb_V).
+      * exact (IHv1s' v2s' H_eqb_list).
+Qed.
+
+(* ********** *)
+
+(* A study of the polymorphic length function: *)
+
+Definition specification_of_list_length (length : forall V : Type, list V -> nat) :=
+  (forall V : Type,
+      length V nil = 0)
+  /\
+  (forall (V : Type)
+          (v : V)
+          (vs' : list V),
+     length V (v :: vs') = S (length V vs')).
+
+(* Unit-test function: *)
+
+Definition test_list_length (candidate : forall V : Type, list V -> nat) :=
+  (candidate nat nil =? 0) &&
+  (candidate bool nil =? 0) &&
+  (candidate nat (1 :: nil) =? 1) &&
+  (candidate bool (true :: nil) =? 1) &&
+  (candidate nat (2 :: 1 :: nil) =? 2) &&
+  (candidate bool (false :: true :: nil) =? 2) &&
+  (candidate nat (3 :: 2 :: 1 :: nil) =? 3) &&
+  (candidate bool (false :: false :: true :: nil) =? 3).
+
+(* The specification specifies at most one length function: *)
+
+Theorem there_is_at_most_one_list_length_function :
+  forall (V : Type)
+         (list_length_1 list_length_2 : forall V : Type, list V -> nat),
+    specification_of_list_length list_length_1 ->
+    specification_of_list_length list_length_2 ->
+    forall vs : list V,
+      list_length_1 V vs = list_length_2 V vs.
+Proof.
+  intros V list_length_1 list_length_2.
+  unfold specification_of_list_length.
+  intros [S_list_length_1_nil S_list_length_1_cons]
+         [S_list_length_2_nil S_list_length_2_cons]
+         vs.
+  induction vs as [ | v vs' IHvs'].
+
+  - Check (S_list_length_2_nil V).
+    rewrite -> (S_list_length_2_nil V).
+    Check (S_list_length_1_nil V).
+    exact (S_list_length_1_nil V).
+
+  - Check (S_list_length_1_cons V v vs').
+    rewrite -> (S_list_length_1_cons V v vs').
+    rewrite -> (S_list_length_2_cons V v vs').
+    rewrite -> IHvs'.
+    reflexivity.
+Qed.
+
+(* Recursive implementation of the length function: *)
+
+Fixpoint list_length (V : Type) (vs : list V) : nat :=
+  match vs with
+    nil =>
+    0
+  | v :: vs' =>
+    S (list_length V vs')
+  end.
+
+Compute (test_list_length list_length).
+
+(* Associated fold-unfold lemmas: *)
+
+Lemma fold_unfold_list_length_nil :
+  forall V : Type,
+    list_length V nil =
+    0.
+Proof.
+  fold_unfold_tactic list_length.
+Qed.
+
+Lemma fold_unfold_list_length_cons :
+  forall (V : Type)
+         (v : V)
+         (vs' : list V),
+    list_length V (v :: vs') =
+    S (list_length V vs').
+Proof.
+  fold_unfold_tactic list_length.
+Qed.
+
+(* The specification specifies at least one length function: *)
+
+Theorem list_length_satisfies_the_specification_of_list_length :
+  specification_of_list_length list_length.
+Proof.
+  unfold specification_of_list_length.
+  exact (conj fold_unfold_list_length_nil fold_unfold_list_length_cons).
+Qed.
+
+(* ***** *)
+
+(* Task 2: *)
+
+(* Implement the length function using an accumulator. *)
+
+Fixpoint list_length_acc (V : Type) (vs : list V) (a : nat) : nat :=
+  match vs with
+    nil =>
+    a
+  | v :: vs' =>
+    list_length_acc V vs' (S a)
+  end.
+
+Definition list_length_alt (V : Type) (vs : list V) : nat :=
+  list_length_acc V vs 0.
+
+Compute (test_list_length list_length_alt).
+
+(* Associated fold-unfold lemmas: *)
+
+Lemma fold_unfold_list_length_acc_nil :
+  forall (V : Type)
+         (a : nat),
+    list_length_acc V nil a =
+    a.
+Proof.
+  fold_unfold_tactic list_length_acc.
+Qed.
+
+Lemma fold_unfold_list_length_acc_cons :
+  forall (V : Type)
+         (v : V)
+         (vs' : list V)
+         (a : nat),
+    list_length_acc V (v :: vs') a =
+    list_length_acc V vs' (S a).
+Proof.
+  fold_unfold_tactic list_length_acc.
+Qed.
+
+Lemma about_list_length_acc :
+  forall (V : Type)
+         (vs : list V)
+         (a : nat),
+    list_length_acc V vs (S a) = S (list_length_acc V vs a).
+Proof.
+  intros V vs.
+  induction vs as [ | v vs' IHvs'].
+  - intro a.
+    rewrite -> (fold_unfold_list_length_acc_nil V (S a)).
+    rewrite -> (fold_unfold_list_length_acc_nil V a).
+    reflexivity.
+  - intro a.
+    rewrite -> (fold_unfold_list_length_acc_cons V v vs' (S a)).
+    rewrite -> (fold_unfold_list_length_acc_cons V v vs' a).
+    exact (IHvs' (S a)).
+Qed.
+
+(* The specification specifies the alt length function too: *)
+
+Theorem list_length_alt_satisfies_the_specification_of_list_length :
+  specification_of_list_length list_length_alt.
+Proof.
+  unfold specification_of_list_length.
+  split.
+  - intro V.
+    unfold list_length_alt.
+    exact (fold_unfold_list_length_acc_nil V 0).
+  - intros V v vs'.
+    unfold list_length_alt.
+    rewrite <- (about_list_length_acc V vs' 0).
+    rewrite -> (fold_unfold_list_length_acc_cons V v vs' 0).
+    reflexivity.
+Qed.
+
+(* ********** *)
+
+(* A study of the polymorphic copy function: *)
+
+Definition specification_of_list_copy (copy : forall V : Type, list V -> list V) :=
+  (forall V : Type,
+      copy V nil = nil)
+  /\
+  (forall (V : Type)
+          (v : V)
+          (vs' : list V),
+     copy V (v :: vs') = v :: (copy V vs')).
+
+Definition test_list_copy (candidate : forall V : Type, list V -> list V) :=
+  (eqb_list nat Nat.eqb (candidate nat nil) nil) &&
+  (eqb_list bool Bool.eqb (candidate bool nil) nil) &&
+  (eqb_list nat Nat.eqb (candidate nat (1 :: nil)) (1 :: nil)) &&
+  (eqb_list bool Bool.eqb (candidate bool (true :: nil)) (true :: nil)) &&
+  (eqb_list nat Nat.eqb (candidate nat (2 :: 1 :: nil)) (2 :: 1 :: nil)) &&
+  (eqb_list bool Bool.eqb (candidate bool (false :: true :: nil)) (false :: true :: nil)).
+
+(* ***** *)
+
+(* Task 3: *)
+
+(*
+   a. Expand the unit-test function for copy with a few more tests.
+*)
+
+Definition test_list_copy_more (candidate : forall V : Type, list V -> list V) :=
+  (eqb_list (list nat) (eqb_list nat Nat.eqb) (candidate (list nat) (nil :: nil)) (nil :: nil)) &&
+  (eqb_list (list bool) (eqb_list bool Bool.eqb) (candidate (list bool) (nil :: nil)) (nil :: nil)) &&
+  (eqb_list (list nat) (eqb_list nat Nat.eqb) (candidate (list nat) ((1 :: 2 :: nil) :: nil)) ((1 :: 2 :: nil) :: nil)) &&
+  (eqb_list (list bool) (eqb_list bool Bool.eqb) (candidate (list bool) ((true :: nil) :: nil)) ((true :: nil) :: nil)).
+
+(*
+   b. Implement the copy function recursively.
+*)
+
+Fixpoint list_copy (V : Type) (vs : list V) : list V :=
+  match vs with
+    nil =>
+    nil
+  | v :: vs' =>
+    v :: (list_copy V vs')
+  end.
+
+Compute (test_list_copy list_copy).
+Compute (test_list_copy_more list_copy).
+
+(*
+   c. State its associated fold-unfold lemmas.
+*)
+
+Lemma fold_unfold_list_copy_nil :
+  forall (V : Type),
+    list_copy V nil =
+    nil.
+Proof.
+  fold_unfold_tactic list_copy.
+Qed.
+
+Lemma fold_unfold_list_copy_cons :
+  forall (V : Type)
+         (v : V)
+         (vs' : list V),
+    list_copy V (v :: vs') =
+    v :: (list_copy V vs').
+Proof.
+  fold_unfold_tactic list_copy.
+Qed.
+
+(*
+   d. Prove whether your implementation satisfies the specification.
+*)
+
+Theorem list_copy_satisfies_the_specification_of_list_copy :
+  specification_of_list_copy list_copy.
+Proof.
+  unfold specification_of_list_copy.
+  exact (conj fold_unfold_list_copy_nil fold_unfold_list_copy_cons).
+Qed.
+
+(*
+   e. Prove whether copy is idempotent.
+*)
+
+Proposition list_copy_is_idempotent :
+  forall (V : Type)
+         (vs : list V),
+    list_copy V (list_copy V vs) = list_copy V vs.
+Proof.
+  intros V vs.
+  induction vs as [ | v vs' IHvs'].
+  - rewrite -> (fold_unfold_list_copy_nil V).
+    rewrite -> (fold_unfold_list_copy_nil V).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_copy_cons V v vs').
+    rewrite -> (fold_unfold_list_copy_cons V v (list_copy V vs')).
+    rewrite -> IHvs'.
+    reflexivity.
+Qed.
+
+(*
+   f. Prove whether copying a list preserves its length.
+*)
+
+Proposition list_copy_preserves_list_length :
+  forall (V : Type)
+         (vs : list V),
+    list_length V (list_copy V vs) = list_length V vs.
+Proof.
+  intros V vs.
+  induction vs as [ | v vs' IHvs'].
+  - rewrite -> (fold_unfold_list_copy_nil V).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_copy_cons V v vs').
+    rewrite -> (fold_unfold_list_length_cons V v vs').
+    rewrite -> (fold_unfold_list_length_cons V v (list_copy V vs')).
+    rewrite -> IHvs'.
+    reflexivity.
+Qed.
+
+(*
+   g. Subsidiary question: can you think of a strikingly simple implementation of the copy function?
+      if so, pray show that it satisfies the specification of copy;
+      is it equivalent to your recursive implementation?
+*)
+
+Definition list_copy_simple (V : Type) (vs : list V) := vs.
+
+Theorem list_copy_simple_satisfies_the_specification_of_list_copy :
+  specification_of_list_copy list_copy_simple.
+Proof.
+  unfold specification_of_list_copy.
+  split.
+  - intro V.
+    unfold list_copy_simple.
+    reflexivity.
+  - intros V v vs'.
+    unfold list_copy_simple.
+    reflexivity.
+Qed.
+
+Proposition there_is_at_most_one_list_copy_function :
+  forall (V : Type)
+         (list_copy_1 list_copy_2 : forall V : Type, list V -> list V),
+         specification_of_list_copy list_copy_1 ->
+         specification_of_list_copy list_copy_2 ->
+         forall vs : list V,
+          list_copy_1 V vs = list_copy_2 V vs.
+Proof.
+  intros V list_copy_1 list_copy_2.
+  unfold specification_of_list_copy.
+  intros [S_list_copy_1_nil S_list_copy_1_cons]
+         [S_list_copy_2_nil S_list_copy_2_cons]
+         vs.
+  induction vs as [ | v vs' IHvs'].
+  - rewrite -> (S_list_copy_1_nil V).
+    rewrite -> (S_list_copy_2_nil V).
+    reflexivity.
+  - rewrite -> (S_list_copy_1_cons V v vs').
+    rewrite -> (S_list_copy_2_cons V v vs').
+    rewrite -> IHvs'.
+    reflexivity.
+Qed.
+
+(*
+   Since our list_copy_simple implementation satisfies the specification_of_list_copy, and we have
+   proven that there_is_at_most_one_list_copy_function, we can conclude that list_copy and
+   list_copy_simple are equivalent.
+*)
+
+(* ********** *)
+
+(* A study of the polymorphic append function: *)
+
+Definition specification_of_list_append (append : forall V : Type, list V -> list V -> list V) :=
+  (forall (V : Type)
+          (v2s : list V),
+      append V nil v2s = v2s)
+  /\
+  (forall (V : Type)
+          (v1 : V)
+          (v1s' v2s : list V),
+      append V (v1 :: v1s') v2s = v1 :: append V v1s' v2s).
+
+(* ***** *)
+
+(* Task 4: *)
+
+(*
+   a. Define a unit-test function for list_append.
+*)
+
+Definition test_list_append (candidate : forall V : Type, list V -> list V -> list V) :=
+  (eqb_list nat Nat.eqb (candidate nat nil nil) nil) &&
+  (eqb_list bool Bool.eqb (candidate bool nil nil) nil) &&
+  (eqb_list nat Nat.eqb (candidate nat (1 :: nil) nil) (1 :: nil)) &&
+  (eqb_list bool Bool.eqb (candidate bool (true :: nil) nil) (true :: nil)) &&
+  (eqb_list nat Nat.eqb (candidate nat (3 :: 2 :: nil) (1 :: nil)) (3 :: 2 :: 1 :: nil)) &&
+  (eqb_list bool Bool.eqb (candidate bool (false :: true :: nil) (false :: true :: nil)) (false :: true :: false :: true :: nil)) &&
+  (eqb_list (list nat) (eqb_list nat Nat.eqb) (candidate (list nat) ((1 :: nil) :: (2 :: nil) :: nil) ((3 :: 4 :: nil) :: nil)) ((1 :: nil) :: (2 :: nil) :: (3 :: 4 :: nil) :: nil)).
+
+(*
+   b. Implement the list_append function recursively.
+*)
+
+Fixpoint list_append (V : Type) (v1s v2s : list V) : list V :=
+  match v1s with
+    nil =>
+    v2s
+  | v1 :: v1s' =>
+    v1 :: (list_append V v1s' v2s)
+  end.
+
+Compute (test_list_append list_append).
+
+(*
+   c. State its associated fold-unfold lemmas.
+*)
+
+Lemma fold_unfold_list_append_nil :
+  forall (V : Type)
+         (v2s : list V),
+    list_append V nil v2s =
+    v2s.
+Proof.
+  fold_unfold_tactic list_append.
+Qed.
+
+Lemma fold_unfold_list_append_cons :
+  forall (V : Type)
+         (v1 : V)
+         (v1s' v2s : list V),
+    list_append V (v1 :: v1s') v2s =
+    v1 :: (list_append V v1s' v2s).
+Proof.
+  fold_unfold_tactic list_append.
+Qed.
+
+(*
+   d. Prove that your implementation satisfies the specification.
+*)
+
+Theorem list_append_satisfies_the_specification_of_list_append :
+  specification_of_list_append list_append.
+Proof.
+  unfold specification_of_list_append.
+  exact (conj fold_unfold_list_append_nil fold_unfold_list_append_cons).
+Qed.
+
+(*
+   e. Prove whether nil is neutral on the left of list_append.
+*)
+
+Property nil_is_left_neutral_wrt_list_append :
+  forall (V : Type)
+         (v2s : list V),
+    list_append V nil v2s = v2s.
+Proof.
+  exact fold_unfold_list_append_nil.
+Qed.
+
+(*
+   f. Prove whether nil is neutral on the right of list_append.
+*)
+
+Property nil_is_right_neutral_wrt_list_append :
+  forall (V : Type)
+         (v1s : list V),
+    list_append V v1s nil = v1s.
+Proof.
+  intros V v1s.
+  induction v1s as [ | v1' v1s' IHv1s' ].
+  - exact (fold_unfold_list_append_nil V nil).
+  - rewrite -> (fold_unfold_list_append_cons V v1' v1s' nil).
+    rewrite -> IHv1s'.
+    reflexivity.
+Qed.
+
+(*
+   g. Prove whether list_append is commutative.
+*)
+
+Property list_append_is_not_commutative :
+  exists (V : Type)
+         (v1s v2s : list V),
+    list_append V v1s v2s <> list_append V v2s v1s.
+Proof.
+  exists nat.
+  exists (0 :: nil).
+  exists (1 :: nil).
+  rewrite -> (fold_unfold_list_append_cons nat 0 nil).
+  rewrite -> (fold_unfold_list_append_nil nat (1 :: nil)).
+  rewrite -> (fold_unfold_list_append_cons nat 1 nil).
+  rewrite -> (fold_unfold_list_append_nil nat (0 :: nil)).
+  unfold not.
+  intro H_absurd.
+  discriminate H_absurd.
+Qed.
+
+(*
+   h. Prove whether list_append is associative.
+*)
+
+Property list_append_is_associative :
+  forall (V : Type)
+         (v1s v2s v3s : list V),
+    list_append V v1s (list_append V v2s v3s) = list_append V (list_append V v1s v2s) v3s.
+Proof.
+  intros V v1s.
+  induction v1s as [ | v1' v1s' IHv1s' ].
+  - intros v2s v3s.
+    rewrite -> (fold_unfold_list_append_nil V (list_append V v2s v3s)).
+    rewrite -> (fold_unfold_list_append_nil V v2s).
+    reflexivity.
+  - intros v2s v3s.
+    rewrite -> (fold_unfold_list_append_cons V v1' v1s' (list_append V v2s v3s)).
+    rewrite -> IHv1s'.
+    rewrite -> (fold_unfold_list_append_cons V v1' v1s' v2s).
+    rewrite -> (fold_unfold_list_append_cons V v1' (list_append V v1s' v2s)).
+    reflexivity.
+Qed.
+
+(*
+   i. Prove whether appending two lists preserves their length.
+*)
+
+Proposition list_append_and_list_length_commute_with_each_other :
+  forall (V : Type)
+         (v1s v2s : list V),
+    list_length V (list_append V v1s v2s) = list_length V v1s + list_length V v2s.
+Proof.
+  intros V v1s.
+  induction v1s as [ | v1' v1s' IHv1s' ].
+  - intros v2s.
+    rewrite -> (fold_unfold_list_append_nil V v2s).
+    rewrite -> (fold_unfold_list_length_nil V).
+    rewrite -> (Nat.add_0_l (list_length V v2s)).
+    reflexivity.
+  - intros v2s.
+    rewrite -> (fold_unfold_list_append_cons V v1' v1s' v2s).
+    rewrite-> (fold_unfold_list_length_cons V v1' (list_append V v1s' v2s)).
+    rewrite -> (IHv1s' v2s).
+    rewrite -> (fold_unfold_list_length_cons V v1' v1s').
+    Search (S _ + _ = S (_ + _)).
+    rewrite -> (plus_Sn_m (list_length V v1s') (list_length V v2s)).
+    reflexivity.
+Qed.
+
+(*
+   j. Prove whether list_append and list_copy commute with each other.
+*)
+
+Proposition list_append_and_list_copy_commute_with_each_other :
+  forall (V : Type)
+         (v1s v2s : list V),
+    list_copy V (list_append V v1s v2s) = list_append V (list_copy V v1s) (list_copy V v2s).
+Proof.
+  intros V v1s.
+  induction v1s as [ | v1' v1s' IHv1s' ].
+  - intros v2s.
+    rewrite -> (fold_unfold_list_append_nil V v2s).
+    rewrite -> (fold_unfold_list_copy_nil V).
+    rewrite -> (fold_unfold_list_append_nil V (list_copy V v2s)).
+    reflexivity.
+  - intros v2s.
+    rewrite -> (fold_unfold_list_append_cons V v1' v1s' v2s).
+    rewrite -> (fold_unfold_list_copy_cons V v1' (list_append V v1s' v2s)).
+    rewrite -> (IHv1s' v2s).
+    rewrite -> (fold_unfold_list_copy_cons V v1' v1s').
+    rewrite -> (fold_unfold_list_append_cons V v1' (list_copy V v1s') (list_copy V v2s)).
+    reflexivity.
+
+Qed.
+
+(* ********** *)
+
+(* A study of the polymorphic reverse function: *)
+
+Definition specification_of_list_reverse (reverse : forall V : Type, list V -> list V) :=
+  forall append : forall W : Type, list W -> list W -> list W,
+    specification_of_list_append append ->
+    (forall V : Type,
+        reverse V nil = nil)
+    /\
+    (forall (V : Type)
+            (v : V)
+            (vs' : list V),
+        reverse V (v :: vs') = append V (reverse V vs') (v :: nil)).
+
+(* ***** *)
+
+(* Task 5: *)
+
+(*
+   a. Define a unit-test function for an implementation of the reverse function.
+*)
+
+Definition test_list_reverse (candidate : forall V : Type, list V -> list V) :=
+  (eqb_list nat Nat.eqb (candidate nat nil) nil) &&
+  (eqb_list bool Bool.eqb (candidate bool nil) nil) &&
+  (eqb_list nat Nat.eqb (candidate nat (1 :: nil)) (1 :: nil)) &&
+  (eqb_list bool Bool.eqb (candidate bool (true :: nil)) (true :: nil)) &&
+  (eqb_list nat Nat.eqb (candidate nat (2 :: 1 :: nil)) (1 :: 2 :: nil)) &&
+  (eqb_list bool Bool.eqb (candidate bool (false :: true :: nil)) (true :: false :: nil)) &&
+  (eqb_list nat Nat.eqb (candidate nat (3 :: 2 :: 1 :: nil)) (1 :: 2 :: 3 :: nil)) &&
+  (eqb_list bool Bool.eqb (candidate bool (true :: false :: true :: nil)) (true :: false :: true :: nil)) &&
+  (eqb_list (list nat) (eqb_list nat Nat.eqb) (candidate (list nat) ((1 :: 2 :: nil) :: (2 :: 3 :: nil) :: nil)) ((2 :: 3 :: nil) :: (1 :: 2 :: nil) :: nil)) &&
+  (eqb_list (list bool) (eqb_list bool Bool.eqb) (candidate (list bool) ((true :: false :: nil) :: (true :: nil) :: nil)) ((true :: nil) :: (true :: false :: nil) :: nil)).
+
+(*
+   b. Implement the reverse function recursively, using list_append.
+*)
+
+Fixpoint list_reverse (V : Type) (vs : list V) : list V :=
+  match vs with
+    nil =>
+    nil
+  | v :: vs' =>
+    list_append V (list_reverse V vs') (v :: nil)
+  end.
+
+Compute (test_list_reverse list_reverse).
+
+(*
+   c. State the associated fold-unfold lemmas.
+*)
+
+Lemma fold_unfold_list_reverse_nil :
+  forall (V : Type),
+    list_reverse V nil =
+    nil.
+Proof.
+  fold_unfold_tactic list_reverse.
+Qed.
+
+Lemma fold_unfold_list_reverse_cons :
+  forall (V : Type)
+         (v : V)
+         (vs' : list V),
+    list_reverse V (v :: vs') =
+    list_append V (list_reverse V vs') (v :: nil).
+Proof.
+  fold_unfold_tactic list_reverse.
+Qed.
+
+(*
+   d. Prove whether your implementation satisfies the specification.
+*)
+
+Theorem there_is_at_most_one_list_append_function :
+  forall (V : Type)
+    (f g : forall V : Type, list V -> list V -> list V),
+    specification_of_list_append f ->
+    specification_of_list_append g ->
+    forall v1s v2s : list V,
+      f V v1s v2s = g V v1s v2s.
+Proof.
+  intros V f g.
+  unfold specification_of_list_append.
+  intros [S_list_append_1_nil S_list_append_1_cons].
+  intros [S_list_append_2_nil S_list_append_2_cons].
+  intros v1s v2s.
+
+  induction v1s as [ | v1' v1s' IHv1s' ].
+  - rewrite -> (S_list_append_2_nil V v2s).
+    exact (S_list_append_1_nil V v2s).
+  - rewrite -> (S_list_append_2_cons V v1' v1s' v2s).
+    rewrite -> (S_list_append_1_cons V v1' v1s' v2s).
+    rewrite -> IHv1s'.
+    reflexivity.
+  Qed.
+
+Theorem list_reverse_satisfies_the_specification_of_list_reverse :
+  specification_of_list_reverse list_reverse.
+Proof.
+  unfold specification_of_list_reverse.
+  intros append S_append.
+  split.
+  - exact fold_unfold_list_reverse_nil.
+  - intros V v vs'.
+    rewrite -> (fold_unfold_list_reverse_cons V v vs').
+    rewrite -> (there_is_at_most_one_list_append_function V list_append append
+             list_append_satisfies_the_specification_of_list_append
+             S_append
+             (list_reverse V vs')
+             (v :: nil)
+          ).
+    reflexivity.
+Qed.
+
+(*
+   e. Prove whether list_reverse is involutory.
+*)
+
+
+Lemma about_list_reverse_and_list_append :
+  forall (V: Type)
+    (v : V)
+    (vs : list V),
+    list_reverse V (list_append V vs (v :: nil)) = v :: (list_reverse V vs).
+Proof.
+  intros V v vs.
+  induction vs as [ | v' vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_append_nil V (v :: nil)).
+    rewrite -> (fold_unfold_list_reverse_cons V v nil).
+    rewrite -> (fold_unfold_list_reverse_nil V).
+    rewrite -> (fold_unfold_list_append_nil V (v :: nil)).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_append_cons V v' vs' (v :: nil)).
+    rewrite -> (fold_unfold_list_reverse_cons V v' (list_append V vs' (v :: nil))).
+    rewrite -> IHvs'.
+    rewrite -> (fold_unfold_list_append_cons V v (list_reverse V vs') (v' :: nil)).
+    rewrite -> (fold_unfold_list_reverse_cons V v' vs').
+    reflexivity.
+  Qed.
+
+Proposition list_reverse_is_involutory :
+  forall (V : Type)
+         (vs : list V),
+    list_reverse V (list_reverse V vs) = vs.
+Proof.
+  intros V vs.
+  induction vs as [ | v' vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_reverse_nil V).
+    rewrite -> (fold_unfold_list_reverse_nil V).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_reverse_cons V v' vs').
+    rewrite -> (about_list_reverse_and_list_append V v' (list_reverse V vs')).
+    rewrite -> IHvs'.
+    reflexivity.
+Qed.
+
+(*
+   f. Prove whether reversing a list preserves its length.
+*)
+
+Proposition list_reverse_and_list_length_commute_with_each_other :
+  forall (V : Type)
+         (vs : list V),
+    list_length V (list_reverse V vs) = list_length V vs.
+Proof.
+  intros V vs.
+  induction vs as [ | v' vs' IHvs' ].
+  - rewrite -> (fold_unfold_list_reverse_nil V).
+    reflexivity.
+  - rewrite -> (fold_unfold_list_reverse_cons V v' vs').
+    Search list_append.
+    rewrite -> (list_append_and_list_length_commute_with_each_other V (list_reverse V vs') (v' :: nil)).
+    rewrite -> (fold_unfold_list_length_cons V v' nil).
+    rewrite -> (fold_unfold_list_length_nil V).
+    rewrite -> IHvs'.
+    rewrite -> (fold_unfold_list_length_cons V v' vs').
+
+    Search (_ + S _ = S _).
+    rewrite -> (Nat.add_1_r (list_length V vs')).
+    reflexivity.
+Qed.
+
+(*
+   g. Do list_append and list_reverse commute with each other (hint: yes they do) and if so how?
+*)
+Proposition list_reverse_and_list_append_commute_with_each_other :
+  forall (V : Type)
+         (v1s v2s : list V),
+    list_append V (list_reverse V v2s) (list_reverse V v1s) = list_reverse V (list_append V v1s v2s).
+Proof.
+  intros V v1s.
+  induction v1s as [ | v1' v1s' IHv1s'].
+  - intros v2s.
+    rewrite -> (fold_unfold_list_reverse_nil V).
+    rewrite -> (nil_is_left_neutral_wrt_list_append V v2s).
+    rewrite -> (nil_is_right_neutral_wrt_list_append V (list_reverse V v2s)).
+    reflexivity.
+  - intros v2s.
+    rewrite -> (fold_unfold_list_reverse_cons V v1' v1s').
+    rewrite -> (fold_unfold_list_append_cons V v1' v1s' v2s).
+    rewrite -> (fold_unfold_list_reverse_cons V v1' (list_append V v1s' v2s)).
+    rewrite -> (list_append_is_associative V (list_reverse V v2s) (list_reverse V v1s') (v1' :: nil)).
+    rewrite -> (IHv1s' ).
+    reflexivity.
+  Qed.
+(*
+   h. Implement the reverse function using an accumulator instead of using list_append.
+*)
+
+(*
+Definition list_reverse_alt (V : Type) (vs : list V) : list V :=
+...
+*)
+
+(*
+   i. Revisit the propositions above (involution, preservation of length, commutation with append)
+      and prove whether reverse_v1 satisfies them.
+      Two proof strategies are possible:
+      (1) self-contained proofs with Eureka lemmas, and
+      (2) proofs that hinge on the equivalence of list_reverse_alt and list_reverse.
+      This subtask is very instructive, but optional.
+*)
+
+(* ********** *)
+
+(* A study of the polymorphic map function: *)
+
+Definition specification_of_list_map (map : forall V W : Type, (V -> W) -> list V -> list W) :=
+  (forall (V W : Type)
+          (f : V -> W),
+      map V W f nil = nil)
+  /\
+  (forall (V W : Type)
+          (f : V -> W)
+          (v : V)
+          (vs' : list V),
+      map V W f (v :: vs') = f v :: map V W f vs').
+
+(* ***** *)
+
+(* Task 6:
+
+   a. Prove whether the specification specifies at most one map function.
+*)
+
+Proposition there_is_at_most_one_list_map_function :
+  forall list_map1 list_map2 : forall V W : Type, (V -> W) -> list V -> list W,
+      specification_of_list_map list_map1 ->
+      specification_of_list_map list_map2 ->
+      forall (V W : Type)
+             (f : V -> W)
+             (vs : list V),
+        list_map1 V W f vs = list_map2 V W f vs.
+Proof.
+Abort.
+
+(*
+   b. Implement the map function recursively.
+*)
+
+Fixpoint list_map (V W : Type) (f : V -> W) (vs : list V) : list W :=
+  match vs with
+    nil =>
+    nil
+  | v :: vs' =>
+    f v :: list_map V W f vs'
+  end.
+
+(*
+   c. State the associated fold-unfold lemmas.
+*)
+
+Lemma fold_unfold_list_map_nil :
+  forall (V W : Type)
+         (f : V -> W),
+    list_map V W f nil =
+    nil.
+Proof.
+  fold_unfold_tactic list_map.
+Qed.
+
+Lemma fold_unfold_list_map_cons :
+  forall (V W : Type)
+         (f : V -> W)
+         (v : V)
+         (vs' : list V),
+    list_map V W f (v :: vs') =
+    f v :: list_map V W f vs'.
+Proof.
+  fold_unfold_tactic list_map.
+Qed.
+
+(*
+   d. Prove whether your implementation satisfies the specification.
+*)
+
+Proposition list_map_satisfies_the_specification_of_list_map :
+  specification_of_list_map list_map.
+Proof.
+  unfold specification_of_list_map.
+  exact (conj fold_unfold_list_map_nil fold_unfold_list_map_cons).
+Qed.
+
+(*
+   e. Implement the copy function as an instance of list_map.
+*)
+
+(*
+Definition list_copy_as_list_map (V : Type) (vs : list V) : list V :=
+  ...
+*)
+
+(*
+Hint: Does list_copy_as_list_map satisfy the specification of list_copy?
+*)
+
+(*
+   f. Prove whether mapping a function over a list preserves the length of this list.
+*)
+
+(*
+   g. Do list_map and list_append commute with each other and if so how?
+*)
+
+(*
+   h. Do list_map and list_reverse commute with each other and if so how?
+*)
+
+(*
+   i. Do list_map and list_reverse_alt commute with each other and if so how?
+*)
+
+(*
+   j. Define a unit-test function for the map function
+      and verify that your implementation satisfies it.
+*)
+
+(* ********** *)
+
+(* A study of the polymorphic fold-right and fold-left functions: *)
+
+Definition specification_of_list_fold_right (fold_right : forall V W : Type, W -> (V -> W -> W) -> list V -> W) :=
+  (forall (V W : Type)
+          (nil_case : W)
+          (cons_case : V -> W -> W),
+     fold_right V W nil_case cons_case nil =
+     nil_case)
+  /\
+  (forall (V W : Type)
+          (nil_case : W)
+          (cons_case : V -> W -> W)
+          (v : V)
+          (vs' : list V),
+     fold_right V W nil_case cons_case (v :: vs') =
+     cons_case v (fold_right V W nil_case cons_case vs')).
+
+Definition specification_of_list_fold_left (fold_left : forall V W : Type, W -> (V -> W -> W) -> list V -> W) :=
+  (forall (V W : Type)
+          (nil_case : W)
+          (cons_case : V -> W -> W),
+     fold_left V W nil_case cons_case nil =
+     nil_case)
+  /\
+  (forall (V W : Type)
+          (nil_case : W)
+          (cons_case : V -> W -> W)
+          (v : V)
+          (vs' : list V),
+     fold_left V W nil_case cons_case (v :: vs') =
+     fold_left V W (cons_case v nil_case) cons_case vs').
+
+(* ***** *)
+
+(* Task 7:
+
+   a. Implement the fold-right function recursively.
+*)
+
+Fixpoint list_fold_right (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
+  match vs with
+    nil =>
+    nil_case
+  | v :: vs' =>
+    cons_case v (list_fold_right V W nil_case cons_case vs')
+  end.
+
+(*
+   b. Implement the fold-left function recursively.
+*)
+
+Fixpoint list_fold_left (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
+  match vs with
+    nil =>
+    nil_case
+  | v :: vs' =>
+    list_fold_left V W (cons_case v nil_case) cons_case vs'
+  end.
+
+(*
+   c. state the fold-unfold lemmas associated to list_fold_right and to list_fold_left
+*)
+
+Lemma fold_unfold_list_fold_right_nil :
+  forall (V W : Type)
+         (nil_case : W)
+         (cons_case : V -> W -> W),
+    list_fold_right V W nil_case cons_case nil =
+    nil_case.
+Proof.
+  fold_unfold_tactic list_fold_right.
+Qed.
+
+Lemma fold_unfold_list_fold_right_cons :
+  forall (V W : Type)
+         (nil_case : W)
+         (cons_case : V -> W -> W)
+         (v : V)
+         (vs' : list V),
+    list_fold_right V W nil_case cons_case (v :: vs') =
+    cons_case v (list_fold_right V W nil_case cons_case vs').
+Proof.
+  fold_unfold_tactic list_fold_right.
+Qed.
+
+Lemma fold_unfold_list_fold_left_nil :
+  forall (V W : Type)
+         (nil_case : W)
+         (cons_case : V -> W -> W),
+    list_fold_left V W nil_case cons_case nil =
+    nil_case.
+Proof.
+  fold_unfold_tactic list_fold_left.
+Qed.
+
+Lemma fold_unfold_list_fold_left_cons :
+  forall (V W : Type)
+         (nil_case : W)
+         (cons_case : V -> W -> W)
+         (v : V)
+         (vs' : list V),
+    list_fold_left V W nil_case cons_case (v :: vs') =
+    list_fold_left V W (cons_case v nil_case) cons_case vs'.
+Proof.
+  fold_unfold_tactic list_fold_left.
+Qed.
+
+(*
+   d. Prove that each of your implementations satisfies the corresponding specification.
+*)
+
+(*
+   e. Which function do foo and bar (defined just below) compute?
+*)
+
+(*
+Definition foo (V : Type) (vs : list V) :=
+  list_fold_right V (list V) nil (fun v vs => v :: vs) vs.
+*)
+
+(*
+Definition bar (V : Type) (vs : list V) :=
+  list_fold_left V (list V) nil (fun v vs => v :: vs) vs.
+*)
+
+(*
+   f. Implement the length function either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice.
+*)
+
+(*
+   g. Implement the copy function either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice.
+*)
+
+(*
+   h. Implement the append function either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice.
+*)
+
+(*
+   i. Implement the reverse function either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice.
+*)
+
+(*
+   j. Implement the map function either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice.
+*)
+
+(*
+   k. Implement eqb_list either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice.
+*)
+
+(*
+   l. Implement list_fold_right as an instance of list_fold_left, using list_reverse.
+*)
+
+(*
+   m. Implement list_fold_left as an instance of list_fold_right, using list_reverse.
+*)
+
+(*
+   n. Implement list_fold_right as an instance of list_fold_left, without using list_reverse.
+*)
+
+(*
+Definition list_fold_right_left (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
+  ...
+*)
+
+(*
+   o. Implement list_fold_left as an instance of list_fold_right, without using list_reverse.
+*)
+
+(*
+Definition list_fold_left_right (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
+  ...
+*)
+
+(*
+   p. Show that
+      if the cons case is a function that is left permutative (defined just below),
+      applying list_fold_left and applying list_fold_right
+      to a nil case, this cons case, and a list
+      give the same result
+*)
+  
+Definition is_left_permutative (V W : Type) (op2 : V -> W -> W) :=
+  forall (v1 v2 : V)
+         (w : W),
+    op2 v1 (op2 v2 w) = op2 v2 (op2 v1 w).
+
+(*
+Theorem folding_left_and_right_over_lists :
+  forall (V W : Type)
+         (cons_case : V -> W -> W),
+    is_left_permutative V W cons_case ->
+    forall (nil_case : W)
+           (vs : list V),
+      list_fold_left  V W nil_case cons_case vs =
+      list_fold_right V W nil_case cons_case vs.
+Proof.
+Abort.
+*)
+
+(*
+   q. Can you think of corollaries of this property?
+*)
+
+Lemma plus_is_left_permutative :
+  is_left_permutative nat nat plus.
+Proof.
+Abort.
+
+(*
+Corollary example_for_plus :
+  forall ns : list nat,
+    list_fold_left nat nat 0 plus ns = list_fold_right nat nat 0 plus ns.
+Proof.
+  Check (folding_left_and_right_over_lists nat nat plus plus_is_left_permutative 0).
+  exact (folding_left_and_right_over_lists nat nat plus plus_is_left_permutative 0).
+Qed.
+*)
+
+(* What do you make of this corollary?
+   Can you think of more such corollaries?
+*)
+
+(*
+   r. Subsidiary question: does the converse of Theorem folding_left_and_right_over_lists hold?
+*)
+
+(*
+Theorem folding_left_and_right_over_lists_converse :
+  forall (V W : Type)
+         (cons_case : V -> W -> W),
+    (forall (nil_case : W)
+            (vs : list V),
+        list_fold_left  V W nil_case cons_case vs =
+        list_fold_right V W nil_case cons_case vs) ->
+    is_left_permutative V W cons_case.
+Proof.
+Abort.
+*)
+
+(* ********** *)
+
+(* Task 8: *)
+
+Fixpoint nat_fold_right (V : Type) (zero_case : V) (succ_case : V -> V) (n : nat) : V :=
+  match n with
+    O =>
+    zero_case
+  | S n' =>
+    succ_case (nat_fold_right V zero_case succ_case n')
+  end.
+
+Lemma fold_unfold_nat_fold_right_O :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : V -> V),
+    nat_fold_right V zero_case succ_case O =
+    zero_case.
+Proof.
+  fold_unfold_tactic nat_fold_right.
+Qed.
+
+Lemma fold_unfold_nat_fold_right_S :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : V -> V)
+         (n' : nat),
+    nat_fold_right V zero_case succ_case (S n') =
+    succ_case (nat_fold_right V zero_case succ_case n').
+Proof.
+  fold_unfold_tactic nat_fold_right.
+Qed.
+
+Fixpoint nat_fold_left (V : Type) (zero_case : V) (succ_case : V -> V) (n : nat) : V :=
+  match n with
+    O =>
+    zero_case
+  | S n' =>
+    nat_fold_left V (succ_case zero_case) succ_case n'
+  end.
+
+Lemma fold_unfold_nat_fold_left_O :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : V -> V),
+    nat_fold_left V zero_case succ_case O =
+    zero_case.
+Proof.
+  fold_unfold_tactic nat_fold_left.
+Qed.
+
+Lemma fold_unfold_nat_fold_left_S :
+  forall (V : Type)
+         (zero_case : V)
+         (succ_case : V -> V)
+         (n' : nat),
+    nat_fold_left V zero_case succ_case (S n') =
+    nat_fold_left V (succ_case zero_case) succ_case n'.
+Proof.
+  fold_unfold_tactic nat_fold_left.
+Qed.
+
+(* ***** *)
+
+(* The addition function: *)
+
+Definition recursive_specification_of_addition (add : nat -> nat -> nat) :=
+  (forall y : nat,
+      add O y = y)
+  /\
+  (forall x' y : nat,
+      add (S x') y = S (add x' y)).
+
+Definition tail_recursive_specification_of_addition (add : nat -> nat -> nat) :=
+  (forall y : nat,
+      add O y = y)
+  /\
+  (forall x' y : nat,
+      add (S x') y = add x' (S y)).
+
+Definition test_add (candidate: nat -> nat -> nat) : bool :=
+  (Nat.eqb (candidate 0 0) 0)
+  &&
+  (Nat.eqb (candidate 0 1) 1)
+  &&
+  (Nat.eqb (candidate 1 0) 1)
+  &&
+  (Nat.eqb (candidate 1 1) 2)
+  &&
+  (Nat.eqb (candidate 1 2) 3)
+  &&
+  (Nat.eqb (candidate 2 1) 3)
+  &&
+  (Nat.eqb (candidate 2 2) 4)
+  &&
+  (* commutativity: *)
+  (Nat.eqb (candidate 2 10) (candidate 10 2))
+  &&
+  (* associativity: *)
+  (Nat.eqb (candidate 2 (candidate 5 10))
+           (candidate (candidate 2 5) 10))
+  (* etc. *)
+  .
+
+(* Testing the unit-test function: *)
+
+Compute (test_add Nat.add).
+
+Fixpoint r_add (x y : nat) : nat :=
+  match x with
+    O =>
+    y
+  | S x' =>
+    S (r_add x' y)
+  end.
+
+Lemma fold_unfold_r_add_O :
+  forall y : nat,
+    r_add O y =
+    y.
+Proof.
+  fold_unfold_tactic r_add.
+Qed.
+
+Lemma fold_unfold_r_add_S :
+  forall x' y : nat,
+    r_add (S x') y =
+    S (r_add x' y).
+Proof.
+  fold_unfold_tactic r_add.
+Qed.
+
+(* Implement the addition function as an instance of nat_fold_right or nat_fold_left, your choice. *)
+
+Definition r_add_right (x y : nat) : nat :=
+  nat_fold_right nat y (fun ih => S ih) x.
+
+Compute (test_add r_add_right).
+
+Proposition r_add_satisfies_the_recursive_specification_of_addition :
+  recursive_specification_of_addition r_add_right.
+Proof.
+  unfold recursive_specification_of_addition, r_add_right.
+  split.
+  - intro y.
+    exact (fold_unfold_nat_fold_right_O nat y (fun ih => S ih)).
+  - intros x' y.
+    exact (fold_unfold_nat_fold_right_S nat y (fun ih => S ih) x').
+Qed.
+
+(*
+Definition r_add_left (x y : nat) : nat :=
+  ... nat_fold_left ... ... ... x ... .
+*)
+
+(* ***** *)
+
+(* The power function: *)
+
+Definition recursive_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 r_power (x n : nat) : nat :=
+  match n with
+    O =>
+    1
+  | S n' =>
+    x * r_power x n'
+  end.
+
+Compute (test_power r_power).
+
+Lemma fold_unfold_r_power_O :
+  forall x : nat,
+    r_power x O =
+    1.
+Proof.
+  fold_unfold_tactic r_power.
+Qed.
+
+Lemma fold_unfold_r_power_S :
+  forall x n' : nat,
+    r_power x (S n') =
+    x * r_power x n'.
+Proof.
+  fold_unfold_tactic r_power.
+Qed.
+
+Fixpoint tr_power_aux (x n a : nat) : nat :=
+  match n with
+    O =>
+    a
+  | S n' =>
+    tr_power_aux x n' (x * a)
+  end.
+
+Lemma fold_unfold_tr_power_aux_O :
+  forall x a : nat,
+    tr_power_aux x 0 a =
+    a.
+Proof.
+  fold_unfold_tactic tr_power_aux.
+Qed.
+
+Lemma fold_unfold_tr_power_v1_S :
+  forall x n' a : nat,
+    tr_power_aux x (S n') a =
+    tr_power_aux x n' (x * a).
+Proof.
+  fold_unfold_tactic tr_power_aux.
+Qed.
+
+Definition tr_power (x n : nat) : nat :=
+  tr_power_aux x n 1.
+
+Compute (test_power tr_power).
+
+(*
+Definition r_power_right (x n : nat) : nat :=
+  ... nat_fold_right ... ... ... n ... .
+
+Compute (test_power r_power_right).
+*)
+
+(*
+Definition r_power_left (x n : nat) : nat :=
+  ... nat_fold_left ... ... ... n ... .
+
+Compute (test_power r_power_left).
+*)
+
+(*
+Definition tr_power_right (x n : nat) : nat :=
+  ... nat_fold_right ... ... ... n ... .
+
+Compute (test_power tr_power_right).
+*)
+
+(*
+Definition tr_power_left (x n : nat) : nat :=
+  ... nat_fold_left ... ... ... n ... .
+
+Compute (test_power tr_power_left).
+*)
+
+(* ***** *)
+
+(* The factorial function: *)
+
+Definition recursive_specification_of_the_factorial_function (fac : nat -> nat) :=
+  (fac 0 = 1)
+  /\
+  (forall n' : nat,
+    fac (S n') = S n' * fac n').
+
+Definition test_fac (candidate : nat -> nat) : bool :=
+  (candidate 0 =? 1)
+  &&
+  (candidate 1 =? 1 * 1)
+  &&
+  (candidate 2 =? 2 * 1 * 1)
+  &&
+  (candidate 3 =? 3 * 2 * 1 * 1)
+  &&
+  (candidate 4 =? 4 * 3 * 2 * 1 * 1)
+  &&
+  (candidate 5 =? 5 * 4 * 3 * 2 * 1 * 1).
+
+Fixpoint r_fac (n : nat) : nat :=
+  match n with
+    O =>
+    1
+  | S n' =>
+    S n' * r_fac n'
+  end.
+
+Compute (test_fac r_fac).
+
+Lemma fold_unfold_r_fac_O :
+  r_fac 0 =
+  1.
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+
+Lemma fold_unfold_r_fac_S :
+  forall n' : nat,
+    r_fac (S n') =
+    S n' * r_fac n'.
+Proof.
+  fold_unfold_tactic r_fac.
+Qed.
+
+Proposition r_fac_satisfies_the_recursive_specification_of_the_factorial_function :
+  recursive_specification_of_the_factorial_function r_fac.
+Proof.
+  unfold recursive_specification_of_the_factorial_function.
+  exact (conj fold_unfold_r_fac_O fold_unfold_r_fac_S).
+Qed.
+
+(* Re-implement r_fac as an instance of nat_fold_right or nat_fold_left, your choice: *)
+
+(*
+Definition r_fac_right (n : nat) : nat :=
+  ... nat_fold_right ... ... ... n ... .
+
+Compute (test_fac r_fac_right).
+
+Definition fac_left (n : nat) : nat :=
+  ... nat_fold_left ... ... ... n ... .
+
+Compute (test_fac r_fac_left).
+*)
+
+Fixpoint tr_fac_aux (n a : nat) : nat :=
+  match n with
+    O =>
+    a
+  | S n' =>
+    tr_fac_aux n' (S n' * a)
+  end.
+
+Definition tr_fac (n : nat) : nat :=
+  tr_fac_aux n 1.
+
+Compute (test_fac tr_fac).
+
+Lemma fold_unfold_tr_fac_aux_O :
+  forall a : nat,
+    tr_fac_aux 0 a =
+    a.
+Proof.
+  fold_unfold_tactic tr_fac_aux.
+Qed.
+
+Lemma fold_unfold_tr_fac_aux_S :
+  forall n' a : nat,
+    tr_fac_aux (S n') a =
+    tr_fac_aux n' (S n' * a).
+Proof.
+  fold_unfold_tactic tr_fac_aux.
+Qed.
+
+Proposition tr_fac_satisfies_the_recursive_specification_of_the_factorial_function :
+  recursive_specification_of_the_factorial_function tr_fac.
+Proof.
+  unfold recursive_specification_of_the_factorial_function.
+Abort.
+
+(* Re-implement tr_fac as an instance of nat_fold_right or nat_fold_left, your choice: *)
+
+(*
+Definition tr_fac_right (n : nat) : nat :=
+  ... nat_fold_right ... ... ... n ... .
+
+Compute (test_fac tr_fac_right).
+
+Definition tr_fac_left (n : nat) : nat :=
+  ... nat_fold_left ... ... ... n ... .
+
+Compute (test_fac tr_fac_alt).
+*)
+
+(* ***** *)
+
+Definition specification_of_the_fibonacci_function (fib : nat -> nat) :=
+  fib 0 = 0
+  /\
+  fib 1 = 1
+  /\
+  forall n'' : nat,
+    fib (S (S n'')) = fib (S n'') + fib n''.
+
+Definition test_fib (candidate: nat -> nat) : bool :=
+  (candidate 0 =? 0)
+  &&
+  (candidate 1 =? 1)
+  &&
+  (candidate 2 =? 1)
+  &&
+  (candidate 3 =? 2)
+  &&
+  (candidate 4 =? 3)
+  &&
+  (candidate 5 =? 5)
+  (* etc. *).
+
+Fixpoint r_fib (n : nat) : nat :=
+  match n with
+    0 =>
+    0
+  | S n' =>
+    match n' with
+      0 =>
+      1
+    | S n'' =>
+      r_fib n' + r_fib n''
+    end
+  end.
+
+Compute (test_fib r_fib).
+
+Lemma fold_unfold_r_fib_O :
+  r_fib O =
+  0.
+Proof.
+  fold_unfold_tactic r_fib.
+Qed.
+
+Lemma fold_unfold_r_fib_S :
+  forall n' : nat,
+    r_fib (S n') =
+    match n' with
+      0 =>
+      1
+    | S n'' =>
+      r_fib n' + r_fib n''
+    end.
+Proof.
+  fold_unfold_tactic r_fib.
+Qed.
+
+Corollary fold_unfold_r_fib_SO :
+  r_fib 1 =
+  1.
+Proof.
+  rewrite -> (fold_unfold_r_fib_S 0).
+  reflexivity.
+Qed.
+
+Corollary fold_unfold_r_fib_SS :
+  forall n'' : nat,
+    r_fib (S (S n'')) =
+    r_fib (S n'') + r_fib n''.
+Proof.
+  intro n''.
+  rewrite -> (fold_unfold_r_fib_S (S n'')).
+  reflexivity.
+Qed.
+
+Proposition r_fib_satisfies_the_specification_of_the_fibonacci_function :
+  specification_of_the_fibonacci_function r_fib.
+Proof.
+  unfold specification_of_the_fibonacci_function.
+  exact (conj fold_unfold_r_fib_O (conj fold_unfold_r_fib_SO fold_unfold_r_fib_SS)).
+Qed.
+
+(* Implement the Fibonacci function as an instance of nat_fold_right or nat_fold_left, your choice: *)
+
+(*
+Definition fib_right (n : nat) : nat :=
+  ... nat_fold_right ... ... ... n ... .
+
+Compute (test_fib tr_fib_right).
+
+Definition fib_left (n : nat) : nat :=
+  ... nat_fold_left ... ... ... n ... .
+
+Compute (test_fib fib_left).
+*)
+
+(* ********** *)
+
+(* Task 9 *)
+
+(* Under which conditions -- if any -- are nat_fold_right and nat_fold_left equivalent? *)
+
+(* ********** *)
+
+(* end of midterm-project.v *)
diff --git a/cs3234/labs/week-05_mystery-functions.v b/cs3234/labs/week-05_mystery-functions.v
new file mode 100644
index 0000000..e162513
--- /dev/null
+++ b/cs3234/labs/week-05_mystery-functions.v
@@ -0,0 +1,754 @@
+(* week-05_mystery-functions.v *)
+(* LPP 2024 - CS3234 2023-2024, Sem2 *)
+(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
+(* Version of 16 Feb 2024 *)
+
+(* ********** *)
+
+(* Paraphernalia: *)
+
+Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
+
+Require Import Bool Arith.
+
+Check Nat.eqb.
+Check (fun i j => Nat.eqb i j).
+(* so "X =? Y" is syntactic sugar for "Nat.eqb X Y" *)
+
+Check Bool.eqb.
+Check (fun b1 b2 => Bool.eqb b1 b2).
+(* so eqb stands for Bool.eqb *)
+
+(* ********** *)
+
+
+Definition specification_of_mystery_function_00 (mf : nat -> nat) :=
+  mf 0 = 1
+  /\
+  forall i j : nat, mf (S (i + j)) = mf i + mf j.
+
+(* ***** *)
+
+Proposition there_is_at_most_one_mystery_function_00 :
+  forall f g : nat -> nat,
+    specification_of_mystery_function_00 f ->
+    specification_of_mystery_function_00 g ->
+    forall n : nat,
+      f n = g n.
+Proof.
+  intros f g.
+  intros [H_f_O H_f_S] [H_g_O H_g_S].
+  intro n.
+  induction n as [| n' IHn'].
+  - rewrite -> H_f_O.
+    symmetry.
+    exact H_g_O.
+  - rewrite <- (Nat.add_0_l n').
+    rewrite -> (H_f_S 0 n').
+    rewrite -> (H_f_O).
+    rewrite -> (H_g_S 0 n').
+    rewrite -> (H_g_O).
+    rewrite -> IHn'.
+    reflexivity.
+Qed.
+
+(* ***** *)
+
+Definition unit_test_for_mystery_function_00a (mf : nat -> nat) :=
+  (mf 0 =? 1)
+  &&
+  (mf 1 =? 2)
+  &&
+  (mf 2 =? 3)
+  &&
+  (mf 3 =? 4).
+
+(* etc. *)
+
+Definition unit_test_for_mystery_function_00b (mf : nat -> nat) :=
+  (mf 0 =? 1) && (mf 1 =? 2) (* etc. *).
+
+Definition unit_test_for_mystery_function_00c (mf : nat -> nat) :=
+  (mf 0 =? 1) && (mf 1 =? 2) && (mf 2 =? 3) (* etc. *).
+
+Definition unit_test_for_mystery_function_00d (mf : nat -> nat) :=
+  (mf 0 =? 1) && (mf 1 =? 2) && (mf 2 =? 3) && (mf 3 =? 4)
+  (* etc. *).
+
+(* ***** *)
+
+Compute (unit_test_for_mystery_function_00d).
+
+Definition mystery_function_00 := S.
+
+Definition less_succinct_mystery_function_00 (n : nat) : nat :=
+  S n.
+
+Compute (unit_test_for_mystery_function_00d mystery_function_00).
+
+Theorem there_is_at_least_one_mystery_function_00 :
+  specification_of_mystery_function_00 mystery_function_00.
+Proof.
+  unfold specification_of_mystery_function_00, mystery_function_00.
+  split.
+  - reflexivity.
+  - intros i j.
+    rewrite -> (plus_Sn_m i (S j)).
+    rewrite <- (plus_n_Sm i j).
+    reflexivity.
+Qed.
+
+(* ***** *)
+
+Definition mystery_function_00_alt := fun (n : nat) => n + 1.
+
+Theorem there_is_at_least_one_mystery_function_00_alt :
+  specification_of_mystery_function_00 mystery_function_00_alt.
+Proof.
+Abort.
+
+(* ********** *)
+
+(* Thanks to calvin's eureka lemma *)
+Definition specification_of_mystery_function_11 (mf : nat -> nat) :=
+  mf 1 = 1
+  /\
+  forall i j : nat,
+    mf (i + j) = mf i + 2 * i * j + mf j.
+
+Proposition about_mystery_function_11 :
+  forall f : nat -> nat,
+    specification_of_mystery_function_11 f ->
+    f 0 = 0.
+Proof.
+  intros f.
+  intros [S_f_1 S_f_ij].
+  assert (S_f_0 := (S_f_ij 0 0)).
+  rewrite -> (Nat.add_0_l 0) in S_f_0.
+  rewrite -> (Nat.mul_0_r 2) in S_f_0.
+  rewrite -> (Nat.mul_0_r 0) in S_f_0.
+  rewrite -> (Nat.add_0_r (f 0)) in S_f_0.
+  rewrite <- (Nat.add_0_r (f 0)) in S_f_0 at 1.
+  symmetry.
+  Check Plus.plus_reg_l_stt.
+  Check (Plus.plus_reg_l_stt 0 (f 0) (f 0) S_f_0).
+  exact (Plus.plus_reg_l_stt 0 (f 0) (f 0) S_f_0).
+  Qed.
+
+Proposition there_is_at_most_one_mystery_function_11 :
+  forall f g : nat -> nat,
+    specification_of_mystery_function_11 f ->
+    specification_of_mystery_function_11 g ->
+    forall n : nat,
+      f n = g n.
+Proof.
+  intros f g.
+  intros S_f S_g.
+  assert (S_tmp_f := S_f).
+  assert (S_tmp_g := S_g).
+  destruct S_tmp_f as [S_f_1 S_f_ij].
+  destruct S_tmp_g as [S_g_1 S_g_ij].
+  intro x.
+  induction x as [| x' IHx'].
+  - rewrite -> (about_mystery_function_11 g S_g).
+    exact (about_mystery_function_11 f S_f).
+  - rewrite <- (Nat.add_1_l x').
+    rewrite -> (S_f_ij 1 x').
+    rewrite -> S_f_1.
+    rewrite -> IHx'.
+    rewrite -> (S_g_ij 1 x').
+    rewrite -> S_g_1.
+    reflexivity.
+Qed.
+
+
+(* ********** *)
+
+Definition specification_of_mystery_function_04 (mf : nat -> nat) :=
+  mf 0 = 0
+  /\
+  forall n' : nat,
+    mf (S n') = mf n' + S (2 * n').
+
+Theorem there_is_at_most_one_mystery_function_04 :
+  forall f g : nat -> nat,
+    specification_of_mystery_function_04 f ->
+    specification_of_mystery_function_04 g ->
+    forall x : nat,
+      f x = g x.
+Proof.
+  intros f g.
+  intros [S_f_0 S_f_n] [S_g_0 S_g_n].
+  intro x.
+  induction x as [| x' IHx'].
+  - rewrite -> S_g_0.
+    exact S_f_0.
+  - rewrite -> (S_f_n x').
+    rewrite -> (S_g_n x').
+    rewrite -> IHx'.
+    reflexivity.
+Qed.
+
+Definition unit_test_for_mystery_function_04 (mf : nat -> nat) :=
+ (mf 1 =? 1)
+ && (mf 0 =? 0)
+ && (mf 2 =? 4)
+ && (mf 3 =? 9).
+
+
+Definition mystery_function_04 := Nat.square.
+
+Compute (unit_test_for_mystery_function_04 mystery_function_04).
+
+Theorem there_is_at_least_one_mystery_function_04 :
+  specification_of_mystery_function_04 mystery_function_04.
+Proof.
+  unfold specification_of_mystery_function_04, mystery_function_04.
+  unfold Nat.square.
+  split.
+  - exact (Nat.mul_1_r 0).
+  - intros n.
+    Search (S _ * _).
+    rewrite -> (Nat.mul_succ_l n (S n)).
+    rewrite -> (Nat.mul_succ_r n n).
+    Search (_ + S _).
+    rewrite <- (Nat.add_assoc (n * n) n (S n)).
+    rewrite -> (Nat.add_succ_r n n).
+    Search (_ + _).
+    rewrite <- (Nat.mul_1_l n) at 3.
+    Search (_ * _ + _).
+    rewrite <- (Nat.mul_succ_l 1 n).
+    reflexivity.
+Qed.
+(* ********** *)
+
+Definition specification_of_mystery_function_15 (mf : nat -> nat * nat) :=
+  mf 0 = (0, 1)
+  /\
+  forall n' : nat,
+    mf (S n') = let (x, y) := mf n'
+                in (S x, y * S x).
+
+Theorem there_is_at_most_one_mystery_function_15 :
+  forall f g : nat -> (nat * nat),
+    specification_of_mystery_function_15 f ->
+    specification_of_mystery_function_15 g ->
+    forall x : nat,
+      f x = g x.
+Proof.
+  intros f g.
+  intros [S_f_0 S_f_n] [S_g_0 S_g_n].
+  intro x.
+  induction x as [| x' IHx'].
+  - rewrite -> S_g_0.
+    exact S_f_0.
+  - rewrite -> (S_f_n x').
+    rewrite -> (S_g_n x').
+    rewrite -> IHx'.
+    reflexivity.
+Qed.
+
+Definition pair_equal (p1 p2: nat * nat) : bool :=
+  match p1, p2 with
+    | (a1, b1), (a2, b2) => (a1 =? a2) && (b1 =? b2)
+       end.
+
+Definition unit_test_for_mystery_function_15 (mf : nat -> nat * nat) :=
+  (pair_equal (mf 0) (0, 1))
+  &&
+  (pair_equal (mf 1) (1, 1))
+  &&
+  (pair_equal (mf 2) (2, 2))
+  &&
+  (pair_equal (mf 3) (3, 6))
+  &&
+  (pair_equal (mf 4) (4, 24))
+  &&
+  (pair_equal (mf 5) (5, 120)).
+
+(* The Factorial Function *)
+Fixpoint factorial (n : nat) :=
+  match n with
+  | 0 => (0, 1)
+  | S k => match (factorial k) with
+          | (a, b) => (n, n * b)
+          end
+  end.
+
+Definition mystery_function_15 := factorial.
+
+Compute (unit_test_for_mystery_function_15 mystery_function_15).
+
+Theorem there_is_at_least_one_mystery_function_15 :
+  specification_of_mystery_function_15 mystery_function_15.
+Proof.
+  unfold specification_of_mystery_function_15, mystery_function_15.
+  unfold factorial.
+  split.
+  - reflexivity.
+  - intro n.
+    induction n as [| n' IHn'].
+    + reflexivity.
+    + fold factorial in IHn'.
+      fold factorial.
+      rewrite -> IHn'.
+      Abort.
+
+
+
+
+
+(* ********** *)
+
+Definition specification_of_mystery_function_16 (mf : nat -> nat * nat) :=
+  mf 0 = (0, 1)
+  /\
+  forall n' : nat,
+    mf (S n') = let (x, y) := mf n'
+                in (y, x + y).
+
+Theorem there_is_at_most_one_mystery_function_16 :
+  forall f g : nat -> (nat * nat),
+    specification_of_mystery_function_16 f ->
+    specification_of_mystery_function_16 g ->
+    forall x : nat,
+      f x = g x.
+Proof.
+  intros f g.
+  intros [S_f_0 S_f_n] [S_g_0 S_g_n].
+  intro x.
+  induction x as [| x' IHx'].
+  - rewrite -> S_g_0.
+    exact S_f_0.
+  - rewrite -> (S_f_n x').
+    rewrite -> (S_g_n x').
+    rewrite -> IHx'.
+    reflexivity.
+Qed.
+(* ********** *)
+
+Definition specification_of_mystery_function_17 (mf : nat -> nat) :=
+  mf 0 = 0
+  /\
+  mf 1 = 1
+  /\
+  mf 2 = 1
+  /\
+  forall p q : nat,
+    mf (S (p + q)) = mf (S p) * mf (S q) + mf p * mf q.
+
+Theorem there_is_at_most_one_mystery_function_17 :
+  forall f g : nat -> nat,
+    specification_of_mystery_function_17 f ->
+    specification_of_mystery_function_17 g ->
+    forall x : nat,
+      f x = g x.
+Proof.
+  intros f g.
+  intros [S_f_0 [S_f_1 [S_f_2 S_f_n]]].
+  intros [S_g_0 [S_g_1 [S_g_2 S_g_n]]].
+  intro x.
+  induction x as [| x' IHx'].
+  - rewrite -> S_g_0.
+    exact S_f_0.
+  - Search (_ + 1 = S _).
+  (* Search (S _ + _). *)
+  (* Check (plus_Sn_m 1 1). *)
+  (* rewrite <- (Nat.add_1_l 2) at 1. *)
+  (* rewrite <- (Nat.add_0_r 3). *)
+  (* rewrite -> (plus_Sn_m 2 0). *)
+  (* rewrite -> (S_mf_pq 1 1). *)
+  (* rewrite -> (S_mf_pq 2 0). *)
+  (* rewrite -> S_mf_2. *)
+  (* rewrite -> S_mf_1. *)
+  (* rewrite -> (S_mf_0). *)
+  (* simpl. *)
+  Abort.
+
+
+
+(* ********** *)
+
+Definition specification_of_mystery_function_18 (mf : nat -> nat) :=
+  mf 0 = 0
+  /\
+  mf 1 = 1
+  /\
+  mf 2 = 1
+  /\
+  forall n''' : nat,
+    mf n''' + mf (S (S (S n'''))) = 2 * mf (S (S n''')).
+
+Theorem there_is_atmost_one_mystery_function_18 :
+  forall f g : nat -> nat,
+    specification_of_mystery_function_18 f ->
+    specification_of_mystery_function_18 g ->
+    forall x : nat,
+      f x = g x.
+Proof.
+  intros f g.
+  intros [S_f_0 [S_f_1 [S_f_2 S_f_n]]].
+  intros [S_g_0 [S_g_1 [S_g_2 S_g_n]]].
+  intro x.
+  induction x as [| x' IHx'].
+  - rewrite -> S_g_0.
+    exact S_f_0.
+  - Search (S (S _) = S _).
+    Abort.
+
+
+
+
+(* ********** *)
+
+Fixpoint add_v1 (i j : nat) : nat :=
+  match i with
+  | O =>
+    j
+  | S i' =>
+    S (add_v1 i' j)
+  end.
+
+Definition specification_of_mystery_function_03 (mf : nat -> nat -> nat) :=
+  mf 0 0 = 0
+  /\
+  (forall i j: nat, mf (S i) j = S (mf i j))
+  /\
+  (forall i j: nat, S (mf i j) = mf i (S j)).
+
+Theorem there_is_at_least_one_mystery_function_03 :
+  specification_of_mystery_function_03 Nat.add.
+Proof.
+  unfold specification_of_mystery_function_03.
+  split.
+  - reflexivity.
+  - split.
+    + intros i j.
+      Search (S _ + _ = S (_ + _)).
+      rewrite -> (plus_Sn_m i j).
+      reflexivity.
+    + intros i j.
+      rewrite <- (plus_n_Sm i j).
+      reflexivity.
+Qed.
+
+Theorem there_is_atmost_one_mystery_function_03 :
+  forall f g : nat -> nat -> nat,
+    specification_of_mystery_function_03 f ->
+    specification_of_mystery_function_03 g ->
+    forall x y : nat,
+      f x y = g x y.
+Proof.
+  intros f g.
+  intros [S_f_0 [S_f_1 S_f_2]].
+  intros [S_g_0 [S_g_1 S_g_2]].
+  induction x as [| x' IHx'].
+  - intro y.
+    Abort.
+
+
+(* ********** *)
+
+Definition specification_of_mystery_function_42 (mf : nat -> nat) :=
+  mf 1 = 42
+  /\
+  forall i j : nat,
+    mf (i + j) = mf i + mf j.
+
+Theorem there_is_atmost_one_mystery_function_42 :
+  forall f g : nat -> nat,
+    specification_of_mystery_function_42 f ->
+    specification_of_mystery_function_42 g ->
+    forall x : nat,
+      f x = g x.
+Proof.
+  intros f g.
+  intros [S_f_1 S_f_S] [S_g_1 S_g_S].
+  intro x.
+  induction x as [| x' IHx'].
+  - rewrite <- (Nat.add_0_l 0).
+      rewrite -> (S_f_S 0 0).
+
+      Check Plus.plus_reg_l_stt.
+  Abort.
+
+(* ********** *)
+
+Definition specification_of_mystery_function_07 (mf : nat -> nat -> nat) :=
+  (forall j : nat, mf 0 j = j)
+  /\
+  (forall i : nat, mf i 0 = i)
+  /\
+  (forall i j k : nat, mf (i + k) (j + k) = (mf i j) + k).
+
+(* ********** *)
+
+Definition specification_of_mystery_function_08 (mf : nat -> nat -> bool) :=
+  (forall j : nat, mf 0 j = true)
+  /\
+  (forall i : nat, mf (S i) 0 = false)
+  /\
+  (forall i j : nat, mf (S i) (S j) = mf i j).
+
+(* ********** *)
+
+Definition specification_of_mystery_function_23 (mf : nat -> nat) :=
+  mf 0 = 0
+  /\
+  mf 1 = 0
+  /\
+  forall n'' : nat,
+    mf (S (S n'')) = S (mf n'').
+
+(* ********** *)
+
+Definition specification_of_mystery_function_24 (mf : nat -> nat) :=
+  mf 0 = 0
+  /\
+  mf 1 = 1
+  /\
+  forall n'' : nat,
+    mf (S (S n'')) = S (mf n'').
+
+(* ********** *)
+
+Definition specification_of_mystery_function_13 (mf : nat -> nat) :=
+  (forall q : nat, mf (2 * q) = q)
+  /\
+  (forall q : nat, mf (S (2 * q)) = q).
+
+(* ********** *)
+
+Definition specification_of_mystery_function_25 (mf : nat -> nat) :=
+  mf 0 = 0
+  /\
+  (forall q : nat,
+      mf (2 * (S q)) = S (mf (S q)))
+  /\
+  mf 1 = 0
+  /\
+  (forall q : nat,
+      mf (S (2 * (S q))) = S (mf (S q))).
+
+(* ****** *)
+
+Definition specification_of_mystery_function_20 (mf : nat -> nat -> nat) :=
+  (forall j : nat, mf O j = j)
+  /\
+  (forall i j : nat, mf (S i) j = S (mf i j)).
+
+(* ****** *)
+
+Definition specification_of_mystery_function_21 (mf : nat -> nat -> nat) :=
+  (forall j : nat, mf O j = j)
+  /\
+  (forall i j : nat, mf (S i) j = mf i (S j)).
+
+(* ****** *)
+
+Definition specification_of_mystery_function_22 (mf : nat -> nat -> nat) :=
+  forall i j : nat,
+    mf O j = j
+    /\
+    mf (S i) j = mf i (S j).
+
+(* ********** *)
+
+(* Binary trees of natural numbers: *)
+
+Inductive tree : Type :=
+  | Leaf : nat -> tree
+  | Node : tree -> tree -> tree.
+
+Definition specification_of_mystery_function_19 (mf : tree -> tree) :=
+  (forall n : nat,
+     mf (Leaf n) = Leaf n)
+  /\
+  (forall (n : nat) (t : tree),
+     mf (Node (Leaf n) t) = Node (Leaf n) (mf t))
+  /\
+  (forall t11 t12 t2 : tree,
+     mf (Node (Node t11 t12) t2) = mf (Node t11 (Node t12 t2))).
+
+(* You might not manage to prove
+   that at most one function satisfies this specification (why?),
+   but consider whether the following function does.
+   Assuming it does, what does this function do?
+   And what is the issue here?
+*)
+
+Fixpoint mystery_function_19_aux (t a : tree) : tree :=
+  match t with
+  | Leaf n =>
+     Node (Leaf n) a
+  | Node t1 t2 =>
+     mystery_function_19_aux t1 (mystery_function_19_aux t2 a)
+  end.
+
+Fixpoint mystery_function_19 (t : tree) : tree :=
+  match t with
+  | Leaf n =>
+     Leaf n
+  | Node t1 t2 =>
+     mystery_function_19_aux t1 (mystery_function_19 t2)
+  end.
+
+Theorem there_is_at_least_one_mystery_function :
+  specification_of_mystery_function_19 mystery_function_19.
+Proof.
+  unfold specification_of_mystery_function_19.
+  unfold mystery_function_19.
+  unfold mystery_function_19_aux.
+
+(* ********** *)
+
+Definition specification_of_mystery_function_05 (mf : nat -> nat) :=
+  mf 0 = 1
+  /\
+  forall i j : nat,
+    mf (S (i + j)) = 2 * mf i * mf j.
+
+(* ********** *)
+
+Definition specification_of_mystery_function_06 (mf : nat -> nat) :=
+  mf 0 = 2
+  /\
+  forall i j : nat,
+    mf (S (i + j)) = mf i * mf j.
+
+(* ********** *)
+
+Definition specification_of_mystery_function_09 (mf : nat -> bool) :=
+  mf 0 = false
+  /\
+  mf 1 = true
+  /\
+  forall i j : nat,
+    mf (i + j) = xorb (mf i) (mf j).
+
+(* ********** *)
+
+Definition specification_of_mystery_function_10 (mf : nat -> bool) :=
+  mf 0 = false
+  /\
+  mf 1 = true
+  /\
+  forall i j : nat,
+    mf (i + j) = Bool.eqb (mf i) (mf j).
+
+(* ********** *)
+
+Definition specification_of_mystery_function_12 (mf : nat -> nat) :=
+  mf 1 = 1
+  /\
+  forall i : nat,
+    mf (S (S i)) = (S (S i)) * mf (S i).
+
+(* ********** *)
+
+Definition specification_of_mystery_function_14 (mf : nat -> bool) :=
+  (forall q : nat, mf (2 * q) = true)
+  /\
+  (forall q : nat, mf (S (2 * q)) = false).
+
+(* ********** *)
+
+Definition specification_of_mystery_function_29 (mf : nat -> bool) :=
+  (mf 0 = true)
+  /\
+  (mf 1 = false)
+  /\
+  (forall n'' : nat, mf (S (S n'')) = mf n'').
+
+(* ********** *)
+
+Require Import String.
+
+Inductive arithmetic_expression : Type :=
+  Literal : nat -> arithmetic_expression
+| Error : string -> arithmetic_expression
+| Plus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression.
+
+Inductive expressible_value : Type :=
+  Expressible_nat : nat -> expressible_value
+| Expressible_msg : string -> expressible_value.
+
+Definition specification_of_mystery_function_30 (mf : arithmetic_expression -> expressible_value) :=
+  (forall n : nat,
+     mf (Literal n) = Expressible_nat n)
+  /\
+  (forall s : string,
+     mf (Error s) = Expressible_msg s)
+  /\
+  ((forall (ae1 ae2 : arithmetic_expression)
+           (n1 n2 : nat),
+       mf ae1 = Expressible_nat n1 ->
+       mf ae2 = Expressible_nat n2 ->
+       mf (Plus ae1 ae2) = Expressible_nat (n1 + n2))
+   /\
+   (forall (ae1 ae2 : arithmetic_expression)
+           (s1 : string),
+       mf ae1 = Expressible_msg s1 ->
+       mf (Plus ae1 ae2) = Expressible_msg s1)
+   /\
+   (forall (ae1 ae2 : arithmetic_expression)
+           (s2 : string),
+       mf ae2 = Expressible_msg s2 ->
+       mf (Plus ae1 ae2) = Expressible_msg s2)).
+Abort.
+
+Theorem there_is_at_most_one_mystery_function_30 :
+  forall f g : arithmetic_expression -> expressible_value,
+    specification_of_mystery_function_30 f ->
+    specification_of_mystery_function_30 g ->
+    forall expr : arithmetic_expression,
+      f expr = g expr.
+Proof.
+  intros f g.
+  intros S_f.
+  intros S_g.
+  intro expr.
+  induction expr as [n' | s' | e1 IHe1 e2  IHe2].
+  - unfold specification_of_mystery_function_30 in S_f.
+    destruct S_f as [S_f_literal _].
+    unfold specification_of_mystery_function_30 in S_g.
+    destruct S_g as [S_g_literal _].
+    rewrite -> (S_g_literal n').
+    exact (S_f_literal n').
+  - unfold specification_of_mystery_function_30 in S_f.
+    destruct S_f as [_ [S_f_error _]].
+    unfold specification_of_mystery_function_30 in S_g.
+    destruct S_g as [_ [S_g_error _]].
+    rewrite -> (S_g_error s').
+    exact (S_f_error s').
+  - revert S_f.
+    revert S_g.
+    unfold specification_of_mystery_function_30.
+Abort.
+(* ********** *)
+
+(* Simple examples of specifications: *)
+
+(* ***** *)
+
+Definition specification_of_the_factorial_function (fac : nat -> nat) :=
+  fac 0 = 1
+  /\
+  forall n' : nat, fac (S n') = S n' * fac n'.
+
+(* ***** *)
+
+Definition specification_of_the_fibonacci_function (fib : nat -> nat) :=
+  fib 0 = 0
+  /\
+  fib 1 = 1
+  /\
+  forall n'' : nat,
+    fib (S (S n'')) = fib n'' + fib (S n'').
+
+(* ********** *)
+
+(* end of week-05_mystery-functions.v *)
+
+
+Search Prop.