From b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 29 Sep 2020 16:22:18 +0200 Subject: simpl -> cbn --- kvx/NeedOp.v | 54 +++++++++++++++++++++++++++--------------------------- 1 file changed, 27 insertions(+), 27 deletions(-) (limited to 'kvx/NeedOp.v') diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v index 4c354d5a..f636336d 100644 --- a/kvx/NeedOp.v +++ b/kvx/NeedOp.v @@ -229,7 +229,7 @@ Lemma needs_of_condition0_sound: Proof. intros until arg2. intros Hcond Hagree. - apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); simpl; auto. + apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); cbn; auto. apply val_inject_lessdef. apply lessdef_vagree. assumption. Qed. @@ -239,7 +239,7 @@ Lemma addl_sound: vagree (Val.addl v1 v2) (Val.addl w1 w2) x. Proof. unfold default; intros. - destruct x; simpl in *; trivial. + destruct x; cbn in *; trivial. - unfold Val.addl. destruct v1; destruct v2; trivial; destruct Archi.ptr64; trivial. - apply Val.addl_lessdef; trivial. @@ -249,7 +249,7 @@ Lemma subl_lessdef: forall v1 v1' v2 v2', Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.subl v1 v2) (Val.subl v1' v2'). Proof. - intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto. + intros. inv H. inv H0. auto. destruct v1'; cbn; auto. cbn; auto. Qed. Lemma subl_sound: @@ -258,10 +258,10 @@ Lemma subl_sound: vagree (Val.subl v1 v2) (Val.subl w1 w2) x. Proof. unfold default; intros. - destruct x; simpl in *; trivial. + destruct x; cbn in *; trivial. - unfold Val.subl. - destruct v1; destruct v2; trivial; destruct Archi.ptr64; simpl; trivial. - destruct (eq_block _ _) ; simpl; trivial. + destruct v1; destruct v2; trivial; destruct Archi.ptr64; cbn; trivial. + destruct (eq_block _ _) ; cbn; trivial. - apply subl_lessdef; trivial. Qed. @@ -272,7 +272,7 @@ Lemma mull_sound: vagree (Val.mull v1 v2) (Val.mull w1 w2) x. Proof. unfold default; intros. - destruct x; simpl in *; trivial. + destruct x; cbn in *; trivial. - unfold Val.mull. destruct v1; destruct v2; trivial. - unfold Val.mull. @@ -284,7 +284,7 @@ Qed. Remark default_idem: forall nv, default (default nv) = default nv. Proof. - destruct nv; simpl; trivial. + destruct nv; cbn; trivial. Qed. Lemma vagree_triple_op_float : @@ -298,14 +298,14 @@ Proof. induction nv; intros Hax Hby Hcz. - trivial. - - simpl in *. destruct a; simpl; trivial. - destruct b; simpl; trivial. - destruct c; simpl; trivial. - - simpl in *. destruct a; simpl; trivial. - destruct b; simpl; trivial. - destruct c; simpl; trivial. + - cbn in *. destruct a; cbn; trivial. + destruct b; cbn; trivial. + destruct c; cbn; trivial. + - cbn in *. destruct a; cbn; trivial. + destruct b; cbn; trivial. + destruct c; cbn; trivial. inv Hax. inv Hby. inv Hcz. - simpl. + cbn. constructor. Qed. @@ -320,14 +320,14 @@ Proof. induction nv; intros Hax Hby Hcz. - trivial. - - simpl in *. destruct a; simpl; trivial. - destruct b; simpl; trivial. - destruct c; simpl; trivial. - - simpl in *. destruct a; simpl; trivial. - destruct b; simpl; trivial. - destruct c; simpl; trivial. + - cbn in *. destruct a; cbn; trivial. + destruct b; cbn; trivial. + destruct c; cbn; trivial. + - cbn in *. destruct a; cbn; trivial. + destruct b; cbn; trivial. + destruct c; cbn; trivial. inv Hax. inv Hby. inv Hcz. - simpl. + cbn. constructor. Qed. @@ -343,7 +343,7 @@ Lemma needs_of_operation_sound: /\ vagree v v' nv. Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); - simpl in *; FuncInv; InvAgree; TrivialExists. + cbn in *; FuncInv; InvAgree; TrivialExists. - apply sign_ext_sound; auto. compute; auto. - apply sign_ext_sound; auto. compute; auto. - apply add_sound; auto. @@ -384,17 +384,17 @@ Proof. - destruct (eval_condition0 _ _ _) as [b|] eqn:EC. erewrite needs_of_condition0_sound by eauto. apply select_sound; auto. - simpl; auto with na. + cbn; auto with na. (* select imm *) - destruct (eval_condition0 _ _ _) as [b|] eqn:EC. { erewrite needs_of_condition0_sound by eauto. apply select_sound; auto with na. } - simpl; auto with na. + cbn; auto with na. (* select long imm *) - destruct (eval_condition0 _ _ _) as [b|] eqn:EC. { erewrite needs_of_condition0_sound by eauto. apply select_sound; auto with na. } - simpl; auto with na. + cbn; auto with na. Qed. Lemma operation_is_redundant_sound: @@ -404,7 +404,7 @@ Lemma operation_is_redundant_sound: vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> vagree v arg1' nv. Proof. - intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. + intros. destruct op; cbn in *; try discriminate; inv H1; FuncInv; subst. - apply sign_ext_redundant_sound; auto. omega. - apply sign_ext_redundant_sound; auto. omega. - apply andimm_redundant_sound; auto. -- cgit