diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-23 08:00:52 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-23 08:00:52 +0100 |
| commit | 313db9c2b0b69fbbb2005ed90fd221932f87e5a0 (patch) | |
| tree | 4600e86476d202b5f3c6c5a6c5adb9b42cd71007 | |
| parent | 62505aeb0303126cac8f1e3f8fb06414c9cd4fb0 (diff) | |
| download | compcert-kvx-313db9c2b0b69fbbb2005ed90fd221932f87e5a0.tar.gz compcert-kvx-313db9c2b0b69fbbb2005ed90fd221932f87e5a0.zip | |
slight simplification
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index f5a84db7..634f50bb 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -733,12 +733,11 @@ Proof. eapply verified_schedule_checks_alls_bundles; eauto. Qed. -Lemma find_bblock_forall_inv lb P: - (forall b, List.In b lb -> P b) -> - forall ofs b, find_bblock ofs lb = Some b -> P b. +Lemma find_bblock_Some_in lb: + forall ofs b, find_bblock ofs lb = Some b -> List.In b lb. Proof. induction lb; simpl; try congruence. - intros H ofs b. + intros ofs b. destruct (zlt ofs 0); try congruence. destruct (zeq ofs 0); eauto. intros X; inversion X; eauto. @@ -771,8 +770,8 @@ Proof. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks _))); simpl in *|-; try congruence. injection EQ1; intros; subst. monadInv EQ0. simpl in * |-. - intros; pattern bundle; eapply find_bblock_forall_inv; eauto. intros; exploit transf_blocks_checks_all_bundles; eauto. + intros; eapply find_bblock_Some_in; eauto. Qed. Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m' o: |