From 39fab726007eb7599b99e2fceab29d422d7ef11d Mon Sep 17 00:00:00 2001
From: Yadunand Prem <yadunand@yadunut.com>
Date: Wed, 15 May 2024 11:56:31 +0800
Subject: [PATCH] feat: add list_copy

---
 cs3234/labs/midterm-project.v | 103 ++++++++++++++++++++++++++++++----
 1 file changed, 93 insertions(+), 10 deletions(-)

diff --git a/cs3234/labs/midterm-project.v b/cs3234/labs/midterm-project.v
index f154988..7baa402 100644
--- a/cs3234/labs/midterm-project.v
+++ b/cs3234/labs/midterm-project.v
@@ -357,44 +357,90 @@ Definition test_list_copy (candidate : forall V : Type, list V -> list V) :=
    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.
-Abort.
-*)
+  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),
+    (vs : list V),
     list_length V (list_copy V vs) = list_length V vs.
 Proof.
-Abort.
-*)
+  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?
@@ -402,6 +448,43 @@ Abort.
       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: *)