feat: add list append

cs3234/labs/midterm-project.v

@@ -506,65 +506,171 @@ Definition specification_of_list_append (append : forall V : Type, list V -> lis
 (*
    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.
 
 (*
    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_astisfies_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.
 (*
    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),
+    (v1s v2s : list V),
     list_length V (list_append V v1s v2s) = list_length V v1s + list_length V v2s.
 Proof.
-Abort.
+  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.
-Abort.
+  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.
 
 (* ********** *)