Commit bea08189 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Simplify some proofs.

parent 3e01dd65
......@@ -18,6 +18,7 @@ COPYING file for more details.
*)
(** * Missing definitions/lemmas *)
Require Import Psatz.
Require Export Reals ZArith.
Require Export Zaux.
......@@ -57,10 +58,8 @@ Theorem Rabs_minus_le:
(Rabs (x-y) <= x)%R.
Proof.
intros x y Hx Hy.
unfold Rabs; case (Rcase_abs (x - y)); intros H.
apply Rplus_le_reg_l with x; ring_simplify; assumption.
apply Rplus_le_reg_l with (-x)%R; ring_simplify.
auto with real.
apply Rabs_le.
lra.
Qed.
Theorem Rplus_eq_reg_r :
......
......@@ -320,18 +320,17 @@ apply Rle_refl.
(* . *)
destruct (Rle_or_lt 0 x).
(* positive *)
rewrite Rabs_right.
rewrite Rabs_right; auto with real.
rewrite Rabs_pos_eq with (1 := H1).
rewrite Rabs_pos_eq.
now apply (proj1 (H x)).
apply Rle_ge.
now apply (proj1 (H x)).
(* negative *)
apply Rlt_le in H1.
rewrite Rabs_left1 with (1 := H1).
rewrite Rabs_left1.
rewrite Rabs_left1 ; auto with real.
apply Ropp_le_contravar.
apply (proj2 (H x)).
auto with real.
apply (proj2 (H x)) ; auto with real.
now apply (proj2 (H x)).
now apply (proj2 (H x)).
Qed.
Theorem Rnd_ZR_pt_monotone :
......
......@@ -753,7 +753,7 @@ apply bpow_gt_0.
pattern x at 1; rewrite <- (Ropp_involutive x).
apply Ropp_lt_contravar.
apply pred_pos_lt_id.
now auto with real.
auto with real.
Qed.
......@@ -765,7 +765,7 @@ intros x Zx; unfold pred.
pattern x at 2; rewrite <- (Ropp_involutive x).
apply Ropp_lt_contravar.
apply succ_gt_id.
now auto with real.
auto with real.
Qed.
Theorem succ_ge_id :
......@@ -837,14 +837,13 @@ assert (Lex:(mag_val beta x (mag beta x) = ex)%Z).
rewrite T; reflexivity.
rewrite Lex in *.
clear T; simpl in *; specialize (Hex H).
rewrite Rabs_right in Hex.
2: apply Rle_ge; apply Rlt_le; easy.
assert (ex-1 < fexp ex < ex)%Z.
split ; apply (lt_bpow beta); rewrite <- M;[idtac|easy].
destruct (proj1 Hex);[trivial|idtac].
contradict Hx; auto with real.
rewrite Rabs_pos_eq in Hex by now apply Rlt_le.
assert (ex - 1 < fexp ex < ex)%Z.
split ; apply (lt_bpow beta) ; rewrite <- M by easy.
lra.
apply Hex.
omega.
rewrite 2!ulp_neq_0; try auto with real.
rewrite 2!ulp_neq_0 by lra.
apply f_equal.
unfold cexp ; apply f_equal.
case_eq (mag beta x); intros ex Hex T.
......@@ -863,7 +862,7 @@ apply id_m_ulp_ge_bpow; trivial.
rewrite ulp_neq_0; trivial.
rewrite ulp_neq_0; trivial.
right; unfold cexp; now rewrite Lex.
contradict Hx; auto with real.
lra.
apply Rle_lt_trans with (2:=proj2 Hex).
rewrite <- Rplus_0_r.
apply Rplus_le_compat_l.
......@@ -1078,8 +1077,7 @@ revert Heps; unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
intros _ (H1,H2).
absurd (0 < 0)%R; auto with real.
now apply Rle_lt_trans with (1:=H1).
exfalso ; lra.
intros n Hn H.
assert (fexp (mag beta eps) = fexp n).
apply valid_exp; try assumption.
......@@ -1145,9 +1143,7 @@ unfold round, scaled_mantissa, cexp.
unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
intros H2.
intros J; absurd (0 < 0)%R; auto with real.
apply Rlt_trans with eps; try assumption; apply Heps.
lra.
intros n Hn H.
assert (fexp (mag beta eps) = fexp n).
apply valid_exp; try assumption.
......
......@@ -614,11 +614,10 @@ destruct (mag beta x) as (e,He); simpl.
assert (e-1 < emin+prec)%Z.
apply (lt_bpow beta).
apply Rle_lt_trans with (2:=Hx).
rewrite <- (Rabs_right x).
apply He; auto with real.
apply Rle_ge; now left.
rewrite <- (Rabs_pos_eq x) by now apply Rlt_le.
now apply He, Rgt_not_eq.
omega.
split;ring.
split ; ring.
Qed.
End Fprop_relative_FLT.
......
......@@ -814,8 +814,9 @@ now apply fexp_m_eq_0.
Qed.
Lemma DN_odd_d_aux: forall z, (F2R d<= z< F2R u)%R ->
Rnd_DN_pt (generic_format beta fexp) z (F2R d).
Lemma DN_odd_d_aux :
forall z, (F2R d <= z < F2R u)%R ->
Rnd_DN_pt (generic_format beta fexp) z (F2R d).
Proof with auto with typeclass_instances.
intros z Hz1.
replace (F2R d) with (round beta fexp Zfloor z).
......@@ -826,22 +827,21 @@ intros Y; apply Rle_antisym; trivial.
apply round_DN_pt...
apply Hd.
apply Hz1.
intros Y; absurd (z < z)%R.
auto with real.
intros Y ; elim (Rlt_irrefl z).
apply Rlt_le_trans with (1:=proj2 Hz1), Rle_trans with (1:=Y).
apply round_DN_pt...
Qed.
Lemma UP_odd_d_aux: forall z, (F2R d< z <= F2R u)%R ->
Rnd_UP_pt (generic_format beta fexp) z (F2R u).
Lemma UP_odd_d_aux :
forall z, (F2R d < z <= F2R u)%R ->
Rnd_UP_pt (generic_format beta fexp) z (F2R u).
Proof with auto with typeclass_instances.
intros z Hz1.
replace (F2R u) with (round beta fexp Zceil z).
apply round_UP_pt...
case (Rnd_DN_UP_pt_split _ _ _ _ Hd Hu (round beta fexp Zceil z)).
apply generic_format_round...
intros Y; absurd (z < z)%R.
auto with real.
intros Y ; elim (Rlt_irrefl z).
apply Rle_lt_trans with (2:=proj1 Hz1), Rle_trans with (2:=Y).
apply round_UP_pt...
intros Y; apply Rle_antisym; trivial.
......
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