yadunut/nus
1
0
Fork 0
Code Issues Pull Requests Actions Projects Releases Wiki Activity
0959069202
nus/cs3234/labs/midterm-project.v
Yadunand Prem 0959069202
feat: sem7
2025-08-10 19:46:26 +08:00

2233 lines
61 KiB
Coq
Raw Blame History

(* 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 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.
intros S_eqb_V.
intros v1s.
induction v1s as [ | v1 v1s' IHv1s' ].
- intros v2s H_eqb_list.
case v2s as [ | v2 v2s' ].
+ reflexivity.
+ rewrite -> fold_unfold_eqb_list_nil in H_eqb_list.
discriminate H_eqb_list.
- intros v2s H_eqb_list.
case v2s as [ | v2 v2s' ].
+ rewrite -> fold_unfold_eqb_list_cons in H_eqb_list.
discriminate H_eqb_list.
+ rewrite -> fold_unfold_eqb_list_cons in H_eqb_list.
Search (_ && _ = true).
destruct (andb_true_iff (eqb_V v1 v2) (eqb_list V eqb_V v1s' v2s')) as [H_tmp _].
destruct (H_tmp H_eqb_list) as [v1_eq_v2 v1s'_eq_v2s'].
rewrite -> (S_eqb_V v1 v2 v1_eq_v2).
rewrite -> (IHv1s' v2s' v1s'_eq_v2s').
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 C_eqb_V v1s.
induction v1s as [ | v1 v1s' IHv1s' ].
- intros v2s H_eqb_list.
case v2s as [ | v2 v2s' ].
+ rewrite -> fold_unfold_eqb_list_nil.
reflexivity.
+ discriminate H_eqb_list.
- intros v2s v1s_eq_v2s.
case v2s as [ | v2 v2s' ].
+ discriminate v1s_eq_v2s.
+ rewrite -> fold_unfold_eqb_list_cons.
injection v1s_eq_v2s as v1_eq_v2 v1s'_eq_v2s'.
Check (C_eqb_V v1 v2 v1_eq_v2).
rewrite -> (C_eqb_V v1 v2 v1_eq_v2).
rewrite -> (IHv1s' v2s' v1s'_eq_v2s').
simpl (true && true).
reflexivity.
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) (acc : nat) : nat :=
match vs with
nil => acc
| v :: vs' =>
list_length_acc V vs' (S acc)
end.
Definition list_length_alt (V : Type) (vs : list V) : nat :=
list_length_acc V vs 0.
Compute (test_list_length list_length_alt).
Lemma fold_unfold_list_length_acc_nil :
forall (V : Type)
(acc : nat),
list_length_acc V nil acc = acc.
Proof.
fold_unfold_tactic list_length_acc.
Qed.
Lemma fold_unfold_list_length_acc_cons :
forall (V : Type)
(v : V)
(vs' : list V)
(acc : nat),
list_length_acc V (v :: vs') acc = list_length_acc V vs' (S acc).
Proof.
fold_unfold_tactic list_length_acc.
Qed.
Lemma about_list_length_acc :
forall (V : Type)
(vs : list V)
(acc : nat),
list_length_acc V vs (S acc) = S (list_length_acc V vs acc).
Proof.
intros V vs.
induction vs as [ | v vs' IHvs' ].
- intro acc.
rewrite ->(fold_unfold_list_length_acc_nil V (S acc)).
rewrite -> (fold_unfold_list_length_acc_nil V acc).
reflexivity.
- intro acc.
rewrite -> (fold_unfold_list_length_acc_cons V v vs' (S acc)).
rewrite -> (IHvs' (S acc)).
rewrite -> (fold_unfold_list_length_acc_cons V v vs' acc).
reflexivity.
Qed.
Theorem list_length_alt_satisfies_the_specification_of_list_length :
specification_of_list_length list_length_alt.
Proof.
unfold specification_of_list_length,list_length_alt.
split.
- intros V.
exact (fold_unfold_list_length_acc_nil V 0).
- intros V v vs'.
rewrite -> (fold_unfold_list_length_acc_cons V v vs' 0).
rewrite -> (about_list_length_acc 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.
*)
(*
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.
(*
c. State its associated fold-unfold lemmas.
*)
Lemma fold_unfold_list_copy_nil :
forall (V : Type),
list_copy V nil = nil.
Proof.
intro V.
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.
intros V v vs.
fold_unfold_tactic list_copy.
Qed.
(*
d. Prove whether your implementation satisfies the specification.
*)
Theorem list_copy_satifies_the_specification_of_list_copy :
specification_of_list_copy list_copy.
Proof.
unfold specification_of_list_copy.
split.
- intro V.
exact (fold_unfold_list_copy_nil V).
- intros V v vs'.
exact (fold_unfold_list_copy_cons V v vs').
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 -> 2 (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 (list_copy V vs')).
rewrite -> IHvs'.
rewrite -> (fold_unfold_list_length_cons V v vs').
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 identity (V : Type) (vs : list V) := vs.
Theorem identity_satisfies_the_specification_of_copy :
specification_of_list_copy identity.
Proof.
unfold specification_of_list_copy.
split.
- intro V.
unfold identity.
reflexivity.
- intros V v vs'.
unfold identity.
reflexivity.
Qed.
Theorem about_list_copy :
forall (V : Type)
(vs : list V),
list_copy V vs = vs.
Proof.
intros V vs.
induction vs as [ | v vs' IHvs'].
- exact (fold_unfold_list_copy_nil V).
- rewrite -> (fold_unfold_list_copy_cons V v vs').
rewrite -> IHvs'.
reflexivity.
Qed.
Theorem identity_and_list_copy_are_equivalent :
forall (V : Type)
(vs : list V),
list_copy V vs = identity V vs.
Proof.
intros V vs.
unfold identity.
exact (about_list_copy V vs).
Qed.
(* ********** *)
(* 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 (2 :: nil) (1 :: nil) ) (2 :: 1 :: nil)) &&
(eqb_list bool Bool.eqb (candidate bool (true :: nil) (false :: nil)) (true :: false :: nil)) &&
(eqb_list nat Nat.eqb (candidate nat (4 :: 3 :: nil) (2 :: 1 :: nil)) (4 :: 3 :: 2 :: 1 :: nil)) &&
(eqb_list bool Bool.eqb (candidate bool (true :: false :: nil) (true :: false :: nil)) (true :: false :: true :: false :: 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.
*)
Theorem fold_unfold_list_append_nil :
forall (V : Type)
(v2s : list V),
list_append V nil v2s = v2s.
Proof.
fold_unfold_tactic list_append.
Qed.
Theorem 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.
split.
- intros V v2s.
exact (fold_unfold_list_append_nil V v2s).
- intros V v1 v1s' v2s.
exact (fold_unfold_list_append_cons V v1 v1s' v2s).
Qed.
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.
unfold specification_of_list_append.
intros V f g [S_f_nil S_f_cons] [S_g_nil S_g_cons] v1s v2s.
induction v1s as [ | v1 v1s' IHv1s' ].
- rewrite -> (S_f_nil V v2s).
rewrite -> (S_g_nil V v2s).
reflexivity.
- rewrite -> (S_f_cons V v1 v1s').
rewrite -> IHv1s'.
rewrite -> (S_g_cons V v1 v1s').
reflexivity.
Qed.
(*
e. Prove whether nil is neutral on the left of list_append.
*)
Theorem nil_is_neutral_on_the_left_of_list_append :
forall (V : Type)
(v2s : list V),
list_append V nil v2s = v2s.
Proof.
intros V v2s.
exact (fold_unfold_list_append_nil V v2s).
Qed.
(*
f. Prove whether nil is neutral on the right of list_append.
*)
Theorem nil_is_neutral_on_the_right_of_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.
*)
Theorem 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 (1 :: nil).
exists (2 :: nil).
rewrite -> (fold_unfold_list_append_cons nat 1 nil (2 :: nil)).
rewrite -> (fold_unfold_list_append_nil nat (2 :: nil)).
rewrite -> (fold_unfold_list_append_cons nat 2 nil (1 :: nil)).
rewrite -> (fold_unfold_list_append_nil nat (1 :: nil)).
unfold not.
intro H_absurd.
discriminate H_absurd.
Qed.
(*
h. Prove whether list_append is associative.
*)
Theorem list_append_is_associative :
forall (V : Type)
(v1s v2s v3s : list V),
list_append V (list_append V v1s v2s) v3s = list_append V v1s (list_append V v2s v3s).
Proof.
intros V v1s v2s v3s.
induction v1s as [ | v1 v1s' IHv1s' ].
- rewrite -> (fold_unfold_list_append_nil V v2s).
rewrite -> (fold_unfold_list_append_nil V (list_append V v2s v3s)).
reflexivity.
- rewrite -> (fold_unfold_list_append_cons V v1 v1s' v2s).
rewrite -> (fold_unfold_list_append_cons V v1 (list_append V v1s' v2s) v3s).
rewrite -> IHv1s'.
rewrite -> (fold_unfold_list_append_cons V v1 v1s' (list_append V v2s v3s)).
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 v2s.
induction v1s as [ | v1 v1s' IHv1s' ].
- rewrite -> (fold_unfold_list_append_nil V v2s).
rewrite -> (fold_unfold_list_length_nil V).
rewrite -> (Nat.add_0_l).
reflexivity.
- rewrite -> (fold_unfold_list_append_cons V v1 v1s').
rewrite -> (fold_unfold_list_length_cons V v1 (list_append V v1s' v2s)).
rewrite -> IHv1s'.
rewrite <- (Nat.add_succ_l (list_length V v1s') (list_length V v2s)).
rewrite -> (fold_unfold_list_length_cons V v1 v1s').
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 v2s.
rewrite -> (about_list_copy V (list_append V v1s v2s)).
rewrite -> (about_list_copy V v1s).
rewrite -> (about_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 (4 :: 3 :: nil)) (3 :: 4 :: nil)) &&
(eqb_list bool Bool.eqb (candidate bool (true :: false :: nil)) (false :: true :: 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 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.
- intro V.
exact (fold_unfold_list_reverse_nil V).
- intros V v vs'.
rewrite -> (fold_unfold_list_reverse_cons V v vs').
exact (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)).
Qed.
(*
e. Prove whether list_reverse is involutory.
*)
Theorem 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).
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).
exact (fold_unfold_list_reverse_nil V).
- 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.
*)
Theorem reversing_a_list_preserves_its_length :
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_length.
rewrite -> (list_append_and_list_length_commute_with_each_other V
(list_reverse V vs')
(v :: nil)).
rewrite -> IHvs'.
rewrite -> (fold_unfold_list_length_cons V v nil).
rewrite -> (fold_unfold_list_length_nil V).
rewrite -> (fold_unfold_list_length_cons V v vs').
Search (_ + 1).
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?
j*)
Theorem list_append_and_list_reverse_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' ]; intro v2s.
- rewrite -> (fold_unfold_list_reverse_nil V).
rewrite -> (nil_is_neutral_on_the_right_of_list_append V (list_reverse V v2s)).
rewrite -> (fold_unfold_list_append_nil V v2s).
reflexivity.
- rewrite -> (fold_unfold_list_reverse_cons V v1 v1s').
rewrite <- (list_append_is_associative V (list_reverse V v2s) (list_reverse V v1s') (v1 :: nil)).
rewrite -> (IHv1s' v2s).
rewrite -> (fold_unfold_list_append_cons V v1 v1s' v2s).
rewrite -> (fold_unfold_list_reverse_cons V v1 (list_append V v1s' v2s)).
reflexivity.
Qed.
(*
h. Implement the reverse function using an accumulator instead of using list_append.
*)
Fixpoint list_reverse_acc (V : Type) (vs : list V) (acc : list V) : 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.
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_acc.
Qed.
Compute test_list_reverse list_reverse_alt.
Lemma about_list_reverse_acc :
forall (V : Type)
(vs acc : list V),
list_reverse_acc V vs acc = list_append V (list_reverse_acc V vs nil) acc.
Proof.
intros V vs.
induction vs as [ | v vs' IHvs' ]; intro acc.
- rewrite -> (fold_unfold_list_reverse_acc_nil V acc).
rewrite -> (fold_unfold_list_reverse_acc_nil V nil).
rewrite -> (nil_is_neutral_on_the_left_of_list_append V acc).
reflexivity.
- rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' acc).
rewrite -> (IHvs' (v :: acc)).
rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
rewrite -> (IHvs' (v :: nil)).
rewrite -> (list_append_is_associative V (list_reverse_acc V vs' nil) (v :: nil) acc).
rewrite -> (fold_unfold_list_append_cons V v nil acc).
rewrite -> (fold_unfold_list_append_nil 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, list_reverse_alt.
intros append S_append.
split.
- intro V.
exact (fold_unfold_list_reverse_acc_nil V nil).
- intros V v vs'.
rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
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)
(v :: nil)
).
exact (about_list_reverse_acc V vs' (v ::nil)).
Qed.
(*
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.
*)
Theorem about_list_reverse_acc_and_cons :
forall (V : Type)
(v : V)
(vs acc : list V),
list_reverse_acc V (list_append V vs (v :: nil)) acc = v :: list_reverse_acc V vs acc.
Proof.
intros V v vs.
induction vs as [ | v' vs' IHvs' ]; intros acc.
- rewrite -> (fold_unfold_list_append_nil V (v :: nil)).
rewrite -> (fold_unfold_list_reverse_acc_cons V v nil acc).
rewrite -> (fold_unfold_list_reverse_acc_nil V (v :: acc)).
rewrite -> (fold_unfold_list_reverse_acc_nil V acc).
reflexivity.
- rewrite -> (fold_unfold_list_append_cons V v' vs' (v :: nil)).
rewrite -> (fold_unfold_list_reverse_acc_cons V v' (list_append V vs' (v :: nil)) acc).
rewrite -> (IHvs' (v' :: acc)).
rewrite -> (fold_unfold_list_reverse_acc_cons V v' vs' acc).
reflexivity.
Qed.
Theorem list_append_and_list_reverse_acc_commute_with_each_other :
forall (V : Type)
(v1s v2s : list V),
list_append V (list_reverse_acc V v2s nil) (list_reverse_acc V v1s nil) = list_reverse_acc V (list_append V v1s v2s) nil.
Proof.
intros V v1s.
induction v1s as [ | v1 v1s' IHv1s' ]; intros v2s.
- rewrite -> (fold_unfold_list_reverse_acc_nil V nil).
rewrite -> (fold_unfold_list_append_nil V v2s).
rewrite -> (nil_is_neutral_on_the_right_of_list_append V (list_reverse_acc V v2s nil)).
reflexivity.
- rewrite -> (fold_unfold_list_reverse_acc_cons V v1 v1s' nil).
rewrite -> (fold_unfold_list_append_cons V v1 v1s' v2s).
rewrite -> (fold_unfold_list_reverse_acc_cons V v1 (list_append V v1s' v2s) nil).
rewrite -> (about_list_reverse_acc V (list_append V v1s' v2s) (v1 :: nil)).
rewrite <- (IHv1s' v2s).
rewrite -> (list_append_is_associative V (list_reverse_acc V v2s nil) (list_reverse_acc V v1s' nil) (v1 :: nil)).
rewrite <- (about_list_reverse_acc V v1s' (v1 :: nil)).
reflexivity.
Qed.
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.
unfold list_reverse_alt.
induction vs as [ | v vs' IHvs' ].
- rewrite -> (fold_unfold_list_reverse_acc_nil V).
reflexivity.
- rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
rewrite -> (about_list_reverse_acc V vs' (v :: nil)).
rewrite <- (list_append_and_list_reverse_acc_commute_with_each_other V (list_reverse_acc V vs' nil) (v :: nil)).
rewrite -> (fold_unfold_list_reverse_acc_cons V v nil nil).
rewrite -> (fold_unfold_list_reverse_acc_nil V (v::nil)).
rewrite -> IHvs'.
rewrite -> (fold_unfold_list_append_cons V v nil vs').
rewrite -> (fold_unfold_list_append_nil V vs').
reflexivity.
Restart.
intros V vs.
unfold list_reverse_alt.
induction vs as [ | v vs' IHvs' ].
- rewrite -> (fold_unfold_list_reverse_acc_nil V).
reflexivity.
- rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
rewrite -> (about_list_reverse_acc V vs' (v :: nil)).
rewrite -> (about_list_reverse_acc_and_cons V v (list_reverse_acc V vs' nil) nil).
rewrite -> IHvs'.
reflexivity.
Qed.
Theorem 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.
unfold list_reverse_alt.
induction vs as [ | v vs' IHvs' ].
- rewrite -> (fold_unfold_list_reverse_acc_nil V nil).
reflexivity.
- rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
rewrite -> (about_list_reverse_acc V vs' (v :: nil)).
Search list_length.
rewrite -> (list_append_and_list_length_commute_with_each_other V (list_reverse_acc V vs' nil) (v :: nil)).
rewrite -> IHvs'.
rewrite -> (fold_unfold_list_length_cons V v nil).
rewrite -> (fold_unfold_list_length_nil V).
rewrite -> (fold_unfold_list_length_cons V v vs').
rewrite -> (Nat.add_1_r (list_length V vs')).
reflexivity.
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 S_list_map1 S_list_map2 V W f vs.
induction vs as [ | v vs' IHvs'].
- unfold specification_of_list_map in S_list_map1.
destruct S_list_map1 as [fold_unfold_list_map1_nil _].
destruct S_list_map2 as [fold_unfold_list_map2_nil _].
rewrite -> (fold_unfold_list_map2_nil V W f).
exact (fold_unfold_list_map1_nil V W f).
- unfold specification_of_list_map in S_list_map1.
destruct S_list_map1 as [_ fold_unfold_list_map1_cons].
destruct S_list_map2 as [_ fold_unfold_list_map2_cons].
rewrite -> (fold_unfold_list_map1_cons V W f v vs').
rewrite -> (fold_unfold_list_map2_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 i => i) vs.
Compute test_list_copy list_copy_as_list_map.
(*
Hint: Does list_copy_as_list_map satisfy the specification of list_copy?
*)
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, list_copy_as_list_map.
split.
- intros V.
exact (fold_unfold_list_map_nil V V (fun i => i)).
- intros V v vs'.
rewrite -> (fold_unfold_list_map_cons V V (fun i => i) v vs').
reflexivity.
Qed.
(*
f. Prove whether mapping a function over a list preserves the length of this list.
*)
Theorem 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 W).
rewrite -> (fold_unfold_list_length_nil V).
reflexivity.
- 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?
*)
Theorem 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 v2s.
induction v1s as [ | v1 v1s' IHv1s' ].
- rewrite (fold_unfold_list_map_nil V W f).
rewrite -> (nil_is_neutral_on_the_left_of_list_append W (list_map V W f v2s)).
rewrite -> (nil_is_neutral_on_the_left_of_list_append V v2s).
reflexivity.
- 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') (list_map V W f v2s)).
rewrite -> IHv1s'.
rewrite -> (fold_unfold_list_append_cons V v1 v1s' v2s).
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?
*)
Theorem 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 W).
rewrite -> (fold_unfold_list_reverse_nil V).
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 -> (fold_unfold_list_reverse_cons V v vs').
rewrite -> IHvs'.
Search list_reverse.
rewrite <- (list_map_and_list_append_commute_with_each_other V W f (list_reverse V vs') (v :: nil)).
rewrite -> (fold_unfold_list_map_cons V W f v nil).
rewrite -> (fold_unfold_list_map_nil V W f).
reflexivity.
Qed.
(*
i. Do list_map and list_reverse_alt commute with each other and if so how?
*)
Theorem 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.
unfold list_reverse_alt.
induction vs as [ | v vs' IHvs' ].
- rewrite -> (fold_unfold_list_map_nil V W f).
rewrite -> (fold_unfold_list_reverse_acc_nil W nil).
rewrite -> (fold_unfold_list_reverse_acc_nil V nil).
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_acc_cons W (f v) (list_map V W f vs')).
rewrite -> (fold_unfold_list_reverse_acc_cons V v vs' nil).
rewrite -> (about_list_reverse_acc V vs' (v :: nil)).
rewrite <- (list_map_and_list_append_commute_with_each_other V W f (list_reverse_acc V vs' nil) (v::nil)).
rewrite -> (fold_unfold_list_map_cons V W f v nil).
rewrite -> (fold_unfold_list_map_nil V W f).
rewrite <- IHvs'.
rewrite <- (about_list_reverse_acc W (list_map V W f vs') (f v :: nil)).
reflexivity.
Qed.
(*
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.
*)
Theorem list_fold_right_satisfies_the_specification_of_list_fold_right :
specification_of_list_fold_right list_fold_right.
Proof.
unfold specification_of_list_fold_right.
split.
- intros V W nil_case cons_case.
exact (fold_unfold_list_fold_right_nil V W nil_case cons_case).
- intros V W nil_case cons_case v vs'.
exact (fold_unfold_list_fold_right_cons V W nil_case cons_case v vs').
Qed.
Theorem list_fold_left_satisfies_the_specification_of_list_fold_left :
specification_of_list_fold_left list_fold_left.
Proof.
unfold specification_of_list_fold_left.
split.
- intros V W nil_case cons_case.
exact (fold_unfold_list_fold_left_nil V W nil_case cons_case).
- intros V W nil_case cons_case v vs'.
exact (fold_unfold_list_fold_left_cons V W nil_case cons_case v vs').
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_as_list_fold_right (V : Type) (vs : list V) :=
list_fold_right V nat 0 (fun _ acc => S acc) vs.
Compute test_list_length list_length_as_list_fold_right.
Theorem list_length_as_list_fold_right_satisfies_the_specification_of_list_length :
specification_of_list_length list_length_as_list_fold_right.
Proof.
unfold specification_of_list_length, list_length_as_list_fold_right.
split.
- intro V.
rewrite -> (fold_unfold_list_fold_right_nil V nat 0 (fun v acc => S acc)).
reflexivity.
- intros V v vs'.
rewrite -> (fold_unfold_list_fold_right_cons V nat 0 (fun v acc => S acc) v vs').
reflexivity.
Qed.
Definition list_length_as_list_fold_left (V : Type) (vs : list V) :=
list_fold_left V nat 0 (fun _ acc => S acc) vs.
Compute test_list_length list_length_as_list_fold_left.
Lemma about_list_length_and_list_fold_left :
forall (V : Type)
(vs : list V)
(acc : nat)
(f : V -> nat -> nat),
(f = fun (_: V) (acc: nat) => S acc) ->
list_fold_left V nat (S acc) f vs =
S (list_fold_left V nat acc f vs).
Proof.
intros V vs acc f S_f.
revert acc.
induction vs as [ | v vs' IHvs' ]; intro acc.
- rewrite -> (fold_unfold_list_fold_left_nil V nat acc f).
exact (fold_unfold_list_fold_left_nil V nat (S acc) f).
- rewrite -> (fold_unfold_list_fold_left_cons V nat (S acc) f v vs').
rewrite -> (fold_unfold_list_fold_left_cons V nat acc f v vs').
rewrite -> S_f.
rewrite <- S_f.
rewrite -> (IHvs' (S acc)).
reflexivity.
Qed.
Lemma about_list_length_and_list_fold_left_alt :
forall (V : Type)
(vs : list V)
(acc : nat),
list_fold_left V nat (S acc) (fun (_: V) (acc: nat) => S acc) vs =
S (list_fold_left V nat acc (fun (_: V) (acc: nat) => S acc) vs).
Proof.
intros V vs.
induction vs as [ | v vs' IHvs' ]; intro acc.
- rewrite -> (fold_unfold_list_fold_left_nil V nat acc (fun v acc => S acc)).
exact (fold_unfold_list_fold_left_nil V nat (S acc) (fun v acc => S acc)).
- rewrite -> (fold_unfold_list_fold_left_cons V nat (S acc) (fun v acc => S acc) v vs').
rewrite -> (fold_unfold_list_fold_left_cons V nat acc (fun v acc => S acc) v vs').
rewrite -> (IHvs' (S acc)).
reflexivity.
Qed.
Theorem list_length_as_list_fold_left_satisfies_the_specification_of_list_length :
specification_of_list_length list_length_as_list_fold_left.
Proof.
unfold specification_of_list_length, list_length_as_list_fold_left.
split.
- intro V.
rewrite -> (fold_unfold_list_fold_left_nil V nat 0 (fun v acc => S acc)).
reflexivity.
- intros V v vs'.
remember (fun (_: V) (acc: nat) => S acc) as f eqn:H_f.
rewrite -> (fold_unfold_list_fold_left_cons V nat 0 f v vs').
rewrite -> H_f.
rewrite <- H_f.
exact (about_list_length_and_list_fold_left V vs' 0 f H_f).
Restart.
unfold specification_of_list_length, list_length_as_list_fold_left.
split.
- intro V.
rewrite -> (fold_unfold_list_fold_left_nil V nat 0 (fun v acc => S acc)).
reflexivity.
- intros V v vs'.
rewrite -> (fold_unfold_list_fold_left_cons V nat 0 (fun v acc => S acc) v vs').
exact (about_list_length_and_list_fold_left_alt V vs' 0).
Qed.
(*
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_as_list_fold_right (V : Type) (vs : list V) :=
list_fold_right V (list V) nil (fun v acc => v :: acc) vs.
Compute test_list_copy list_copy_as_list_fold_right.
Theorem list_copy_as_list_fold_right_satisfies_the_specification_of_list_copy :
specification_of_list_copy list_copy_as_list_fold_right.
Proof.
unfold specification_of_list_copy, list_copy_as_list_fold_right.
split.
- intros V.
remember (fun v acc => v :: acc) as f eqn:H_f.
exact (fold_unfold_list_fold_right_nil V (list V) nil f).
- intros V v vs'.
remember (fun v acc => v :: acc) as f eqn:H_f.
rewrite -> (fold_unfold_list_fold_right_cons V (list V) nil f v vs').
rewrite -> H_f.
reflexivity.
Qed.
Definition list_copy_as_list_fold_left (V : Type) (vs : list V) :=
list_fold_left V (list V) nil (fun v acc => list_append V acc (v :: nil)) vs.
Lemma about_list_copy_and_list_fold_left :
forall (V : Type)
(v : V)
(vs acc : list V)
(f : V -> list V -> list V),
(f = (fun (v : V) (acc : list V) => list_append V acc (v :: nil))) ->
list_fold_left V (list V) (v :: acc) f vs = v :: list_fold_left V (list V) acc f vs.
Proof.
intros V v vs acc f H_f.
revert acc.
induction vs as [ | v' vs' IHvs' ];intros acc.
- rewrite -> (fold_unfold_list_fold_left_nil V (list V) (v :: acc) f).
rewrite -> (fold_unfold_list_fold_left_nil V (list V) acc f).
reflexivity.
- rewrite -> (fold_unfold_list_fold_left_cons V (list V) (v :: acc) f v' vs').
rewrite -> H_f.
rewrite <- H_f.
rewrite -> (fold_unfold_list_append_cons V v acc (v' :: nil)).
rewrite -> (IHvs' (list_append V acc (v' :: nil))).
rewrite -> (fold_unfold_list_fold_left_cons V (list V) acc f v' vs').
rewrite -> H_f.
rewrite <- H_f.
reflexivity.
Qed.
Theorem list_copy_as_list_fold_left_satisfies_the_specification_of_list_copy :
specification_of_list_copy list_copy_as_list_fold_left.
Proof.
unfold specification_of_list_copy, list_copy_as_list_fold_left.
split.
- intros V.
remember (fun v acc => list_append V acc (v :: nil)) as f eqn:H_f.
exact (fold_unfold_list_fold_left_nil V (list V) nil f).
- intros V v vs'.
remember (fun v acc => list_append V acc (v :: nil)) as f eqn:H_f.
rewrite -> (fold_unfold_list_fold_left_cons V (list V) nil f v vs').
rewrite -> H_f.
rewrite <- H_f.
rewrite -> (fold_unfold_list_append_nil V (v :: nil)).
exact (about_list_copy_and_list_fold_left V v vs' nil f H_f).
Qed.
Compute test_list_copy list_copy_as_list_fold_left.
(*
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.
*)
(* 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. *)
Definition list_append_as_list_fold_right (V : Type) (v1s v2s : list V) : list V :=
list_fold_right V (list V) v2s (fun v ih => v :: ih) v1s.
Compute test_list_append list_append_as_list_fold_right.
Theorem list_append_as_list_fold_right_satsifies_the_specification_of_list_append :
specification_of_list_append list_append_as_list_fold_right.
Proof.
unfold specification_of_list_append, list_append_as_list_fold_right.
split.
- intros V v2s.
remember (fun v ih => v :: ih) as f eqn:H_f.
exact (fold_unfold_list_fold_right_nil V (list V) v2s f).
- intros V v1 v1s' v2s.
remember (fun v ih => v :: ih) as f eqn:H_f.
rewrite -> (fold_unfold_list_fold_right_cons V (list V) v2s f v1 v1s').
rewrite -> H_f.
reflexivity.
Qed.
(* This is very very wrong, but I'm giving up for now *)
Definition list_append_as_list_fold_left (V : Type) (v1s v2s : list V) : list V :=
list_fold_left V (list V) v1s (fun v acc => v::acc) v2s.
Compute list_append_as_list_fold_left nat (1 :: 2 :: nil) (3 :: 4 :: nil).
Compute test_list_append list_append_as_list_fold_left.
(*
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_as_list_fold_left (V: Type) (vs : list V) : list V :=
list_fold_left V (list V) nil (fun v acc => v :: acc) vs.
Compute list_reverse_as_list_fold_left nat (1 :: 2 :: nil).
Compute test_list_reverse list_reverse_as_list_fold_left.
Theorem list_reverse_as_list_fold_left_satsifies_the_specification_of_list_reverse:
specification_of_list_reverse list_reverse_as_list_fold_left.
Proof.
unfold specification_of_list_reverse, list_reverse_as_list_fold_left.
intros append S_append.
split.
- intros V.
remember (fun v acc => v :: acc) as f eqn:H_f.
exact (fold_unfold_list_fold_left_nil V (list V) nil f).
- intros V v vs'.
remember (fun v acc => v :: acc) as f eqn:H_f.
rewrite -> (fold_unfold_list_fold_left_cons V (list V) nil f v vs').
split.
Qed.
(*
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 *)
Reference in New Issue View Git Blame Copy Permalink