diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 08:15:33 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 08:15:33 +0200 |
| commit | 68edea74c5ac8b4767f5a19d1aadc072959e1107 (patch) | |
| tree | 15709f672fabe9628382b1d62b6e50a4abdea1f0 /aarch64/Asmgenproof.v | |
| parent | 6eaf6247368b8284665e3a826701a0d4882eaaf4 (diff) | |
| download | compcert-kvx-68edea74c5ac8b4767f5a19d1aadc072959e1107.tar.gz compcert-kvx-68edea74c5ac8b4767f5a19d1aadc072959e1107.zip | |
Factorize common proof-pattern as lemmas
unfolding a non-empty list of basic blocks will unfold the head
(unfold_bblock) and then recur on the tail.
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 38 |
1 files changed, 30 insertions, 8 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 0f33b80f..2c693b25 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -535,6 +535,34 @@ Proof. omega. Qed. +Lemma unfold_car_cdr bb bbs tc: + unfold (bb :: bbs) = OK tc -> + exists tbb tc', unfold_bblock bb = OK tbb /\ unfold bbs = OK tc'. +Proof. + intros UNFOLD. + unfold unfold in UNFOLD. + apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UBB). destruct UBB as (UBB & REST). + apply bind_inversion in REST. destruct REST as (? & UNFOLD'). + fold unfold in UNFOLD'. destruct UNFOLD'. + eexists; eauto. +Qed. + +Lemma unfold_cdr bb bbs tc: + unfold (bb :: bbs) = OK tc -> + exists tc', unfold bbs = OK tc'. +Proof. + intros; exploit unfold_car_cdr; eauto. intros (_ & ? & _ & ?). + eexists; eauto. +Qed. + +Lemma unfold_car bb bbs tc: + unfold (bb :: bbs) = OK tc -> + exists tbb, unfold_bblock bb = OK tbb. +Proof. + intros; exploit unfold_car_cdr; eauto. intros (? & _ & ? & _). + eexists; eauto. +Qed. + Lemma all_blocks_translated: forall bbs tc, unfold bbs = OK tc -> @@ -546,10 +574,7 @@ Proof. - intros ? UNFOLD ? IN. (* unfold proceeds by unfolding the basic block at the head of the list and * then recurring *) - unfold unfold in UNFOLD. - apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UBB). destruct UBB as (UBB & REST). - apply bind_inversion in REST. destruct REST as (? & UNFOLD'). - fold unfold in UNFOLD'. destruct UNFOLD'. + exploit unfold_car_cdr; eauto. intros (? & ? & ? & ?). (* basic block is either in head or tail *) inversion IN as [EQ | NEQ]. + rewrite <- EQ; eexists; eauto. @@ -567,10 +592,7 @@ Proof. - destruct pos. + intros. inversion FINDBB as (EQ). rewrite <- EQ. apply in_eq. + intros. - unfold unfold in UNFOLD. - apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UBB). destruct UBB as (UBB & REST). - apply bind_inversion in REST. destruct REST as (? & UNFOLD'). - fold unfold in UNFOLD'. destruct UNFOLD'. + exploit unfold_cdr; eauto. intros (tc' & UNFOLD'). unfold find_bblock in FINDBB. simpl in FINDBB. fold find_bblock in FINDBB. apply in_cons. eapply IH; eauto. |