From 43b078ba35aec32840f459d67de3fe6408184cea Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 25 May 2020 22:32:33 +0100 Subject: Finished proving the first case --- src/translation/HTLgenspec.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 8ea4384..f01ab1c 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -235,7 +235,7 @@ Proof. destruct (peq pc pc1). + subst. - destruct instr1. + destruct instr1 eqn:?. econstructor. unfold add_instr in EQ. destruct (check_empty_node_datapath s1 pc1); try discriminate. @@ -251,10 +251,15 @@ Proof. destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; [ discriminate | apply H7 ]. + inversion H1. inversion H7. rewrite H. apply tr_instr_Inop. + eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + + eapply IHl. apply EQ0. assumption. destruct H1. inversion H1. subst. contradiction. assumption. + + Qed. Theorem transl_module_correct : -- cgit