Complete bblock_size_aux

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.