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/ConstpropOpproof.v | 196 ++++++++++++++++++++++++------------------------- 1 file changed, 98 insertions(+), 98 deletions(-) (limited to 'kvx/ConstpropOpproof.v') diff --git a/kvx/ConstpropOpproof.v b/kvx/ConstpropOpproof.v index 05bbdde1..ffd35bcc 100644 --- a/kvx/ConstpropOpproof.v +++ b/kvx/ConstpropOpproof.v @@ -105,7 +105,7 @@ Proof. + (* global *) inv H2. exists (Genv.symbol_address ge id ofs); auto. + (* stack *) - inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. + inv H2. exists (Vptr sp ofs); split; auto. cbn. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma cond_strength_reduction_correct: @@ -115,7 +115,7 @@ Lemma cond_strength_reduction_correct: eval_condition cond' e##args' m = eval_condition cond e##args m. Proof. intros until vl. unfold cond_strength_reduction. - case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVM. + case (cond_strength_reduction_match cond args vl); cbn; intros; InvApproxRegs; SimplVM. - apply Val.swap_cmp_bool. - auto. - apply Val.swap_cmpu_bool. @@ -137,7 +137,7 @@ Proof. intros. unfold make_cmp_base. generalize (cond_strength_reduction_correct c args vl H). destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ. - econstructor; split. simpl; eauto. rewrite EQ. auto. + econstructor; split. cbn; eauto. rewrite EQ. auto. Qed. Lemma make_cmp_correct: @@ -154,43 +154,43 @@ Proof. unfold make_cmp. case (make_cmp_match c args vl); intros. - unfold make_cmp_imm_eq. destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. -+ simpl in H; inv H. InvBooleans. subst n. - exists (e#r1); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. ++ cbn in H; inv H. InvBooleans. subst n. + exists (e#r1); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. -* simpl in H; inv H. InvBooleans. subst n. - exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. +* cbn in H; inv H. InvBooleans. subst n. + exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. * apply make_cmp_base_correct; auto. - unfold make_cmp_imm_ne. destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. -+ simpl in H; inv H. InvBooleans. subst n. - exists (e#r1); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. ++ cbn in H; inv H. InvBooleans. subst n. + exists (e#r1); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. -* simpl in H; inv H. InvBooleans. subst n. - exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. +* cbn in H; inv H. InvBooleans. subst n. + exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. * apply make_cmp_base_correct; auto. - unfold make_cmp_imm_eq. destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. -+ simpl in H; inv H. InvBooleans. subst n. - exists (e#r1); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. ++ cbn in H; inv H. InvBooleans. subst n. + exists (e#r1); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. -* simpl in H; inv H. InvBooleans. subst n. - exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. +* cbn in H; inv H. InvBooleans. subst n. + exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. * apply make_cmp_base_correct; auto. - unfold make_cmp_imm_ne. destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. -+ simpl in H; inv H. InvBooleans. subst n. - exists (e#r1); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. ++ cbn in H; inv H. InvBooleans. subst n. + exists (e#r1); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. -* simpl in H; inv H. InvBooleans. subst n. - exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. +* cbn in H; inv H. InvBooleans. subst n. + exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. * apply make_cmp_base_correct; auto. - apply make_cmp_base_correct; auto. Qed. @@ -203,7 +203,7 @@ Proof. intros. unfold make_addimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (e#r); split; auto. - destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. + destruct (e#r); cbn; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. exists (Val.add e#r (Vint n)); split; auto. Qed. @@ -215,10 +215,10 @@ Lemma make_shlimm_correct: Proof. intros; unfold make_shlimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shl_zero. auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.shl_zero. auto. destruct (Int.ltu n Int.iwordsize). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_shrimm_correct: @@ -229,10 +229,10 @@ Lemma make_shrimm_correct: Proof. intros; unfold make_shrimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shr_zero. auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.shr_zero. auto. destruct (Int.ltu n Int.iwordsize). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_shruimm_correct: @@ -243,10 +243,10 @@ Lemma make_shruimm_correct: Proof. intros; unfold make_shruimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shru_zero. auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.shru_zero. auto. destruct (Int.ltu n Int.iwordsize). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_mulimm_correct: @@ -257,12 +257,12 @@ Lemma make_mulimm_correct: Proof. intros; unfold make_mulimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (Vint Int.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_zero; auto. + exists (Vint Int.zero); split; auto. destruct (e#r1); cbn; auto. rewrite Int.mul_zero; auto. predSpec Int.eq Int.eq_spec n Int.one; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_one; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.mul_one; auto. destruct (Int.is_power2 n) eqn:?; intros. - rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. simpl; eauto. auto. - econstructor; split; eauto. simpl. rewrite H; auto. + rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. cbn; eauto. auto. + econstructor; split; eauto. cbn. rewrite H; auto. Qed. Lemma make_divimm_correct: @@ -275,11 +275,11 @@ Proof. intros; unfold make_divimm. predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. destruct (e#r1) eqn:?; - try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + try (rewrite Val.divs_one in H; exists (Vint i); split; cbn; try rewrite Heqv0; auto); inv H; auto. destruct (Int.is_power2 n) eqn:?. destruct (Int.ltu i (Int.repr 31)) eqn:?. - exists v; split; auto. simpl. + exists v; split; auto. cbn. erewrite Val.divs_pow2; eauto. reflexivity. congruence. exists v; auto. exists v; auto. @@ -295,10 +295,10 @@ Proof. intros; unfold make_divuimm. predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. destruct (e#r1) eqn:?; - try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + try (rewrite Val.divu_one in H; exists (Vint i); split; cbn; try rewrite Heqv0; auto); inv H; auto. destruct (Int.is_power2 n) eqn:?. - econstructor; split. simpl; eauto. + econstructor; split. cbn; eauto. rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto. exists v; auto. Qed. @@ -312,7 +312,7 @@ Lemma make_moduimm_correct: Proof. intros; unfold make_moduimm. destruct (Int.is_power2 n) eqn:?. - exists v; split; auto. simpl. decEq. eapply Val.modu_pow2; eauto. congruence. + exists v; split; auto. cbn. decEq. eapply Val.modu_pow2; eauto. congruence. exists v; auto. Qed. @@ -324,18 +324,18 @@ Lemma make_andimm_correct: Proof. intros; unfold make_andimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. - subst n. exists (Vint Int.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_zero; auto. + subst n. exists (Vint Int.zero); split; auto. destruct (e#r); cbn; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_mone; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int.and_mone; auto. destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero | _ => false end) eqn:UNS. destruct x; try congruence. exists (e#r); split; auto. - inv H; auto. simpl. replace (Int.and i n) with i; auto. + inv H; auto. cbn. replace (Int.and i n) with i; auto. generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ. Int.bit_solve. destruct (zlt i0 n0). replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)). - rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. + rewrite Int.bits_zero. cbn. rewrite andb_true_r. auto. rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. rewrite H6 by auto. auto. @@ -349,9 +349,9 @@ Lemma make_orimm_correct: Proof. intros; unfold make_orimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_zero; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int.or_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. - subst n. exists (Vint Int.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_mone; auto. + subst n. exists (Vint Int.mone); split; auto. destruct (e#r); cbn; auto. rewrite Int.or_mone; auto. econstructor; split; eauto. auto. Qed. @@ -362,7 +362,7 @@ Lemma make_xorimm_correct: Proof. intros; unfold make_xorimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.xor_zero; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int.xor_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. subst n. exists (Val.notint e#r); split; auto. econstructor; split; eauto. auto. @@ -376,7 +376,7 @@ Proof. intros. unfold make_addlimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst. exists (e#r); split; auto. - destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto. + destruct (e#r); cbn; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto. exists (Val.addl e#r (Vlong n)); split; auto. Qed. @@ -388,11 +388,11 @@ Lemma make_shllimm_correct: Proof. intros; unfold make_shllimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. unfold Int64.shl'. rewrite Z.shiftl_0_r, Int64.repr_unsigned. auto. destruct (Int.ltu n Int64.iwordsize'). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_shrlimm_correct: @@ -403,11 +403,11 @@ Lemma make_shrlimm_correct: Proof. intros; unfold make_shrlimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. unfold Int64.shr'. rewrite Z.shiftr_0_r, Int64.repr_signed. auto. destruct (Int.ltu n Int64.iwordsize'). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_shrluimm_correct: @@ -418,11 +418,11 @@ Lemma make_shrluimm_correct: Proof. intros; unfold make_shrluimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. unfold Int64.shru'. rewrite Z.shiftr_0_r, Int64.repr_unsigned. auto. destruct (Int.ltu n Int64.iwordsize'). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_mullimm_correct: @@ -433,15 +433,15 @@ Lemma make_mullimm_correct: Proof. intros; unfold make_mullimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst. - exists (Vlong Int64.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_zero; auto. + exists (Vlong Int64.zero); split; auto. destruct (e#r1); cbn; auto. rewrite Int64.mul_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.one; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_one; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int64.mul_one; auto. destruct (Int64.is_power2' n) eqn:?; intros. exists (Val.shll e#r1 (Vint i)); split; auto. - destruct (e#r1); simpl; auto. + destruct (e#r1); cbn; auto. erewrite Int64.is_power2'_range by eauto. erewrite Int64.mul_pow2' by eauto. auto. - econstructor; split; eauto. simpl; rewrite H; auto. + econstructor; split; eauto. cbn; rewrite H; auto. Qed. Lemma make_divlimm_correct: @@ -453,7 +453,7 @@ Lemma make_divlimm_correct: Proof. intros; unfold make_divlimm. destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?. - rewrite H0 in H. econstructor; split. simpl; eauto. + rewrite H0 in H. econstructor; split. cbn; eauto. erewrite Val.divls_pow2; eauto. auto. exists v; auto. exists v; auto. @@ -468,9 +468,9 @@ Lemma make_divluimm_correct: Proof. intros; unfold make_divluimm. destruct (Int64.is_power2' n) eqn:?. - econstructor; split. simpl; eauto. + econstructor; split. cbn; eauto. rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. - simpl. + cbn. erewrite Int64.is_power2'_range by eauto. erewrite Int64.divu_pow2' by eauto. auto. exists v; auto. @@ -485,9 +485,9 @@ Lemma make_modluimm_correct: Proof. intros; unfold make_modluimm. destruct (Int64.is_power2 n) eqn:?. - exists v; split; auto. simpl. decEq. + exists v; split; auto. cbn. decEq. rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. - simpl. erewrite Int64.modu_and by eauto. auto. + cbn. erewrite Int64.modu_and by eauto. auto. exists v; auto. Qed. @@ -498,9 +498,9 @@ Lemma make_andlimm_correct: Proof. intros; unfold make_andlimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. - subst n. exists (Vlong Int64.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_zero; auto. + subst n. exists (Vlong Int64.zero); split; auto. destruct (e#r); cbn; auto. rewrite Int64.and_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.mone; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_mone; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int64.and_mone; auto. econstructor; split; eauto. auto. Qed. @@ -511,9 +511,9 @@ Lemma make_orlimm_correct: Proof. intros; unfold make_orlimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_zero; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int64.or_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.mone; intros. - subst n. exists (Vlong Int64.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_mone; auto. + subst n. exists (Vlong Int64.mone); split; auto. destruct (e#r); cbn; auto. rewrite Int64.or_mone; auto. econstructor; split; eauto. auto. Qed. @@ -524,7 +524,7 @@ Lemma make_xorlimm_correct: Proof. intros; unfold make_xorlimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.xor_zero; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int64.xor_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.mone; intros. subst n. exists (Val.notl e#r); split; auto. econstructor; split; eauto. auto. @@ -538,9 +538,9 @@ Lemma make_mulfimm_correct: Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. - simpl. econstructor; split. eauto. rewrite H; subst n. - destruct (e#r1); simpl; auto. rewrite Float.mul2_add; auto. - simpl. econstructor; split; eauto. + cbn. econstructor; split. eauto. rewrite H; subst n. + destruct (e#r1); cbn; auto. rewrite Float.mul2_add; auto. + cbn. econstructor; split; eauto. Qed. Lemma make_mulfimm_correct_2: @@ -551,10 +551,10 @@ Lemma make_mulfimm_correct_2: Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. - simpl. econstructor; split. eauto. rewrite H; subst n. - destruct (e#r2); simpl; auto. rewrite Float.mul2_add; auto. + cbn. econstructor; split. eauto. rewrite H; subst n. + destruct (e#r2); cbn; auto. rewrite Float.mul2_add; auto. rewrite Float.mul_commut; auto. - simpl. econstructor; split; eauto. + cbn. econstructor; split; eauto. Qed. Lemma make_mulfsimm_correct: @@ -565,9 +565,9 @@ Lemma make_mulfsimm_correct: Proof. intros; unfold make_mulfsimm. destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. - simpl. econstructor; split. eauto. rewrite H; subst n. - destruct (e#r1); simpl; auto. rewrite Float32.mul2_add; auto. - simpl. econstructor; split; eauto. + cbn. econstructor; split. eauto. rewrite H; subst n. + destruct (e#r1); cbn; auto. rewrite Float32.mul2_add; auto. + cbn. econstructor; split; eauto. Qed. Lemma make_mulfsimm_correct_2: @@ -578,10 +578,10 @@ Lemma make_mulfsimm_correct_2: Proof. intros; unfold make_mulfsimm. destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. - simpl. econstructor; split. eauto. rewrite H; subst n. - destruct (e#r2); simpl; auto. rewrite Float32.mul2_add; auto. + cbn. econstructor; split. eauto. rewrite H; subst n. + destruct (e#r2); cbn; auto. rewrite Float32.mul2_add; auto. rewrite Float32.mul_commut; auto. - simpl. econstructor; split; eauto. + cbn. econstructor; split; eauto. Qed. Lemma make_cast8signed_correct: @@ -594,8 +594,8 @@ Proof. exists e#r; split; auto. assert (V: vmatch bc e#r (Sgn Ptop 8)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. - econstructor; split; simpl; eauto. + inv V; cbn; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. + econstructor; split; cbn; eauto. Qed. Lemma make_cast16signed_correct: @@ -608,8 +608,8 @@ Proof. exists e#r; split; auto. assert (V: vmatch bc e#r (Sgn Ptop 16)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. - econstructor; split; simpl; eauto. + inv V; cbn; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. + econstructor; split; cbn; eauto. Qed. Lemma op_strength_reduction_correct: @@ -620,7 +620,7 @@ Lemma op_strength_reduction_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some w /\ Val.lessdef v w. Proof. intros until v; unfold op_strength_reduction; - case (op_strength_reduction_match op args vl); simpl; intros. + case (op_strength_reduction_match op args vl); cbn; intros. - (* cast8signed *) InvApproxRegs; SimplVM; inv H0. apply make_cast8signed_correct; auto. - (* cast16signed *) @@ -733,15 +733,15 @@ Lemma addr_strength_reduction_correct: exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'. Proof. intros until res. unfold addr_strength_reduction. - destruct (addr_strength_reduction_match addr args vl); simpl; + destruct (addr_strength_reduction_match addr args vl); cbn; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). - destruct (orb _ _). + exists (Val.offset_ptr e#r1 n); auto. -+ simpl. rewrite Genv.shift_symbol_address. econstructor; split; eauto. - inv H0; simpl; auto. ++ cbn. rewrite Genv.shift_symbol_address. econstructor; split; eauto. + inv H0; cbn; auto. - rewrite Ptrofs.add_zero_l. econstructor; split; eauto. change (Vptr sp (Ptrofs.add n1 n)) with (Val.offset_ptr (Vptr sp n1) n). - inv H0; simpl; auto. + inv H0; cbn; auto. - exists res; auto. Qed. -- cgit