From 553439bba71646bf8107c14cf85c09d9d355e4be Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Sat, 2 Mar 2024 15:17:54 +0800 Subject: [PATCH] feat: 3234 more functions --- cs3234/labs/midterm_project.v | 167 ++++++++++++++++++++++++++++++++-- ma1522/1522 Notes.pdf | Bin 119191 -> 119191 bytes 2 files changed, 160 insertions(+), 7 deletions(-) diff --git a/cs3234/labs/midterm_project.v b/cs3234/labs/midterm_project.v index f7ce432..9bc7bfc 100644 --- a/cs3234/labs/midterm_project.v +++ b/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? *) diff --git a/ma1522/1522 Notes.pdf b/ma1522/1522 Notes.pdf index b9cec555d7762ab97cab549d329e405f97282d1a..2129b6f2a1845210350b9500e8595d4326d9d5b7 100644 GIT binary patch delta 673 zcmV;S0$%->qX(Cx2Y|Ez^n`zs)lvCRmHHF@z05qm`E~p5^R&?_k9~i6_q0j!e0_hj zz4+(j_M7)lZ|~kgyuV-l0*jg4&0I{k_j@wY!A^roEni$cUA?{kNpgZu4NZCvC^aAX zI{#U9+DDf)_1g3QG8H|e!Emnh7EN+8wHTKXtEQ{;u3HG3PcAvN*R6j)n>vN(qLYuv zC_E=wy_Ju=)*}dgispnoWq`o);*UZTg!9w@I8HAl$ z=?#-2EA$~>huKt+0vciL-m!O-*RkZGFqht6k@ryKoi~f^0;i7CqWhOO+(2nF+5XUK zOCM;D)PM56QvPpuH5-5G->q$_{_sCoQ2aymleXPqCXc-2*80>GLZT2-4hbf7Ifb-? zcAi)9*wm_6)|1zu_hMMfrB+5>`NE#k0fZSW!qduAnI^jz?TPp(FNdV`m7UzD&l+PN zDSc*;)zSn3JG9{EcSA}OjsMHs)|$Di99Ww6;eG0#_)mH-L=At7PkNg~^qK$vy?;ap zMy_rdEvmQb6iPNBwkDerIU_wY8VnBFU&`ylmc6KMW9+5VcEcKemL6f=u)CC3-O}B7 zDOtwKh%+0@mtOgl5R#WTc>_6}ZyeT(PUM9SZ_}3nMpgydc)E06-X1j@&p_e)5KY*4 zFO1XTps+`^JDNfsVIbT?xRgbaE^XvZwAfT4Ke@~WX57Fqmt_&o0WQ4{7>515n1myu zEHlVpUm%j==!ERByRS)TZ8o3$58Wa0K9>O!0TZ`HhXD#jK{+{PVmCKpIAbzlW;kXr zV`elrWo9#EW;rx9W@0flVm>@MIb~uuH)1$rGGS&oW-w!BG&f~tGh}8tG&N>oF*Uc4 H%mD`l?>bA< delta 673 zcmV;S0$%->qX(Cx2Y|Ez^n`z4%Ni+ss??wG?`7uk&9B>cpQnvhdF=bkyQfW(=j;2M z?ZrPIx8J;fdVBW{;{E;V7g)^XZsuaTz2B3G4t5$$YWd>o>FVwMPm&XSYG~4XK&ko2 z*ZI$?(>}Vasn?$Wm#OF(4Tf{2w`h`+sl~XAST$XxcilqRd~(UDy>5T~+0-dK7oB`W zM&UWh>aBd_wH`s}Q#2>!DFXzS7k?C*Ae^TLz;SvZNuI7u^IWnLMs+wutMeN)lEbl0 zPj8qMS)mX4I?Sem6wnA`_l~`zypAOgg}LdpS0}`GkN4Cx7Meo5E6xua!4?t%PFKC zwDY`*$EH@rvYxyKy%)n;F10f9$`|&O4j{~65uR3_$~4)%XivmPc{wDduk7SLebyNJ zNa-_!td=GS*r5eKzZ+7TX#8L1w${vD<-pRk5ARd|#DCIzA!>hEeA3$_qR;&Q@BJe> zFmiRvXi>dYr%wj0*)v-Ak_hTWyS>Xz=t zOUW`;Mx5DLzVyncgpj<%$s5S&eB-cQbRsWwc$>ZqFtRGp#?z(q^7g3Ncm@jRhiJma zdtsaw2ZcSV-O)ny2m|3B!lf*VbZH}RqQ#~X`N?H2FyjV>xh#ut4shvxz%cCZ#UvaN zWtl++`vQ>^M<-;5-F;0$YqR;}e*nnwLze*(0TZ`HhXD#jK{#eOI5##oF=b(8Vl*>k zV`O48IAb_DGBGw`GB;#oVm>@LW;i%EHa9V4VP#@8Gh}0AVly~nI5{#gHeoV1WMsFH H%mD`loI+VZ