diff options
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgenproof.v | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 13aecf4d..d69d8886 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -501,8 +501,31 @@ Proof. generalize (list_length_z_aux_increase _ tl 1); omega. Qed. + +Lemma list_length_add_acc A (l : list A) acc: + list_length_z_aux l acc = (list_length_z l) + acc. +Proof. + unfold list_length_z, list_length_z_aux. simpl. + fold list_length_z_aux. + rewrite (list_length_z_aux_shift l acc 0). + omega. +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. +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)). -Admitted. +Proof. + unfold size. + repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). reflexivity. +Qed. Lemma bblock_size_pos bb: size bb >= 1. Proof. |