diff options
| -rw-r--r-- | aarch64/Asmgenproof.v | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 9598043c..16977d67 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -744,7 +744,6 @@ Proof. apply bind_inversion in UNFOLD_BBLOCK. destruct UNFOLD_BBLOCK as (? & UNFOLD_BODY & H). inversion H as (UNFOLD_BBLOCK). - remember (list_nth_z (header bb) n) as label_opt eqn:LBL. destruct label_opt. * (* nth instruction is a label *) eexists; split. { eapply is_nth_label; eauto. } @@ -762,17 +761,18 @@ Proof. ++ eapply is_nth_basic; eauto. ++ repeat (rewrite <- app_assoc). eapply list_nth_z_find_bi_with_header; eauto. -- (* nth instruction is the exit instruction *) - rewrite <- app_assoc. rewrite find_instr_past_header; auto. - rewrite <- app_assoc. erewrite find_instr_past_body; eauto. + generalize n_beyond_body. intros TEMP. + assert (n >= Z.of_nat (Datatypes.length (header bb) + + Datatypes.length (body bb))) as NGE. { auto. } clear TEMP. remember (exit bb) as exit_opt eqn:EXIT. destruct exit_opt. - ++ generalize n_beyond_body. intros. - assert (n >= Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb))). { auto. } + ++ rewrite <- app_assoc. rewrite find_instr_past_header; auto. + rewrite <- app_assoc. erewrite find_instr_past_body; eauto. assert (SIZE' := SIZE). unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE. destruct SIZE as (LOWER & UPPER). repeat (rewrite Nat2Z.inj_add in UPPER). - repeat (rewrite <- length_agree in UPPER). repeat (rewrite Nat2Z.inj_add in H2). - repeat (rewrite <- length_agree in H2). simpl in UPPER. + repeat (rewrite <- length_agree in UPPER). repeat (rewrite Nat2Z.inj_add in NGE). + repeat (rewrite <- length_agree in NGE). simpl in UPPER. assert (n = list_length_z (header bb) + list_length_z (body bb)). { omega. } assert (n = size bb - 1). { unfold size. rewrite <- EXIT. simpl. @@ -781,11 +781,10 @@ Proof. symmetry in EXIT. eexists; split. ** eapply is_nth_ctlflow; eauto. - ** simpl. destruct (zeq (n - list_length_z (header bb) - list_length_z (body bb)) 0). 2: { (*absurd *) omega. } - reflexivity. + ** simpl. + destruct (zeq (n - list_length_z (header bb) - list_length_z (body bb)) 0). { reflexivity. } + (* absurd *) omega. ++ (* absurd *) - generalize n_beyond_body. intros. - assert (n >= Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb))). { auto. } unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE. destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. omega. + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB. |