diff options
Diffstat (limited to 'kvx/lib/Machblockgen.v')
| -rw-r--r-- | kvx/lib/Machblockgen.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kvx/lib/Machblockgen.v b/kvx/lib/Machblockgen.v index ab186083..3d5d7b2c 100644 --- a/kvx/lib/Machblockgen.v +++ b/kvx/lib/Machblockgen.v @@ -148,11 +148,11 @@ Lemma add_to_code_is_trans_code i c bl: is_trans_code c bl -> is_trans_code (i::c) (add_to_code (trans_inst i) bl). Proof. - destruct bl as [|bh0 bl]; simpl. + destruct bl as [|bh0 bl]; cbn. - intro H. inversion H. subst. eauto. - remember (trans_inst i) as ti. destruct ti as [l|bi|cfi]. - + intros; eapply Tr_add_label; eauto. destruct i; simpl in * |- *; congruence. + + intros; eapply Tr_add_label; eauto. destruct i; cbn in * |- *; congruence. + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b]. * eapply Tr_add_basic; eauto. * cutrewrite (add_basic bi empty_bblock = add_to_new_bblock (MB_basic bi)); auto. @@ -170,7 +170,7 @@ Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, is_trans_code c2 mbi -> is_trans_code (rev_append c1 c2) (trans_code_rev c1 mbi). Proof. - induction c1 as [| i c1]; simpl; auto. + induction c1 as [| i c1]; cbn; auto. Qed. Lemma trans_code_is_trans_code c: is_trans_code c (trans_code c). @@ -186,17 +186,17 @@ Lemma add_to_code_is_trans_code_inv i c bl: is_trans_code (i::c) bl -> exists bl0, is_trans_code c bl0 /\ bl = add_to_code (trans_inst i) bl0. Proof. intro H; inversion H as [|H0 H1 bl0| | H0 bi bh H1 bl0]; clear H; subst; (repeat econstructor); eauto. - + (* case Tr_end_block *) inversion H3; subst; simpl; auto. + + (* case Tr_end_block *) inversion H3; subst; cbn; auto. * destruct (header bh); congruence. - * destruct bl0; simpl; congruence. - + (* case Tr_add_basic *) rewrite H3. simpl. destruct (header bh); congruence. + * destruct bl0; cbn; congruence. + + (* case Tr_add_basic *) rewrite H3. cbn. 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 -> exists mbi0, is_trans_code c2 mbi0 /\ mbi=trans_code_rev c1 mbi0. Proof. - induction c1 as [| i c1]; simpl; eauto. + induction c1 as [| i c1]; cbn; eauto. intros; exploit IHc1; eauto. intros (mbi0 & H1 & H2); subst. exploit add_to_code_is_trans_code_inv; eauto. |