From 7cdb61b3549698de8f2270aca8beffd3007c29ac Mon Sep 17 00:00:00 2001 From: Yadunand Prem Date: Thu, 15 Feb 2024 16:16:09 +0800 Subject: [PATCH] feat: fix week 3 --- ...3_structural-induction-over-binary-trees.v | 21 ++++--------------- 1 file changed, 4 insertions(+), 17 deletions(-) diff --git a/cs3234/labs/week-03_structural-induction-over-binary-trees.v b/cs3234/labs/week-03_structural-induction-over-binary-trees.v index cc5b715..4f13107 100644 --- a/cs3234/labs/week-03_structural-induction-over-binary-trees.v +++ b/cs3234/labs/week-03_structural-induction-over-binary-trees.v @@ -197,24 +197,11 @@ Proof. - rewrite <- M_t_t'. rewrite -> (mirror_is_involutory mirror S_mirror V t). reflexivity. - - rewrite -> (S_Node V t1 t2). - Check (mirror_is_involutory mirror S_mirror V t1). - (* TODO: Figure this out *) + - rewrite <- M_t_t'. + rewrite -> (mirror_is_involutory mirror S_mirror V t). + reflexivity. - Abort. - - - - - -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. + Restart. intros mirror S_mirror V t t' M_t_t'. assert (f_equal :