From 1b0b39802aa0564ae6f8df05360c8b573e564a5a Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Mon, 20 May 2024 00:43:09 +0800 Subject: [PATCH] feat: list_length with fold left and right --- cs3234/labs/midterm-project.v | 118 ++++++++++++++++++++++++++++++++-- 1 file changed, 114 insertions(+), 4 deletions(-) diff --git a/cs3234/labs/midterm-project.v b/cs3234/labs/midterm-project.v index ef3587d..37ac907 100644 --- a/cs3234/labs/midterm-project.v +++ b/cs3234/labs/midterm-project.v @@ -1379,24 +1379,134 @@ 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. *)