From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/SelectDivproof.v | 196 +++++++++++++++++++++++------------------------ 1 file changed, 98 insertions(+), 98 deletions(-) (limited to 'backend/SelectDivproof.v') diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index d4bd4f5c..ffe607e4 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -50,17 +50,17 @@ Lemma Zdiv_mul_pos: Zdiv n d = Zdiv (m * n) (two_p (N + l)). Proof. intros m l l_pos [LO HI] n RANGE. - exploit (Z_div_mod_eq n d). auto. + exploit (Z_div_mod_eq n d). auto. set (q := n / d). set (r := n mod d). intro EUCL. assert (0 <= r <= d - 1). unfold r. generalize (Z_mod_lt n d d_pos). omega. - assert (0 <= m). + assert (0 <= m). apply Zmult_le_0_reg_r with d. auto. - exploit (two_p_gt_ZERO (N + l)). omega. omega. + exploit (two_p_gt_ZERO (N + l)). omega. omega. set (k := m * d - two_p (N + l)). - assert (0 <= k <= two_p l). + assert (0 <= k <= two_p l). unfold k; omega. assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). unfold k. rewrite EUCL. ring. @@ -70,14 +70,14 @@ Proof. apply Zle_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. replace (N + l) with (l + N) by omega. - rewrite two_p_is_exp. + rewrite two_p_is_exp. replace (two_p l * two_p N - two_p l) with (two_p l * (two_p N - 1)) by ring. apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. omega. omega. assert (0 <= two_p (N + l) * r). - apply Zmult_le_0_compat. + apply Zmult_le_0_compat. exploit (two_p_gt_ZERO (N + l)). omega. omega. omega. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). @@ -87,23 +87,23 @@ Proof. omega. exploit (two_p_gt_ZERO (N + l)). omega. omega. assert (0 <= m * n - two_p (N + l) * q). - apply Zmult_le_reg_r with d. auto. - replace (0 * d) with 0 by ring. rewrite H2. omega. + apply Zmult_le_reg_r with d. auto. + replace (0 * d) with 0 by ring. rewrite H2. omega. assert (m * n - two_p (N + l) * q < two_p (N + l)). apply Zmult_lt_reg_r with d. omega. - rewrite H2. + rewrite H2. apply Zle_lt_trans with (two_p (N + l) * d - two_p l). - omega. + omega. exploit (two_p_gt_ZERO l). omega. omega. - symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q). + symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q). ring. omega. Qed. Lemma Zdiv_unique_2: forall x y q, y > 0 -> 0 < y * q - x <= y -> Zdiv x y = q - 1. Proof. - intros. apply Zdiv_unique with (x - (q - 1) * y). ring. - replace ((q - 1) * y) with (y * q - y) by ring. omega. + intros. apply Zdiv_unique with (x - (q - 1) * y). ring. + replace ((q - 1) * y) with (y * q - y) by ring. omega. Qed. Lemma Zdiv_mul_opp: @@ -116,29 +116,29 @@ Lemma Zdiv_mul_opp: Proof. intros m l l_pos [LO HI] n RANGE. replace (m * (-n)) with (- (m * n)) by ring. - exploit (Z_div_mod_eq n d). auto. + exploit (Z_div_mod_eq n d). auto. set (q := n / d). set (r := n mod d). intro EUCL. assert (0 <= r <= d - 1). unfold r. generalize (Z_mod_lt n d d_pos). omega. - assert (0 <= m). + assert (0 <= m). apply Zmult_le_0_reg_r with d. auto. exploit (two_p_gt_ZERO (N + l)). omega. omega. cut (Zdiv (- (m * n)) (two_p (N + l)) = -q - 1). omega. - apply Zdiv_unique_2. + apply Zdiv_unique_2. apply two_p_gt_ZERO. omega. replace (two_p (N + l) * - q - - (m * n)) with (m * n - two_p (N + l) * q) by ring. set (k := m * d - two_p (N + l)). - assert (0 < k <= two_p l). + assert (0 < k <= two_p l). unfold k; omega. assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). unfold k. rewrite EUCL. ring. split. - apply Zmult_lt_reg_r with d. omega. + apply Zmult_lt_reg_r with d. omega. replace (0 * d) with 0 by omega. rewrite H2. assert (0 < k * n). apply Zmult_lt_0_compat; omega. @@ -146,10 +146,10 @@ Proof. apply Zmult_le_0_compat. exploit (two_p_gt_ZERO (N + l)); omega. omega. omega. apply Zmult_le_reg_r with d. omega. - rewrite H2. + rewrite H2. assert (k * n <= two_p (N + l)). - rewrite Zplus_comm. rewrite two_p_is_exp; try omega. - apply Zle_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. + rewrite Zplus_comm. rewrite two_p_is_exp; try omega. + apply Zle_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). replace (two_p (N + l) * d - two_p (N + l)) @@ -170,12 +170,12 @@ Lemma Zquot_mul: Z.quot n d = Zdiv (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0). Proof. intros. destruct (zlt n 0). - exploit (Zdiv_mul_opp m l H H0 (-n)). omega. + exploit (Zdiv_mul_opp m l H H0 (-n)). omega. replace (- - n) with n by ring. replace (Z.quot n d) with (- Z.quot (-n) d). rewrite Zquot_Zdiv_pos by omega. omega. rewrite Z.quot_opp_l by omega. ring. - rewrite Zplus_0_r. rewrite Zquot_Zdiv_pos by omega. + rewrite Zplus_0_r. rewrite Zquot_Zdiv_pos by omega. apply Zdiv_mul_pos; omega. Qed. @@ -202,13 +202,13 @@ Proof with (try discriminate). destruct (zlt m Int.modulus)... destruct (zle 0 p)... destruct (zlt p 32)... - simpl in EQ. inv EQ. - split. auto. split. auto. intros. - replace (32 + p') with (31 + (p' + 1)) by omega. + simpl in EQ. inv EQ. + split. auto. split. auto. intros. + replace (32 + p') with (31 + (p' + 1)) by omega. apply Zquot_mul; try omega. replace (31 + (p' + 1)) with (32 + p') by omega. omega. - change (Int.min_signed <= n < Int.half_modulus). - unfold Int.max_signed in H. omega. + change (Int.min_signed <= n < Int.half_modulus). + unfold Int.max_signed in H. omega. Qed. Lemma divu_mul_params_sound: @@ -230,7 +230,7 @@ Proof with (try discriminate). destruct (zlt m Int.modulus)... destruct (zle 0 p)... destruct (zlt p 32)... - simpl in EQ. inv EQ. + simpl in EQ. inv EQ. split. auto. split. auto. intros. apply Zdiv_mul_pos; try omega. assumption. Qed. @@ -245,23 +245,23 @@ Proof. intros. set (n := Int.signed x). set (d := Int.signed y) in *. exploit divs_mul_params_sound; eauto. intros (A & B & C). split. auto. split. auto. - unfold Int.divs. fold n; fold d. rewrite C by (apply Int.signed_range). - rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv. + unfold Int.divs. fold n; fold d. rewrite C by (apply Int.signed_range). + rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv. rewrite Int.shru_lt_zero. unfold Int.add. apply Int.eqm_samerepr. apply Int.eqm_add. - rewrite Int.shr_div_two_p. apply Int.eqm_unsigned_repr_r. apply Int.eqm_refl2. + rewrite Int.shr_div_two_p. apply Int.eqm_unsigned_repr_r. apply Int.eqm_refl2. rewrite Int.unsigned_repr. f_equal. rewrite Int.signed_repr. rewrite Int.modulus_power. f_equal. ring. - cut (Int.min_signed <= n * m / Int.modulus < Int.half_modulus). - unfold Int.max_signed; omega. - apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos. + cut (Int.min_signed <= n * m / Int.modulus < Int.half_modulus). + unfold Int.max_signed; omega. + apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos. apply Int.modulus_pos. split. apply Zle_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega. apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto. - apply Zle_lt_trans with (Int.half_modulus * m). + apply Zle_lt_trans with (Int.half_modulus * m). apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto. - apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto. + apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto. assert (32 < Int.max_unsigned) by (compute; auto). omega. - unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr. + unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr. apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega. Qed. @@ -274,8 +274,8 @@ Theorem divs_mul_shift_1: Int.divs x y = Int.add (Int.shr (Int.mulhs x (Int.repr m)) (Int.repr p)) (Int.shru x (Int.repr 31)). Proof. - intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). - intros (A & B & C). split. auto. rewrite C. + intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). + intros (A & B & C). split. auto. rewrite C. unfold Int.mulhs. rewrite Int.signed_repr. auto. generalize Int.min_signed_neg; unfold Int.max_signed; omega. Qed. @@ -288,17 +288,17 @@ Theorem divs_mul_shift_2: Int.divs x y = Int.add (Int.shr (Int.add (Int.mulhs x (Int.repr m)) x) (Int.repr p)) (Int.shru x (Int.repr 31)). Proof. - intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). + intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). intros (A & B & C). split. auto. rewrite C. f_equal. f_equal. rewrite Int.add_signed. unfold Int.mulhs. set (n := Int.signed x). transitivity (Int.repr (n * (m - Int.modulus) / Int.modulus + n)). - f_equal. + f_equal. replace (n * (m - Int.modulus)) with (n * m + (-n) * Int.modulus) by ring. - rewrite Z_div_plus. ring. apply Int.modulus_pos. - apply Int.eqm_samerepr. apply Int.eqm_add; auto with ints. - apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned. - apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2. f_equal. f_equal. - rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption. + rewrite Z_div_plus. ring. apply Int.modulus_pos. + apply Int.eqm_samerepr. apply Int.eqm_add; auto with ints. + apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2. f_equal. f_equal. + rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption. apply zlt_false. omega. Qed. @@ -309,19 +309,19 @@ Theorem divu_mul_shift: Int.divu x y = Int.shru (Int.mulhu x (Int.repr m)) (Int.repr p). Proof. intros. exploit divu_mul_params_sound; eauto. intros (A & B & C). - split. auto. - rewrite Int.shru_div_two_p. rewrite Int.unsigned_repr. + split. auto. + rewrite Int.shru_div_two_p. rewrite Int.unsigned_repr. unfold Int.divu, Int.mulhu. f_equal. rewrite C by apply Int.unsigned_range. rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega). - f_equal. rewrite (Int.unsigned_repr m). + f_equal. rewrite (Int.unsigned_repr m). rewrite Int.unsigned_repr. f_equal. ring. cut (0 <= Int.unsigned x * m / Int.modulus < Int.modulus). unfold Int.max_unsigned; omega. apply Zdiv_interval_1. omega. compute; auto. compute; auto. - split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega. + split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega. apply Zle_lt_trans with (Int.modulus * m). - apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega. - apply Zmult_lt_compat_l. compute; auto. omega. + apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega. + apply Zmult_lt_compat_l. compute; auto. omega. unfold Int.max_unsigned; omega. assert (32 < Int.max_unsigned) by (compute; auto). omega. Qed. @@ -347,10 +347,10 @@ Proof. (Vint (Int.mulhu x (Int.repr M)))). { EvalOp. econstructor. econstructor; eauto. econstructor. EvalOp. simpl; reflexivity. constructor. auto. } - exploit eval_shruimm. eexact H1. instantiate (1 := Int.repr p). - intros [v [P Q]]. simpl in Q. - replace (Int.ltu (Int.repr p) Int.iwordsize) with true in Q. - inv Q. rewrite B. auto. + exploit eval_shruimm. eexact H1. instantiate (1 := Int.repr p). + intros [v [P Q]]. simpl in Q. + replace (Int.ltu (Int.repr p) Int.iwordsize) with true in Q. + inv Q. rewrite B. auto. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto. assert (32 < Int.max_unsigned) by (compute; auto). omega. Qed. @@ -363,17 +363,17 @@ Theorem eval_divuimm: Proof. unfold divuimm; intros. generalize H0; intros DIV. destruct x; simpl in DIV; try discriminate. - destruct (Int.eq n2 Int.zero) eqn:Z2; inv DIV. + destruct (Int.eq n2 Int.zero) eqn:Z2; inv DIV. destruct (Int.is_power2 n2) as [l | ] eqn:P2. -- erewrite Int.divu_pow2 by eauto. - replace (Vint (Int.shru i l)) with (Val.shru (Vint i) (Vint l)). +- erewrite Int.divu_pow2 by eauto. + replace (Vint (Int.shru i l)) with (Val.shru (Vint i) (Vint l)). apply eval_shruimm; auto. - simpl. erewrite Int.is_power2_range; eauto. + simpl. erewrite Int.is_power2_range; eauto. - destruct (Compopts.optim_for_size tt). + eapply eval_divu_base; eauto. EvalOp. + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. * exists (Vint (Int.divu i n2)); split; auto. - econstructor; eauto. eapply eval_divu_mul; eauto. + econstructor; eauto. eapply eval_divu_mul; eauto. * eapply eval_divu_base; eauto. EvalOp. Qed. @@ -386,7 +386,7 @@ Theorem eval_divu: Proof. unfold divu; intros until b. destruct (divu_match b); intros. - inv H0. inv H5. simpl in H7. inv H7. eapply eval_divuimm; eauto. -- eapply eval_divu_base; eauto. +- eapply eval_divu_base; eauto. Qed. Lemma eval_mod_from_div: @@ -395,8 +395,8 @@ Lemma eval_mod_from_div: nth_error le O = Some (Vint x) -> eval_expr ge sp e m le (mod_from_div a n) (Vint (Int.sub x (Int.mul y n))). Proof. - unfold mod_from_div; intros. - exploit eval_mulimm; eauto. instantiate (1 := n). intros [v [A B]]. + unfold mod_from_div; intros. + exploit eval_mulimm; eauto. instantiate (1 := n). intros [v [A B]]. simpl in B. inv B. EvalOp. Qed. @@ -408,7 +408,7 @@ Theorem eval_moduimm: Proof. unfold moduimm; intros. generalize H0; intros MOD. destruct x; simpl in MOD; try discriminate. - destruct (Int.eq n2 Int.zero) eqn:Z2; inv MOD. + destruct (Int.eq n2 Int.zero) eqn:Z2; inv MOD. destruct (Int.is_power2 n2) as [l | ] eqn:P2. - erewrite Int.modu_and by eauto. change (Vint (Int.and i (Int.sub n2 Int.one))) @@ -417,10 +417,10 @@ Proof. - destruct (Compopts.optim_for_size tt). + eapply eval_modu_base; eauto. EvalOp. + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. - * econstructor; split. - econstructor; eauto. eapply eval_mod_from_div. - eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. - rewrite Int.modu_divu. auto. + * econstructor; split. + econstructor; eauto. eapply eval_mod_from_div. + eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. + rewrite Int.modu_divu. auto. red; intros; subst n2; discriminate. * eapply eval_modu_base; eauto. EvalOp. Qed. @@ -434,7 +434,7 @@ Theorem eval_modu: Proof. unfold modu; intros until b. destruct (modu_match b); intros. - inv H0. inv H5. simpl in H7. inv H7. eapply eval_moduimm; eauto. -- eapply eval_modu_base; eauto. +- eapply eval_modu_base; eauto. Qed. Lemma eval_divs_mul: @@ -451,10 +451,10 @@ Proof. (Vint (Int.mulhs x (Int.repr M)))). { EvalOp. econstructor. eauto. econstructor. EvalOp. simpl; reflexivity. constructor. auto. } - exploit eval_shruimm. eexact V. instantiate (1 := Int.repr (Int.zwordsize - 1)). - intros [v1 [Y LD]]. simpl in LD. - change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. - simpl in LD. inv LD. + exploit eval_shruimm. eexact V. instantiate (1 := Int.repr (Int.zwordsize - 1)). + intros [v1 [Y LD]]. simpl in LD. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. + simpl in LD. inv LD. assert (RANGE: 0 <= p < 32 -> Int.ltu (Int.repr p) Int.iwordsize = true). { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto. assert (32 < Int.max_unsigned) by (compute; auto). omega. } @@ -463,15 +463,15 @@ Proof. exploit eval_shrimm. eexact X. instantiate (1 := Int.repr p). intros [v1 [Z LD]]. simpl in LD. rewrite RANGE in LD by auto. inv LD. exploit eval_add. eexact Z. eexact Y. intros [v1 [W LD]]. - simpl in LD. inv LD. + simpl in LD. inv LD. rewrite B. exact W. - exploit (divs_mul_shift_2 x); eauto. intros [A B]. - exploit eval_add. eexact X. eexact V. intros [v1 [Z LD]]. - simpl in LD. inv LD. + exploit eval_add. eexact X. eexact V. intros [v1 [Z LD]]. + simpl in LD. inv LD. exploit eval_shrimm. eexact Z. instantiate (1 := Int.repr p). intros [v1 [U LD]]. simpl in LD. rewrite RANGE in LD by auto. inv LD. exploit eval_add. eexact U. eexact Y. intros [v1 [W LD]]. - simpl in LD. inv LD. + simpl in LD. inv LD. rewrite B. exact W. Qed. @@ -484,7 +484,7 @@ Proof. unfold divsimm; intros. generalize H0; intros DIV. destruct x; simpl in DIV; try discriminate. destruct (Int.eq n2 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. + || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. destruct (Int.is_power2 n2) as [l | ] eqn:P2. - destruct (Int.ltu l (Int.repr 31)) eqn:LT31. + eapply eval_shrximm; eauto. eapply Val.divs_pow2; eauto. @@ -493,7 +493,7 @@ Proof. + eapply eval_divs_base; eauto. EvalOp. + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. * exists (Vint (Int.divs i n2)); split; auto. - econstructor; eauto. eapply eval_divs_mul; eauto. + econstructor; eauto. eapply eval_divs_mul; eauto. * eapply eval_divs_base; eauto. EvalOp. Qed. @@ -506,7 +506,7 @@ Theorem eval_divs: Proof. unfold divs; intros until b. destruct (divs_match b); intros. - inv H0. inv H5. simpl in H7. inv H7. eapply eval_divsimm; eauto. -- eapply eval_divs_base; eauto. +- eapply eval_divs_base; eauto. Qed. Theorem eval_modsimm: @@ -515,25 +515,25 @@ Theorem eval_modsimm: Val.mods x (Vint n2) = Some z -> exists v, eval_expr ge sp e m le (modsimm e1 n2) v /\ Val.lessdef z v. Proof. - unfold modsimm; intros. + unfold modsimm; intros. exploit Val.mods_divs; eauto. intros [y [A B]]. generalize A; intros DIV. destruct x; simpl in DIV; try discriminate. destruct (Int.eq n2 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. + || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. destruct (Int.is_power2 n2) as [l | ] eqn:P2. - destruct (Int.ltu l (Int.repr 31)) eqn:LT31. + exploit (eval_shrximm ge sp e m (Vint i :: le) (Eletvar O)). - constructor. simpl; eauto. eapply Val.divs_pow2; eauto. - intros [v1 [X LD]]. inv LD. - econstructor; split. econstructor. eauto. - apply eval_mod_from_div. eexact X. simpl; eauto. + constructor. simpl; eauto. eapply Val.divs_pow2; eauto. + intros [v1 [X LD]]. inv LD. + econstructor; split. econstructor. eauto. + apply eval_mod_from_div. eexact X. simpl; eauto. simpl. auto. + eapply eval_mods_base; eauto. EvalOp. - destruct (Compopts.optim_for_size tt). + eapply eval_mods_base; eauto. EvalOp. + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. - * econstructor; split. + * econstructor; split. econstructor. eauto. apply eval_mod_from_div with (x := i); auto. eapply eval_divs_mul with (x := i); eauto. simpl. auto. @@ -549,7 +549,7 @@ Theorem eval_mods: Proof. unfold mods; intros until b. destruct (mods_match b); intros. - inv H0. inv H5. simpl in H7. inv H7. eapply eval_modsimm; eauto. -- eapply eval_mods_base; eauto. +- eapply eval_mods_base; eauto. Qed. (** * Floating-point division *) @@ -563,10 +563,10 @@ Proof. intros until y. unfold divf. destruct (divf_match b); intros. - unfold divfimm. destruct (Float.exact_inverse n2) as [n2' | ] eqn:EINV. + inv H0. inv H4. simpl in H6. inv H6. econstructor; split. - EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. - simpl; eauto. - destruct x; simpl; auto. erewrite Float.div_mul_inverse; eauto. - + TrivialExists. + EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. + simpl; eauto. + destruct x; simpl; auto. erewrite Float.div_mul_inverse; eauto. + + TrivialExists. - TrivialExists. Qed. @@ -579,10 +579,10 @@ Proof. intros until y. unfold divfs. destruct (divfs_match b); intros. - unfold divfsimm. destruct (Float32.exact_inverse n2) as [n2' | ] eqn:EINV. + inv H0. inv H4. simpl in H6. inv H6. econstructor; split. - EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. - simpl; eauto. - destruct x; simpl; auto. erewrite Float32.div_mul_inverse; eauto. - + TrivialExists. + EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. + simpl; eauto. + destruct x; simpl; auto. erewrite Float32.div_mul_inverse; eauto. + + TrivialExists. - TrivialExists. Qed. -- cgit