From eacdec2dd13611f94fe12a41cf04cf38dc389092 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Fri, 12 Jun 2020 18:13:52 +0100 Subject: Fix broken proof. --- src/translation/HTLgenspec.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 57d2d87..57d7d62 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -433,8 +433,8 @@ Proof. Qed. Hint Resolve iter_expand_instr_spec : htlspec. -Lemma create_arr_inv : forall x y z a b c d, - create_arr x y z = OK (a, b) c d -> y = b. +Lemma create_arr_inv : forall w x y z a b c d, + create_arr w x y z = OK (a, b) c d -> y = b. Proof. inversion 1. reflexivity. Qed. @@ -454,14 +454,14 @@ Proof. monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) - pose proof (create_arr_inv _ _ _ _ _ _ _ EQ0) as STK_LEN. + pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. rewrite <- STK_LEN. econstructor; simpl; trivial. intros. inv_incr. assert (EQ3D := EQ3). - destruct x3. + destruct x4. apply collect_declare_datapath_trans in EQ3. apply collect_declare_controllogic_trans in EQ3D. assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. -- cgit