diff options
| author | tvdd <tvdd@debian.lan> | 2019-03-05 11:49:32 +0100 |
|---|---|---|
| committer | tvdd <tvdd@debian.lan> | 2019-03-05 11:49:32 +0100 |
| commit | be56a34df35fcebdf723c204f83b1208c92e0b77 (patch) | |
| tree | a960b379975c69306833f5a148f8d46d253043e2 | |
| parent | 0d709513e08aa36faae2fe3d006e7e4c23aa4aff (diff) | |
| download | compcert-kvx-be56a34df35fcebdf723c204f83b1208c92e0b77.tar.gz compcert-kvx-be56a34df35fcebdf723c204f83b1208c92e0b77.zip | |
add_to_code_is_trans_code proof 2
| -rw-r--r-- | mppa_k1c/Machblockgen.v | 20 |
1 files changed, 6 insertions, 14 deletions
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index 0a8b2ccd..fb63c78c 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -127,16 +127,6 @@ Inductive is_trans_code: Mach.code -> code -> Prop := trans_inst i = MB_basic bi -> header bh = nil -> is_trans_code (i::c) (add_basic bi bh::bl). -(* Use Tr_end_block instead of: - | Tr_empty_bblock c bh bl: - is_trans_code c bl -> - bh = empty_bblock -> - is_trans_code c (bh::bl) - | Tr_cfi i bi c bl: - is_trans_code c bl -> - trans_inst i = MB_cfi bi -> - is_trans_code (i::c) (cfi_bblock bi :: bl). -*) Local Hint Resolve Tr_nil Tr_end_block. @@ -153,10 +143,12 @@ Proof. * eapply Tr_add_basic; eauto. * cutrewrite (add_basic bi empty_bblock = add_to_new_bblock (MB_basic bi)); auto. rewrite Heqti; eapply Tr_end_block; eauto. - rewrite <- Heqti. - eapply End_basic. - (* + intros. eapply Tr_cfi. eauto. symmetry in Heqti. eauto. *) -Admitted. (* A FINIR *) + rewrite <- Heqti. eapply End_basic. congruence. + + intros. + cutrewrite (cfi_bblock cfi = add_to_new_bblock (MB_cfi cfi)); auto. + rewrite Heqti. eapply Tr_end_block; eauto. + rewrite <- Heqti. eapply End_cfi. congruence. +Qed. Local Hint Resolve add_to_code_is_trans_code. |