feat: 3234 more functions

cs3234/labs/midterm_project.v

@@ -920,10 +920,14 @@ Proof.
    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)
@@ -934,6 +938,93 @@ Definition list_reverse_alt (V : Type) (vs : list V) : list V :=
       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 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.
+  intros [S_append_nil S_append_cons].
+  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).
+    induction vs as [ | v' vs' IHvs' ].
+    + rewrite -> (fold_unfold_list_reverse_acc_nil V (v :: nil)).
+      rewrite -> (fold_unfold_list_reverse_acc_nil V nil).
+      rewrite -> (S_append_nil V (v :: nil)).
+      reflexivity.
+    + rewrite -> (fold_unfold_list_reverse_acc_cons V v' vs' (v :: nil)).
+      rewrite -> (fold_unfold_list_reverse_acc_cons V v' vs' nil).
+      Search list_append.
+Abort.
+
+(* Theorem about_list_reverse_acc_and_list_append : *)
+(*   forall append : forall W : Type, list W -> list W -> list W, *)
+(*     specification_of_list_append append -> *)
+(*     forall (V: Type) *)
+(*       (acc acc' vs : list V), *)
+(*       list_reverse_acc V vs (append V acc acc') = append V (list_reverse_acc V vs acc) acc'. *)
+(* Proof. *)
+(*   intros append [S_append_nil S_append_cons]. *)
+(*   intros V acc acc' vs. *)
+(*   revert acc' vs. *)
+(*   induction acc as [ | v acc'' IHacc'']. *)
+(*   - intros acc' vs. *)
+(*     rewrite -> (S_append_nil V acc'). *)
+(*     Check (fold_unfold_list_reverse_acc_nil). *)
+
+(* reverse vs (append acc acc') = append (reverse vs acc) acc' *)
+(* reverse vs (a :: b :: nil) = [reverse vs (a :: nil)] (b :: nil) *)
+(* reverse abc nil
+= reverse bc [a, nil]
+= reverse c [b, a, nil]
+= reverse nil [c, b, a, nil]
+ *)
+
+
+
+(* Lemma about_list_append : *)
+(*   forall append : forall W : list W -> list W -> list W, *)
+(*     specification_of_list_append append -> *)
+(*     (V : Type) *)
+(*       (v v' : V) *)
+(*       append V *)
+
+(* Definition there_is_at_most_one_list_reverse_function : *)
+(*   forall (V : Type) *)
+(*     (f g : forall V : Type, list V -> list V), *)
+(*     specification_of_list_reverse f -> *)
+(*     specification_of_list_reverse g -> *)
+(*     forall vs : list V, *)
+(*       f V vs = g V vs. *)
+(* Proof. *)
+(*   intros V. *)
+(*   intros f g S_f S_g. *)
+(*   intros vs. *)
+
+
 (* ********** *)
 
 (* A study of the polymorphic map function: *)
@@ -965,7 +1056,18 @@ Proposition there_is_at_most_one_list_map_function :
              (vs : list V),
         list_map1 V W f vs = list_map2 V W f vs.
 Proof.
-Abort.
+  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.
@@ -1018,10 +1120,22 @@ 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.
+    rewrite -> (fold_unfold_list_map_cons V V (fun v => v) v vs).
+    reflexivity.
+Qed.
 
 (*
 Hint: Does list_copy_as_list_map satisfy the specification of list_copy?
@@ -1030,11 +1144,50 @@ 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?
 *)