diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-24 15:40:36 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-24 15:47:06 +0200 |
| commit | 6eaf6247368b8284665e3a826701a0d4882eaaf4 (patch) | |
| tree | 4b4c06f2f101f32b9c7cf86411dd953d3bda919b /aarch64 | |
| parent | 0a47d9af1403686ef1c87615eb5aeb9b1aad5d25 (diff) | |
| download | compcert-kvx-6eaf6247368b8284665e3a826701a0d4882eaaf4.tar.gz compcert-kvx-6eaf6247368b8284665e3a826701a0d4882eaaf4.zip | |
Simplify premises
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgenproof.v | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index dde939ed..0f33b80f 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -556,13 +556,13 @@ Proof. + eapply IHbbs; eauto. Qed. -Lemma bblock_in_bblocks f bb: forall +Lemma bblock_in_bblocks bbs bb: forall tc pos - (UNFOLD: unfold (fn_blocks f) = OK tc) - (FINDBB: find_bblock pos (fn_blocks f) = Some bb), - In bb (fn_blocks f). + (UNFOLD: unfold bbs = OK tc) + (FINDBB: find_bblock pos bbs = Some bb), + In bb bbs. Proof. - induction (fn_blocks f) as [| b bbs IH]. + induction bbs as [| b bbs IH]. - intros. inversion FINDBB. - destruct pos. + intros. inversion FINDBB as (EQ). rewrite <- EQ. apply in_eq. @@ -577,15 +577,12 @@ Proof. + intros. inversion FINDBB. Qed. -Lemma blocks_translated b pos f bb: forall - (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) - (FINDBB: find_bblock pos (fn_blocks f) = Some bb), +Lemma blocks_translated tc pos bbs bb: forall + (UNFOLD: unfold bbs = OK tc) + (FINDBB: find_bblock pos bbs = Some bb), exists tbb, unfold_bblock bb = OK tbb. Proof. - intros. - exploit internal_functions_unfold; eauto. - intros (tc & FINDtf & TRANStf & ?). - exploit bblock_in_bblocks; eauto. intros BB. + intros; exploit bblock_in_bblocks; eauto; intros; eapply all_blocks_translated; eauto. Qed. |