yadunut/nus
1
0
Fork 0
Code Issues Pull Requests Actions Projects Releases Wiki Activity

feat: fix week 3 and add todo

Browse Source
This commit is contained in:
Yadunand Prem 2024-02-14 17:26:21 +08:00
parent 14e3095632
commit bf80245ccf
No known key found for this signature in database
1 changed files with 3 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

55
cs3234/labs/week-03_structural-induction-over-binary-trees.v
View File

@ -199,6 +199,9 @@ Proof.
reflexivity.
- rewrite -> (S_Node V t1 t2).
Check (mirror_is_involutory mirror S_mirror V t1).
(* TODO: Figure this out *)
Abort.
@ -233,60 +236,8 @@ Qed.
(* ********** *)
Definition specification_of_number_of_leaves (number_of_leaves : forall V : Type, binary_tree V -> nat) : Prop :=
(forall (V : Type)
(v : V),
number_of_leaves V (Leaf V v) =
1)
/\
(forall (V : Type)
(t1 t2 : binary_tree V),
number_of_leaves V (Node V t1 t2) =
number_of_leaves V t1 + number_of_leaves V t2).
(* ***** *)
(* Exercise 09b *)
Proposition there_is_at_most_one_number_of_leaves_function :
forall number_of_leaves1 number_of_leaves2 : forall V : Type, binary_tree V -> nat,
specification_of_number_of_leaves number_of_leaves1 ->
specification_of_number_of_leaves number_of_leaves2 ->
forall (V : Type)
(t : binary_tree V),
number_of_leaves1 V t = number_of_leaves2 V t.
Proof.
Abort.
(* ***** *)
Definition specification_of_number_of_nodes (number_of_nodes : forall V : Type, binary_tree V -> nat) : Prop :=
(forall (V : Type)
(v : V),
number_of_nodes V (Leaf V v) =
0)
/\
(forall (V : Type)
(t1 t2 : binary_tree V),
number_of_nodes V (Node V t1 t2) =
S (number_of_nodes V t1 + number_of_nodes V t2)).
(* ***** *)
(* Exercise 09c *)
Proposition there_is_at_most_one_number_of_nodes_function :
forall number_of_nodes1 number_of_nodes2 : forall V : Type, binary_tree V -> nat,
specification_of_number_of_nodes number_of_nodes1 ->
specification_of_number_of_nodes number_of_nodes2 ->
forall (V : Type)
(t : binary_tree V),
number_of_nodes1 V t = number_of_nodes2 V t.
Proof.
Abort.
(* ***** *)
Theorem about_the_relative_number_of_leaves_and_nodes_in_a_tree :
forall number_of_leaves : forall V : Type, binary_tree V -> nat,
specification_of_number_of_leaves number_of_leaves ->