From d00330eb7a3dbe308a6aa57646491f03eadea9a7 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Mon, 21 Sep 2020 15:53:07 +0200 Subject: Replace common pattern with simpler lemma. Turns two rewrites and a simplification into a single rewrite via list_length_z_cons. --- aarch64/Asmgenproof.v | 45 ++++++++++++++++----------------------------- 1 file 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). -- cgit