Commit b28d90f7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix some compilation issues.

parent 8ceec0c2
......@@ -201,7 +201,7 @@ apply Rmult_le_compat_r.
apply ulp_ge_0.
left; apply Rlt_plus_1.
rewrite 2!ulp_neq_0; trivial.
2: now apply Rmult_integral_contrapositive_currified.
2: lra.
change 2 at 2 with (bpow 1).
rewrite <- bpow_plus.
apply bpow_le.
......@@ -221,18 +221,16 @@ rewrite Rabs_mult.
pattern (Rabs u) at 1; rewrite <- (Rmult_1_l (Rabs u)).
apply Rmult_le_compat_r.
apply Rabs_pos.
change 2 with (Z2R 2).
rewrite <- (Z2R_abs 2).
now apply (Z2R_le 1 2).
(* *)
case (Req_dec u 0); intros K.
rewrite K, Rmult_0_r.
omega.
rewrite canonic_exp_FLT_FIX.
rewrite canonic_exp_FLT_FIX; trivial.
unfold FIX_exp, canonic_exp; omega.
apply Rlt_le_trans with (1:=Hu).
apply bpow_le; omega.
apply Rmult_integral_contrapositive_currified; trivial.
lra.
rewrite Rabs_mult.
rewrite Rabs_pos_eq.
2: now apply (Z2R_le 0 2).
......@@ -1449,7 +1447,7 @@ destruct uLev as [uLtv|uEqv].
(* when u < v *)
assert (B: u <= v) by now left.
assert (K1: b <> 0).
apply Rmult_integral_contrapositive_currified ; lra.
unfold b ; lra.
(* . initial lemma *)
assert (Y:(Rabs (round_flt (v - u) - (v-u)) <= ulp_flt b)).
apply Rle_trans with (/2*ulp_flt (v-u)).
......@@ -1467,7 +1465,7 @@ apply ulp_le_pos...
lra.
unfold b ; lra.
rewrite 2!ulp_neq_0; trivial.
2: apply Rmult_integral_contrapositive_currified; trivial.
2: lra.
change 2 with (bpow 1).
rewrite <- bpow_plus.
apply bpow_le.
......@@ -1553,10 +1551,8 @@ apply Rmult_eq_reg_l with 2.
rewrite Rmult_0_r, J1,M; unfold F2R; simpl; ring.
rewrite Rabs_mult.
rewrite Rabs_right.
2: apply Rle_ge; auto with real.
apply Rmult_le_compat_l.
lra.
exact Y.
2: lra.
apply Rmult_le_compat_l with (2 := Y).
lra.
apply round_generic...
apply FLT_format_half...
......
......@@ -183,8 +183,8 @@ destruct (Req_dec x' 0) as [Zx'|Nzx'].
apply Rplus_le_compat_r.
apply (Rmult_le_reg_r (bpow (- ln_beta x))); [now apply bpow_gt_0|].
unfold ulp, canonic_exp; bpow_simplify.
replace 1%R with (/2 * 2)%R by field.
apply Rmult_le_compat_l; [lra|].
apply Rmult_le_reg_l with (1 := Rlt_0_2).
replace (2 * (/ 2 * _)) with (bpow (fexp1 (ln_beta x) - ln_beta x)) by field.
apply Rle_trans with 1; [|lra].
change 1 with (bpow 0); apply bpow_le.
omega.
......@@ -1461,6 +1461,7 @@ apply double_round_gt_mid.
unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
rewrite Zmult_1_r.
apply Z2R_le, Rinv_le in Hbeta.
simpl in Hbeta.
lra.
apply Rlt_0_2.
Qed.
......
......@@ -709,7 +709,7 @@ unfold F2R; simpl; unfold Z.pow_pos; simpl.
rewrite Zmult_1_r, Hb, Z2R_mult.
simpl; field.
apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2).
rewrite Rmult_0_r, <-Z2R_mult, <-Hb.
rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb.
apply radix_pos.
apply trans_eq with (-1+Fexp (Fplus beta d u'))%Z.
unfold Fmult.
......@@ -737,7 +737,7 @@ unfold F2R; simpl; unfold Z.pow_pos; simpl.
rewrite Zmult_1_r, Hb, Z2R_mult.
simpl; field.
apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2).
rewrite Rmult_0_r, <-Z2R_mult, <-Hb.
rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb.
apply radix_pos.
apply trans_eq with (-1+Fexp u)%Z.
unfold Fmult.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment