Minor cleanup of find_instr_bblock

- Remove one auto-generated name
- Move assertion on n's size up
- Clear unnecessary hypothesis (iirc generalize worked better than
  exploit here)
- Rewrite progress of Asm.find_instr only in the case that needs it

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.