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

feat: fix week 3

Browse Source
This commit is contained in:
Yadunand Prem 2024-02-15 16:16:09 +08:00
parent 7ef2e570ea
commit 7cdb61b354
No known key found for this signature in database
1 changed files with 4 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -197,24 +197,11 @@ Proof.
- rewrite <- M_t_t'. - rewrite <- M_t_t'.
rewrite -> (mirror_is_involutory mirror S_mirror V t). rewrite -> (mirror_is_involutory mirror S_mirror V t).
reflexivity. reflexivity.
- rewrite -> (S_Node V t1 t2). - rewrite <- M_t_t'.
Check (mirror_is_involutory mirror S_mirror V t1). rewrite -> (mirror_is_involutory mirror S_mirror V t).
(* TODO: Figure this out *) reflexivity.
Abort. Restart.
Proposition mirror_reverses_itself :
forall mirror : forall V : Type, binary_tree V -> binary_tree V,
specification_of_mirror mirror ->
forall (V : Type)
(t t' : binary_tree V),
mirror V t = t' ->
mirror V t' = t.
Proof.
intros mirror S_mirror V t t' M_t_t'. intros mirror S_mirror V t t' M_t_t'.
assert (f_equal : assert (f_equal :