diff options
| author | tvdd <tvdd@debian.lan> | 2019-04-04 15:01:58 +0200 |
|---|---|---|
| committer | tvdd <tvdd@debian.lan> | 2019-04-04 15:01:58 +0200 |
| commit | b4ed42a385a4560c82d9ffa234fd00608f431583 (patch) | |
| tree | af74bbe58471f48a67638681313a162e6a78bd6b | |
| parent | 9d286aa671a9c320114337a821fab8677e03558e (diff) | |
| download | compcert-kvx-b4ed42a385a4560c82d9ffa234fd00608f431583.tar.gz compcert-kvx-b4ed42a385a4560c82d9ffa234fd00608f431583.zip | |
dist_end_block_code_simu_mid_block proof
| -rw-r--r-- | mppa_k1c/Machblockgenproof.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index 0ca23a36..267cbebb 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -307,11 +307,18 @@ Proof. unfold add_label, size; simpl; omega. Qed. +Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1. +Proof. + intro H. unfold add_basic, size; rewrite H; simpl. omega. +Qed. + + Lemma size_add_to_newblock i: size (add_to_new_bblock i) = 1. Proof. destruct i; auto. Qed. + Lemma dist_end_block_code_simu_mid_block i c: dist_end_block_code (i::c) <> 0 -> (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c)). @@ -324,7 +331,11 @@ Proof. - rewrite size_add_label; subst_is_trans_code H. omega. -Admitted. (* A FINIR *) + - rewrite size_add_basic; auto. + subst_is_trans_code H. + omega. +Qed. + Local Hint Resolve dist_end_block_code_simu_mid_block. |