Replace common pattern with simpler lemma.

Turns two rewrites and a simplification into a single rewrite via
list_length_z_cons.

1 files changed, 16 insertions, 29 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 2ee4d476..4ee7c550 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -307,14 +307,18 @@ Proof.
     omega.
 Qed.
 
+Lemma list_length_z_cons A hd (tl : list A):
+  list_length_z (hd :: tl) = list_length_z tl + 1.
+Proof.
+  unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity.
+Qed.
+
 Lemma length_agree A (l : list A):
   list_length_z l = Z.of_nat (length l).
 Proof.
   induction l as [| ? l IH]; intros.
   - unfold list_length_z; reflexivity.
-  - unfold list_length_z; simpl;
-    rewrite list_length_add_acc, Zpos_P_of_succ_nat;
-    omega.
+  - simpl; rewrite list_length_z_cons, Zpos_P_of_succ_nat; omega.
 Qed.
 
 Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)).
@@ -323,12 +327,6 @@ Proof.
   repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). reflexivity.
 Qed.
 
-Lemma list_length_z_cons A hd (tl : list A):
-  list_length_z (hd :: tl) = list_length_z tl + 1.
-Proof.
-  unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity.
-Qed.
-
 Lemma header_size_lt_block_size bb:
   list_length_z (header bb) < size bb.
 Proof.
@@ -1023,18 +1021,15 @@ Proof.
     rewrite ATPC in AGPC; symmetry in AGPC, ATPC_NEXT.
 
     inversion MATCHI as [? ? ? ? ? M_AGREE RS_AGREE ATPC' OFS RS RS']; subst.
-    symmetry in ATPC'. unfold list_length_z in ATPC'.
-    simpl in ATPC'. rewrite list_length_add_acc in ATPC'.
+    symmetry in ATPC'. rewrite list_length_z_cons in ATPC'.
     rewrite ATPC in ATPC'.
     unfold Val.offset_ptr in ATPC'.
     simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
-    unfold list_length_z in FIND_INSTR; simpl in FIND_INSTR.
-    rewrite list_length_add_acc in FIND_INSTR.
+    rewrite list_length_z_cons in FIND_INSTR.
 
     destruct BOUNDED as [(? & LT_MAX) LT_END_OF_BODY].
-    assert (list_length_z bis < end_of_body).
-    { unfold list_length_z in LT_END_OF_BODY; simpl in LT_END_OF_BODY;
-      rewrite list_length_add_acc in LT_END_OF_BODY; omega. }
+    assert (list_length_z bis < end_of_body)
+      by (rewrite list_length_z_cons in LT_END_OF_BODY; omega).
     generalize (Ptrofs.unsigned_range_2 ofs); intros.
     exploit (Asm.exec_step_internal tge b
              (Ptrofs.add ofs (Ptrofs.repr (end_of_body - (list_length_z bis + 1))))
@@ -1045,8 +1040,7 @@ Proof.
       rewrite Z.add_sub_assoc; assumption. }
     intros STEP_NEXT.
 
-    unfold list_length_z in MI_NEXT; simpl in MI_NEXT.
-    rewrite list_length_add_acc in MI_NEXT.
+    rewrite list_length_z_cons in MI_NEXT.
     (* XXX use better tactics *)
     replace (end_of_body - (list_length_z bis + 1) + 1)
        with (end_of_body - list_length_z bis) in MI_NEXT by omega.
@@ -1057,10 +1051,9 @@ Proof.
       intros n NLT.
       assert (NLT': (n + 1 < length (bi_next :: bis))%nat). { simpl; omega. }
       specialize (FINDBI (n + 1)%nat NLT').
-      unfold list_length_z in FINDBI. simpl in FINDBI. rewrite list_length_add_acc in FINDBI.
-      destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e. simpl in e. omega. }
-      unfold list_length_z in FINDBI. simpl in FINDBI. rewrite list_length_add_acc in FINDBI.
-      rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI. rewrite Z.add_0_r in FINDBI.
+      rewrite list_length_z_cons in FINDBI; simpl in FINDBI.
+      destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e; simpl in e; omega. }
+      rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI.
       replace (Ptrofs.unsigned ofs + end_of_body - (list_length_z bis + 1) + (Z.of_nat n + 1))
          with (Ptrofs.unsigned ofs + end_of_body - list_length_z bis + Z.of_nat n) in FINDBI by omega.
       replace (Z.pred (Z.of_nat n + 1)) with (Z.of_nat n) in FINDBI by omega.
@@ -1070,7 +1063,7 @@ Proof.
 
     eexists; split.
     + eapply star_step; eauto.
-    + info_auto.
+    + auto.
 Qed.
 
 Lemma find_basic_instructions b ofs f bb tc: forall
@@ -1140,15 +1133,9 @@ Proof.
   rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT.
 
   inv MATCHI. symmetry in AGPC0.
-  unfold list_length_z in AGPC0.
-  simpl in AGPC0. rewrite list_length_add_acc in AGPC0.
   rewrite ATPC in AGPC0.
   unfold Val.offset_ptr in AGPC0.
   simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
-  unfold list_length_z in FIND_INSTR; simpl in FIND_INSTR.
-  rewrite list_length_add_acc in FIND_INSTR.
-  rewrite Z.add_0_r in FIND_INSTR.
-  rewrite Z.add_0_r in AGPC0.
 
   assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
     by (eapply size_of_blocks_bounds; eauto).