diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-03 13:53:32 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-03 13:53:32 +0200 |
| commit | 52836c3aa914f864d464031a2f0948afb07e84e3 (patch) | |
| tree | 67b62dc09102b4b34d0aa941a83911a87c5f018f | |
| parent | 6d21e5e9ffc5b3876db3cad987e026206693e416 (diff) | |
| download | compcert-kvx-52836c3aa914f864d464031a2f0948afb07e84e3.tar.gz compcert-kvx-52836c3aa914f864d464031a2f0948afb07e84e3.zip | |
introduce a small tactic.
| -rw-r--r-- | mppa_k1c/Machblockgenproof.v | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index 7f877aa3..eb330e99 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -199,6 +199,10 @@ Definition concat (h: list label) (c: code): code := | b::c' => {| header := h ++ (header b); body := body b; exit := exit b |}::c' end. +Ltac subst_is_trans_code H := + rewrite is_trans_code_inv in H; + rewrite <- H in * |- *. + Lemma find_label_transcode_preserved: forall l c c', Mach.find_label l c = Some c' -> @@ -233,8 +237,7 @@ Proof. inversion H0 as [H1]. clear H0. erewrite find_label_at_begin; simpl; eauto. - apply is_trans_code_inv in Heqbl. - rewrite <- Heqbl. + subst_is_trans_code Heqbl. exists (l :: nil); simpl; eauto. - subst; assert (H: l0 <> l); try congruence; clear H0. exploit IHHeqbl; eauto. @@ -254,7 +257,7 @@ Proof. intros. exploit Mach_find_label_split; eauto. destruct 1 as [(H2&H3)|(H2&H3)]. - rewrite H2 in H. unfold trans_inst in H. congruence. + rewrite H2 in H. unfold trans_inst in H. congruence. exploit IHHeqbl; eauto. clear IHHeqbl Heqbl. intros (h & H4 & H5). @@ -318,7 +321,7 @@ Proof. inversion Heqbl as [|bl0 H| |]; subst; clear Heqbl. - rewrite size_add_to_newblock; omega. - rewrite size_add_label; - rewrite is_trans_code_inv in H; rewrite <- H. + subst_is_trans_code H. omega. Admitted. (* A FINIR *) |