diff options
| author | tvdd <tvdd@debian.lan> | 2019-03-07 17:32:24 +0100 |
|---|---|---|
| committer | tvdd <tvdd@debian.lan> | 2019-03-07 17:32:24 +0100 |
| commit | 4ec4ce3c17c0aceadc34d0d203b0f01f0fbabfa1 (patch) | |
| tree | 08776a5879dd52f87475dc6ac1ba601f589d187f | |
| parent | be56a34df35fcebdf723c204f83b1208c92e0b77 (diff) | |
| download | compcert-kvx-4ec4ce3c17c0aceadc34d0d203b0f01f0fbabfa1.tar.gz compcert-kvx-4ec4ce3c17c0aceadc34d0d203b0f01f0fbabfa1.zip | |
Machblockgen proofs
| -rw-r--r-- | mppa_k1c/Machblockgen.v | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index fb63c78c..4dfc309e 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -175,8 +175,8 @@ Proof. + (* case Tr_end_block *) inversion H3; subst; simpl; auto. * destruct (header bh); congruence. * destruct bl0; simpl; congruence. - + (* case Tr_add_basic *) -Admitted. (* A FINIR *) + + (* case Tr_add_basic *) rewrite H3. simpl. destruct (header bh); congruence. +Qed. Lemma trans_code_is_trans_code_rev_inv c1: forall c2 mbi, is_trans_code (rev_append c1 c2) mbi -> @@ -186,11 +186,22 @@ Proof. intros; exploit IHc1; eauto. intros (mbi0 & H1 & H2); subst. exploit add_to_code_is_trans_code_inv; eauto. -Admitted. (* A FINIR *) + intros. destruct H0 as [mbi1 [H2 H3]]. + exists mbi1. split; congruence. +Qed. Local Hint Resolve trans_code_is_trans_code. Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c). Proof. constructor; intros; subst; auto. -Admitted. (* A FINIR *) + unfold trans_code. + exploit (trans_code_is_trans_code_rev_inv (rev_append c nil) nil bl); eauto. + * rewrite <- rev_alt. + rewrite <- rev_alt. + rewrite (rev_involutive c). + apply H. + * intros. + destruct H0 as [mbi [H0 H1]]. + inversion H0. subst. reflexivity. +Qed. |