From 095906920251ef3aaa840b60598d1709388d1199 Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Sun, 10 Aug 2025 19:46:26 +0800 Subject: [PATCH] feat: sem7 --- .gitignore | 10 ++ .gitmodules | 3 + cs3234/labs/midterm-project.v | 131 +++++++++++++++++++++ cs3234/labs/week-11_induction-principles.v | 35 +++++- cs4212/week-01-simple-2025 | 1 + devenv.lock | 103 ++++++++++++++++ devenv.nix | 5 + devenv.yaml | 15 +++ 8 files changed, 302 insertions(+), 1 deletion(-) create mode 100644 .gitmodules create mode 160000 cs4212/week-01-simple-2025 create mode 100644 devenv.lock create mode 100644 devenv.nix create mode 100644 devenv.yaml diff --git a/.gitignore b/.gitignore index ac5648f..d3d626d 100644 --- a/.gitignore +++ b/.gitignore @@ -632,3 +632,13 @@ cs2109s/labs/ps6/MNIST/raw cs2109s/labs/ps7/MNIST/raw cs2109s/labs/.idea cs2109s/labs/ps7/cifar-10-batches-py + +# Devenv +.devenv* +devenv.local.nix + +# direnv +.direnv + +# pre-commit +.pre-commit-config.yaml diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..fdbbb12 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "cs4212/week-01-simple-2025"] + path = cs4212/week-01-simple-2025 + url = https://github.com/cs4212/week-01-simple-2025 diff --git a/cs3234/labs/midterm-project.v b/cs3234/labs/midterm-project.v index 37ac907..4dfd5ae 100644 --- a/cs3234/labs/midterm-project.v +++ b/cs3234/labs/midterm-project.v @@ -1510,19 +1510,150 @@ 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. *) +Definition list_copy_as_list_fold_right (V : Type) (vs : list V) := + list_fold_right V (list V) nil (fun v acc => v :: acc) vs. + +Compute test_list_copy list_copy_as_list_fold_right. + +Theorem list_copy_as_list_fold_right_satisfies_the_specification_of_list_copy : + specification_of_list_copy list_copy_as_list_fold_right. +Proof. + unfold specification_of_list_copy, list_copy_as_list_fold_right. + split. + - intros V. + remember (fun v acc => v :: acc) as f eqn:H_f. + exact (fold_unfold_list_fold_right_nil V (list V) nil f). + - intros V v vs'. + remember (fun v acc => v :: acc) as f eqn:H_f. + rewrite -> (fold_unfold_list_fold_right_cons V (list V) nil f v vs'). + rewrite -> H_f. + reflexivity. +Qed. + +Definition list_copy_as_list_fold_left (V : Type) (vs : list V) := + list_fold_left V (list V) nil (fun v acc => list_append V acc (v :: nil)) vs. + +Lemma about_list_copy_and_list_fold_left : + forall (V : Type) + (v : V) + (vs acc : list V) + (f : V -> list V -> list V), + (f = (fun (v : V) (acc : list V) => list_append V acc (v :: nil))) -> + list_fold_left V (list V) (v :: acc) f vs = v :: list_fold_left V (list V) acc f vs. +Proof. + intros V v vs acc f H_f. + revert acc. + induction vs as [ | v' vs' IHvs' ];intros acc. + - rewrite -> (fold_unfold_list_fold_left_nil V (list V) (v :: acc) f). + rewrite -> (fold_unfold_list_fold_left_nil V (list V) acc f). + reflexivity. + - rewrite -> (fold_unfold_list_fold_left_cons V (list V) (v :: acc) f v' vs'). + rewrite -> H_f. + rewrite <- H_f. + rewrite -> (fold_unfold_list_append_cons V v acc (v' :: nil)). + rewrite -> (IHvs' (list_append V acc (v' :: nil))). + rewrite -> (fold_unfold_list_fold_left_cons V (list V) acc f v' vs'). + rewrite -> H_f. + rewrite <- H_f. + reflexivity. +Qed. + +Theorem list_copy_as_list_fold_left_satisfies_the_specification_of_list_copy : + specification_of_list_copy list_copy_as_list_fold_left. +Proof. + unfold specification_of_list_copy, list_copy_as_list_fold_left. + split. + - intros V. + remember (fun v acc => list_append V acc (v :: nil)) as f eqn:H_f. + exact (fold_unfold_list_fold_left_nil V (list V) nil f). + - intros V v vs'. + remember (fun v acc => list_append V acc (v :: nil)) as f eqn:H_f. + rewrite -> (fold_unfold_list_fold_left_cons V (list V) nil f v vs'). + rewrite -> H_f. + rewrite <- H_f. + rewrite -> (fold_unfold_list_append_nil V (v :: nil)). + exact (about_list_copy_and_list_fold_left V v vs' nil f H_f). +Qed. + +Compute test_list_copy list_copy_as_list_fold_left. (* h. Implement the append function either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice. *) +(* 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. *) + +Definition list_append_as_list_fold_right (V : Type) (v1s v2s : list V) : list V := + list_fold_right V (list V) v2s (fun v ih => v :: ih) v1s. + +Compute test_list_append list_append_as_list_fold_right. + +Theorem list_append_as_list_fold_right_satsifies_the_specification_of_list_append : + specification_of_list_append list_append_as_list_fold_right. +Proof. + unfold specification_of_list_append, list_append_as_list_fold_right. + split. + - intros V v2s. + remember (fun v ih => v :: ih) as f eqn:H_f. + exact (fold_unfold_list_fold_right_nil V (list V) v2s f). + - intros V v1 v1s' v2s. + remember (fun v ih => v :: ih) as f eqn:H_f. + rewrite -> (fold_unfold_list_fold_right_cons V (list V) v2s f v1 v1s'). + rewrite -> H_f. + reflexivity. +Qed. + +(* This is very very wrong, but I'm giving up for now *) +Definition list_append_as_list_fold_left (V : Type) (v1s v2s : list V) : list V := + list_fold_left V (list V) v1s (fun v acc => v::acc) v2s. + +Compute list_append_as_list_fold_left nat (1 :: 2 :: nil) (3 :: 4 :: nil). + +Compute test_list_append list_append_as_list_fold_left. + + + + (* i. Implement the reverse function either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice. *) +Definition list_reverse_as_list_fold_left (V: Type) (vs : list V) : list V := + list_fold_left V (list V) nil (fun v acc => v :: acc) vs. + +Compute list_reverse_as_list_fold_left nat (1 :: 2 :: nil). + +Compute test_list_reverse list_reverse_as_list_fold_left. + +Theorem list_reverse_as_list_fold_left_satsifies_the_specification_of_list_reverse: + specification_of_list_reverse list_reverse_as_list_fold_left. +Proof. + unfold specification_of_list_reverse, list_reverse_as_list_fold_left. + intros append S_append. + split. + - intros V. + remember (fun v acc => v :: acc) as f eqn:H_f. + exact (fold_unfold_list_fold_left_nil V (list V) nil f). + - intros V v vs'. + remember (fun v acc => v :: acc) as f eqn:H_f. + rewrite -> (fold_unfold_list_fold_left_cons V (list V) nil f v vs'). + + split. + + Qed. + (* j. Implement the map function either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice. *) + (* k. Implement eqb_list either as an instance of list_fold_right or as an instance of list_fold_left, and justify your choice. *) diff --git a/cs3234/labs/week-11_induction-principles.v b/cs3234/labs/week-11_induction-principles.v index 12e6c99..04307a3 100644 --- a/cs3234/labs/week-11_induction-principles.v +++ b/cs3234/labs/week-11_induction-principles.v @@ -247,6 +247,28 @@ Proof. induction n as [ | [ | n''] IHn']. Abort. +Lemma nat_ind2 : + forall P : nat -> Prop, + P 0 -> + P 1 -> + (forall k : nat, P k -> P (S k) -> P (S (S k))) -> + forall n : nat, P n. +Proof. + intros P H_P0 H_P1 H_PSS [ | [ | n'' ] ]. + - exact H_P0. + - exact H_P1. + - assert (both : forall m : nat, P m /\ P(S m)). + { intro m. + induction m as [ | m' [ IHm' IHSm' ] ]. + - exact (conj H_P0 H_P1). + - split. + + exact IHSm'. + + exact (H_PSS m' IHm' IHSm' ). + } + destruct (both n'') as [Pn'' PSn'']. + exact (H_PSS n'' Pn'' PSn''). +Qed. + (* Thus equipped, the following theorem is proved pretty directly: *) Theorem there_is_at_most_one_fibonacci_function : @@ -262,7 +284,18 @@ Proof. [H_fib2_0 [H_fib2_1 H_fib2_SS]] n. induction n as [ | | n'' IHn'' IHSn''] using nat_ind2. -Abort. + - rewrite -> H_fib1_0. + rewrite -> H_fib2_0. + reflexivity. + - rewrite -> H_fib1_1. + rewrite -> H_fib2_1. + reflexivity. + - rewrite -> (H_fib1_SS n''). + rewrite -> (H_fib2_SS n''). + rewrite -> IHn''. + rewrite -> IHSn''. + reflexivity. +Qed. (* ***** *) diff --git a/cs4212/week-01-simple-2025 b/cs4212/week-01-simple-2025 new file mode 160000 index 0000000..9ef6c44 --- /dev/null +++ b/cs4212/week-01-simple-2025 @@ -0,0 +1 @@ +Subproject commit 9ef6c4412425b9b537139ba7a5b1aada9a307896 diff --git a/devenv.lock b/devenv.lock new file mode 100644 index 0000000..4d958ed --- /dev/null +++ b/devenv.lock @@ -0,0 +1,103 @@ +{ + "nodes": { + "devenv": { + "locked": { + "dir": "src/modules", + "lastModified": 1754141078, + "owner": "cachix", + "repo": "devenv", + "rev": "a21413b7977726581d26951da25d4c31235c3253", + "type": "github" + }, + "original": { + "dir": "src/modules", + "owner": "cachix", + "repo": "devenv", + "type": "github" + } + }, + "flake-compat": { + "flake": false, + "locked": { + "lastModified": 1747046372, + "owner": "edolstra", + "repo": "flake-compat", + "rev": "9100a0f413b0c601e0533d1d94ffd501ce2e7885", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", + "type": "github" + } + }, + "git-hooks": { + "inputs": { + "flake-compat": "flake-compat", + "gitignore": "gitignore", + "nixpkgs": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1750779888, + "owner": "cachix", + "repo": "git-hooks.nix", + "rev": "16ec914f6fb6f599ce988427d9d94efddf25fe6d", + "type": "github" + }, + "original": { + "owner": "cachix", + "repo": "git-hooks.nix", + "type": "github" + } + }, + "gitignore": { + "inputs": { + "nixpkgs": [ + "git-hooks", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1709087332, + "owner": "hercules-ci", + "repo": "gitignore.nix", + "rev": "637db329424fd7e46cf4185293b9cc8c88c95394", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "gitignore.nix", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1753719760, + "owner": "cachix", + "repo": "devenv-nixpkgs", + "rev": "0f871fffdc0e5852ec25af99ea5f09ca7be9b632", + "type": "github" + }, + "original": { + "owner": "cachix", + "ref": "rolling", + "repo": "devenv-nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "devenv": "devenv", + "git-hooks": "git-hooks", + "nixpkgs": "nixpkgs", + "pre-commit-hooks": [ + "git-hooks" + ] + } + } + }, + "root": "root", + "version": 7 +} diff --git a/devenv.nix b/devenv.nix new file mode 100644 index 0000000..822a1ae --- /dev/null +++ b/devenv.nix @@ -0,0 +1,5 @@ +{ pkgs, lib, config, inputs, ... }: + +{ + packages = [ pkgs.git pkgs.opam pkgs.typst ]; +} diff --git a/devenv.yaml b/devenv.yaml new file mode 100644 index 0000000..116a2ad --- /dev/null +++ b/devenv.yaml @@ -0,0 +1,15 @@ +# yaml-language-server: $schema=https://devenv.sh/devenv.schema.json +inputs: + nixpkgs: + url: github:cachix/devenv-nixpkgs/rolling + +# If you're using non-OSS software, you can set allowUnfree to true. +# allowUnfree: true + +# If you're willing to use a package that's vulnerable +# permittedInsecurePackages: +# - "openssl-1.1.1w" + +# If you have more than one devenv you can merge them +#imports: +# - ./backend