From db5769b9b4cb256264f20a24f3490e83169b7e7a Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Tue, 7 May 2024 00:02:04 +0800 Subject: [PATCH] feat: remove midterm project --- cs3234/labs/midterm_project.v | 2121 --------------------------------- 1 file changed, 2121 deletions(-) delete mode 100644 cs3234/labs/midterm_project.v diff --git a/cs3234/labs/midterm_project.v b/cs3234/labs/midterm_project.v deleted file mode 100644 index c85c09e..0000000 --- a/cs3234/labs/midterm_project.v +++ /dev/null @@ -1,2121 +0,0 @@ -(* midterm-project.v *) -(* LPP 2024 - CS3234 2023-2024, Sem2 *) -(* Olivier Danvy *) -(* 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. -*) - -Fixpoint list_reverse_acc (V : Type) (vs acc: list V) := - match vs with - | nil => acc - | v :: vs' => list_reverse_acc V vs' (v :: acc) - end. - -Definition list_reverse_alt (V : Type) (vs : list V) : list V := - list_reverse_acc V vs nil. - -(* - 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. -*) - -Lemma fold_unfold_list_reverse_acc_nil : - forall (V : Type) - (acc : list V) - , - list_reverse_acc V nil acc = acc. -Proof. - fold_unfold_tactic list_reverse_acc. -Qed. - -Lemma fold_unfold_list_reverse_acc_cons : - forall (V : Type) - (v : V) - (vs' acc : list V), - list_reverse_acc V (v :: vs') acc = list_reverse_acc V vs' (v :: acc). -Proof. - fold_unfold_tactic list_reverse. -Qed. - -Theorem about_list_reverse_acc_and_list_append : - forall (V: Type) - (v : V) - (vs acc : list V), - list_reverse_acc V vs (list_append V acc (v :: nil)) = - list_append V (list_reverse_acc V vs acc) (v :: nil). -Proof. - intros V v vs. - induction vs as [ | v' vs' IHvs']. - - intro acc. - rewrite -> (fold_unfold_list_reverse_acc_nil V (list_append V acc (v :: nil))). - rewrite -> (fold_unfold_list_reverse_acc_nil V acc). - reflexivity. - - intro acc. - rewrite -> (fold_unfold_list_reverse_acc_cons V v' vs' (list_append V acc (v :: nil))). - rewrite -> (fold_unfold_list_reverse_acc_cons V v' vs' acc). - rewrite <- (IHvs' (v' :: acc)). - rewrite -> (fold_unfold_list_append_cons V v' acc). - reflexivity. -Qed. - -Theorem list_reverse_alt_satisfies_the_specification_of_list_reverse : - specification_of_list_reverse list_reverse_alt. -Proof. - unfold specification_of_list_reverse. - intros append. - unfold specification_of_list_append. - intro S_append. - split. - - intros V. - unfold list_reverse_alt. - exact (fold_unfold_list_reverse_acc_nil V nil). - - intros V v vs. - unfold list_reverse_alt. - rewrite -> (fold_unfold_list_reverse_acc_cons V v vs nil). - rewrite <- (fold_unfold_list_append_nil V (v :: nil)). - rewrite -> (about_list_reverse_acc_and_list_append V v vs nil). - (* FIXME: This feels pretty sketchy and I don't fully pass in arguments, so there might be some Coq magic here. *) - Check (there_is_at_most_one_list_append_function V append list_append S_append - list_append_satisfies_the_specification_of_list_append). - rewrite -> (there_is_at_most_one_list_append_function V append list_append S_append - list_append_satisfies_the_specification_of_list_append - (list_reverse_acc V vs nil) (list_append V nil (v :: nil))). - rewrite -> (nil_is_left_neutral_wrt_list_append V). - reflexivity. -Qed. -(* {END} *) - -(* {task_5_h_4} *) -Theorem there_is_at_most_one_list_reverse_function : - forall (V: Type) - (list_reverse_1 list_reverse_2 : forall V : Type, list V -> list V), - specification_of_list_reverse list_reverse_1 -> - specification_of_list_reverse list_reverse_2 -> - forall vs : list V, - list_reverse_1 V vs = list_reverse_2 V vs. -Proof. - intros V list_reverse_1 list_reverse_2. - intros S_list_reverse_1 S_list_reverse_2. - unfold specification_of_list_reverse in S_list_reverse_1. - assert (specification_of_list_append list_append) as S_list_append. - { exact list_append_satisfies_the_specification_of_list_append. } - assert (S_list_reverse_1 := (S_list_reverse_1 list_append S_list_append)). - assert (S_list_reverse_2 := (S_list_reverse_2 list_append S_list_append)). - destruct S_list_reverse_1 as [S_list_reverse_1_nil S_list_reverse_1_cons]. - destruct S_list_reverse_2 as [S_list_reverse_2_nil S_list_reverse_2_cons]. - - intro vs. - induction vs as [ | v' vs' IHvs' ]. - - rewrite -> (S_list_reverse_2_nil V). - exact (S_list_reverse_1_nil V). - - rewrite -> (S_list_reverse_2_cons V v' vs'). - rewrite -> (S_list_reverse_1_cons V v' vs'). - rewrite -> IHvs'. - reflexivity. -Qed. -(* {END} *) - -(* TODO The name of this isn't that great *) - -(* {task_5_h_5} *) -Proposition list_reverse_and_list_reverse_alt_equiv : - forall (V : Type) - (vs : list V), - list_reverse V vs = list_reverse_alt V vs. -Proof. - intro V. - exact (there_is_at_most_one_list_reverse_function V list_reverse list_reverse_alt - list_reverse_satisfies_the_specification_of_list_reverse - list_reverse_alt_satisfies_the_specification_of_list_reverse). -Qed. -(* {END} *) - -(* TODO The name of this isn't that great *) - -(* {task_5_h_6} *) -Proposition list_reverse_alt_and_list_append_commute_with_each_other : - forall (V : Type) - (v1s v2s : list V), - list_append V (list_reverse_alt V v2s) (list_reverse_alt V v1s) = list_reverse_alt V (list_append V v1s v2s). -Proof. - intros V v1s v2s. - rewrite <- (list_reverse_and_list_reverse_alt_equiv V v2s). - rewrite <- (list_reverse_and_list_reverse_alt_equiv V v1s). - rewrite <- (list_reverse_and_list_reverse_alt_equiv V (list_append V v1s v2s)). - exact (list_reverse_and_list_append_commute_with_each_other V v1s v2s). -Qed. -(* {END} *) - -(* TODO The name of this isn't that great *) - -(* {task_5_h_7} *) -Proposition list_reverse_alt_and_list_length_commute_with_each_other : - forall (V : Type) - (vs : list V), - list_length V (list_reverse_alt V vs) = list_length V vs. -Proof. - intros V vs. - rewrite <- (list_reverse_and_list_reverse_alt_equiv V vs). - exact (list_reverse_and_list_length_commute_with_each_other V vs). -Qed. -(* {END} *) - -(* TODO The name of this isn't that great *) - -(* {task_5_h_8} *) -Proposition list_reverse_alt_is_involutory : - forall (V : Type) - (vs : list V), - list_reverse_alt V (list_reverse_alt V vs) = vs. -Proof. - intros V vs. - rewrite <- (list_reverse_and_list_reverse_alt_equiv V vs). - rewrite <- (list_reverse_and_list_reverse_alt_equiv V (list_reverse V vs)). - exact (list_reverse_is_involutory V vs). -Qed. - - - -(* ********** *) - -(* 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. - intros list_map1 list_map2. - intros [S_list_map1_nil S_list_map1_cons]. - intros [S_list_map2_nil S_list_map2_cons]. - intros V W f vs. - induction vs as [ | v vs' IHvs' ]. - - rewrite -> (S_list_map2_nil V W f). - exact (S_list_map1_nil V W f). - - rewrite -> (S_list_map2_cons V W f v vs'). - rewrite -> (S_list_map1_cons V W f v vs'). - rewrite -> IHvs'. - reflexivity. -Qed. - -(* - 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 := - list_map V V (fun v => v) vs. - -Theorem list_copy_as_list_map_satisfies_the_specification_of_list_copy : - specification_of_list_copy list_copy_as_list_map. -Proof. - unfold specification_of_list_copy. - split. - - intro V. - unfold list_copy_as_list_map. - rewrite -> (fold_unfold_list_map_nil V V (fun v => v)). - reflexivity. - - intros V v vs. - unfold list_copy_as_list_map. - rewrite -> (fold_unfold_list_map_cons V V (fun a => a) v vs). - reflexivity. -Qed. - -(* -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. -*) -Proposition list_map_and_list_length_commute_with_each_other : - forall (V W : Type) - (f : V -> W) - (vs : list V), - list_length W (list_map V W f vs) = list_length V vs. -Proof. - intros V W f vs. - induction vs as [ | v' vs' IHvs' ]. - - rewrite ->(fold_unfold_list_map_nil V W f). - rewrite -> (fold_unfold_list_length_nil V). - exact (fold_unfold_list_length_nil W). - - rewrite -> (fold_unfold_list_map_cons V W f v' vs'). - rewrite -> (fold_unfold_list_length_cons W (f v') (list_map V W f vs')). - rewrite -> IHvs'. - rewrite -> (fold_unfold_list_length_cons V v' vs'). - reflexivity. - Qed. - -(* - g. Do list_map and list_append commute with each other and if so how? -*) - -Proposition list_map_and_list_append_commute_with_each_other : - forall (V W : Type) - (f : V -> W) - (v1s v2s : list V), - list_append W (list_map V W f v1s) (list_map V W f v2s) = list_map V W f (list_append V v1s v2s). -Proof. - intros V W f v1s. - induction v1s as [ | v1' v1s' IHv1s' ]. - - intros v2s. - rewrite -> (fold_unfold_list_map_nil V W f). - rewrite -> (fold_unfold_list_append_nil V v2s). - rewrite -> (fold_unfold_list_append_nil W (list_map V W f v2s)). - reflexivity. - - intros v2s. - rewrite -> (fold_unfold_list_map_cons V W f v1' v1s'). - rewrite -> (fold_unfold_list_append_cons W (f v1') (list_map V W f v1s')). - rewrite -> (IHv1s' v2s). - rewrite -> (fold_unfold_list_append_cons V v1' v1s'). - rewrite -> (fold_unfold_list_map_cons V W f v1' (list_append V v1s' v2s)). - reflexivity. - Qed. - -(* - h. Do list_map and list_reverse commute with each other and if so how? -*) - -Proposition list_map_and_list_reverse_commute_with_each_other : - forall (V W : Type) - (f : V -> W) - (vs : list V), - list_reverse W (list_map V W f vs) = list_map V W f (list_reverse V vs). -Proof. - intros V W f vs. - induction vs as [ | v vs' IHvs' ]. - - rewrite -> (fold_unfold_list_map_nil V W f). - rewrite -> (fold_unfold_list_reverse_nil V). - rewrite -> (fold_unfold_list_reverse_nil W). - rewrite -> (fold_unfold_list_map_nil V W f). - reflexivity. - - rewrite -> (fold_unfold_list_map_cons V W f v vs'). - rewrite -> (fold_unfold_list_reverse_cons W (f v) (list_map V W f vs')). - rewrite -> IHvs'. - rewrite -> (fold_unfold_list_reverse_cons V v vs'). - rewrite <- (fold_unfold_list_map_nil V W f). - rewrite <- (fold_unfold_list_map_cons V W f v nil). - Check list_map_and_list_append_commute_with_each_other. - rewrite -> (list_map_and_list_append_commute_with_each_other V W f (list_reverse V vs') (v :: nil)). - reflexivity. -Qed. - - - -(* - i. Do list_map and list_reverse_alt commute with each other and if so how? -*) - -Proposition list_map_and_list_reverse_alt_commute_with_each_other : - forall (V W : Type) - (f : V -> W) - (vs : list V), - list_reverse_alt W (list_map V W f vs) = list_map V W f (list_reverse_alt V vs). -Proof. - intros V W f vs. - Check list_reverse_and_list_reverse_alt_equiv. - rewrite <- (list_reverse_and_list_reverse_alt_equiv W (list_map V W f vs)). - rewrite <- (list_reverse_and_list_reverse_alt_equiv V vs). - exact (list_map_and_list_reverse_commute_with_each_other V W f vs). -Qed. - - -(* - j. Define a unit-test function for the map function - and verify that your implementation satisfies it. -*) - -Fixpoint evenp (n : nat): bool := - match n with - | 0 => true - | S n' => match n' with - | 0 => false - | S n'' => evenp n'' - end - end. - -Definition test_list_map (candidate : forall V W : Type, (V -> W) -> list V -> list W) := - (eqb_list nat Nat.eqb (candidate nat nat (fun v => v) nil) nil) && - (eqb_list nat Nat.eqb (candidate nat nat (fun v => v) (1 :: 2:: 3 :: nil)) (1 :: 2 :: 3 :: nil)) && - (eqb_list nat Nat.eqb (candidate nat nat (fun v => S v) (1 :: 2:: 3 :: nil)) (2 :: 3 :: 4 :: nil)) && - (eqb_list bool Bool.eqb (candidate nat bool evenp (1 :: 2:: 3 :: nil)) (false :: true :: false :: nil)). - -Compute test_list_map list_map. - -(* ********** *) - -(* 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. -*) - -Theorem list_fold_left_satisfies_the_specification_of_fold_left : - specification_of_list_fold_left list_fold_left. -Proof. - unfold specification_of_list_fold_left. - split. - - exact fold_unfold_list_fold_left_nil. - - exact fold_unfold_list_fold_left_cons. -Qed. - -Theorem list_fold_right_satisfies_the_specification_of_fold_right : - specification_of_list_fold_right list_fold_right. -Proof. - unfold specification_of_list_fold_right. - split. - - exact fold_unfold_list_fold_right_nil. - - exact fold_unfold_list_fold_right_cons. -Qed. - -(* - 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. - -Compute test_list_copy foo. - -Definition bar (V : Type) (vs : list V) := - list_fold_left V (list V) nil (fun v vs => v :: vs) vs. - -Compute test_list_reverse bar. - -(* - 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. -*) - -Definition list_length_using_list_fold_left (V: Type) (vs : list V): nat := - list_fold_left V nat 0 (fun _ length => S (length)) vs. - -Compute test_list_length list_length_using_list_fold_left. - -(* - 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. -*) - -Definition list_copy_using_list_fold_right (V: Type) (vs : list V): (list V) := - list_fold_right V (list V) nil (fun v acc => v :: acc) vs. - -Compute test_list_copy list_copy_using_list_fold_right. - -(* - 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. -*) -Definition list_append_using_list_fold_right (V: Type) (v1s v2s : list V): (list V) := - list_fold_right V (list V) v2s (fun v acc => v :: acc) v1s. - -Compute test_list_append list_append_using_list_fold_right. - -(* - 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. -*) -Definition list_reverse_using_list_fold_left (V: Type) (vs : list V): (list V) := - list_fold_left V (list V) nil (fun v acc => v :: acc) vs. - -Compute test_list_reverse list_reverse_using_list_fold_left. - -(* - 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. -*) - -Definition list_map_using_list_fold_right (V W: Type) (f : V -> W) (vs : list V): (list W) := - list_fold_right V (list W) nil (fun v w => (f v) :: w) vs. - -Compute test_list_map list_map_using_list_fold_right. - -(* - k. Implement eqb_list either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice. -*) - -(* FIXME: This feels very hacky, because of the match result with, but I have no idea how to consider if the first list finishes iteration, -then the result should be false without the match case outside of the fold function - *) - -Definition eqb_list_using_list_fold_right (V : Type) (eqb_V: V -> V -> bool) (v1s v2s : list V) := - let result := list_fold_left V - (bool * list V) - (true, v2s) - (fun v1 acc => - match acc with - | (false, v2::v2s') => (false, v2s') - | (false, nil) => (false, nil) - | (true, v2::v2s') => (eqb_V v1 v2, v2s') - | (true, nil) => (false, nil) - end) - v1s in - match result with - | (false, _) => false - | (true, nil) => true - | _ => false - end. - -(* TODO Write testcases *) - - -(* - 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 *)