From 728888d8a3f70afd526f6c4454327f52ea4c4746 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 17:47:55 +0100 Subject: Val_cmp* -> Val.mxcmp* --- scheduling/postpass_lib/Machblockgenproof.v | 27 ++++++--------------------- 1 file changed, 6 insertions(+), 21 deletions(-) (limited to 'scheduling/postpass_lib') diff --git a/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v index fc722887..d121a54b 100644 --- a/scheduling/postpass_lib/Machblockgenproof.v +++ b/scheduling/postpass_lib/Machblockgenproof.v @@ -190,7 +190,7 @@ Proof. intros H H0 H1. unfold find_label. remember (is_label l _) as b. - cutrewrite (b = false); auto. + replace b with false; auto. subst; unfold is_label. destruct i; cbn in * |- *; try (destruct (in_dec l nil); intuition). inversion H. @@ -286,7 +286,7 @@ Lemma find_label_preserved: Mach.find_label l (Mach.fn_code f) = Some c -> exists h, In l h /\ find_label l (fn_code (transf_function f)) = Some (concat h (trans_code c)). Proof. - intros. cutrewrite ((fn_code (transf_function f)) = trans_code (Mach.fn_code f)); eauto. + intros. replace (fn_code (transf_function f)) with (trans_code (Mach.fn_code f)); eauto. apply find_label_transcode_preserved; auto. Qed. @@ -661,7 +661,7 @@ Proof. inversion H1; subst; clear H1. inversion_clear H0; cbn. - (* function_internal*) - cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto. + replace (trans_code (Mach.fn_code f0)) with (fn_code (transf_function f0)); eauto. eapply exec_function_internal; eauto. rewrite <- parent_sp_preserved; eauto. rewrite <- parent_ra_preserved; eauto. @@ -733,12 +733,12 @@ Proof. intro H; destruct c as [|i' c]. { inversion H. } remember (trans_inst i) as ti. destruct ti as [lbl|bi|cfi]. - - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ). + - (*i=lbl *) replace (i ) with (Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ). exists nil; cbn; eexists. eapply Tr_add_label; eauto. - (*i=basic*) destruct i'. 10: { exists (add_to_new_bblock (MB_basic bi)::nil). exists b. - cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto. + replace ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_basic bi) :: (b::l)));eauto. rewrite Heqti. eapply Tr_end_block; eauto. rewrite <-Heqti. @@ -748,7 +748,7 @@ Proof. - (*i=cfi*) destruct i; try(cbn in Heqti; congruence). all: exists (add_to_new_bblock (MB_cfi cfi)::nil); exists b; - cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto; + replace ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto; rewrite Heqti; eapply Tr_end_block; eauto; rewrite <-Heqti; @@ -765,21 +765,6 @@ Proof. eauto. Qed. -(* FIXME: these two lemma should go into [Coqlib.v] *) -Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). -Proof. - induction l1; cbn; auto with coqlib. -Qed. -Hint Resolve is_tail_app: coqlib. - -Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. -Proof. - induction l1; cbn; auto with coqlib. - intros l2 l3 H; inversion H; eauto with coqlib. -Qed. -Hint Resolve is_tail_app_inv: coqlib. - - Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> exists b, is_tail (b :: trans_code c) (trans_code c2). Proof. -- cgit