Commit 11fe817a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Simplified proofs.

parent 7773d1aa
......@@ -80,9 +80,7 @@ destruct (Rdichotomy x 0) as [Hx2|Hx2].
intros Hx.
elim Fx.
rewrite Hx.
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
apply generic_format_0.
(* negative *)
assert (Hu2 : Rnd_DN_pt F (-x) (-xu)).
apply Rnd_UP_DN_pt_sym.
......@@ -119,9 +117,8 @@ Theorem ulp_error :
Proof.
intros rnd Hrnd x.
assert (Hs := generic_format_satisfies_any beta _ prop_exp).
destruct (rounding_fun_of_pred _ (satisfies_any_imp_DN F Hs)) as (rndd, Hd).
specialize (Hd x).
destruct (Rle_lt_or_eq_dec (rndd x) x) as [Hxd|Hxd].
destruct (proj1 (satisfies_any_imp_DN F Hs) x) as (d, Hd).
destruct (Rle_lt_or_eq_dec d x) as [Hxd|Hxd].
(* x <> rnd x *)
apply Hd.
assert (Fx : ~F x).
......@@ -130,22 +127,21 @@ apply Rlt_not_le with (1 := Hxd).
apply Req_le.
apply sym_eq.
now apply Rnd_DN_pt_idempotent with (1 := Hd).
destruct (rounding_fun_of_pred _ (satisfies_any_imp_UP F Hs)) as (rndu, Hu).
specialize (Hu x).
assert (Hxu : (x < rndu x)%R).
apply Rnot_le_lt.
intros Hxu.
apply Fx.
rewrite Rle_antisym with (2 := Hxu).
destruct (proj1 (satisfies_any_imp_UP F Hs) x) as (u, Hu).
assert (Hxu : (x < u)%R).
destruct (Rle_lt_or_eq_dec x u) as [Hxu|Hxu].
apply Hu.
exact Hxu.
elim Fx.
rewrite Hxu.
apply Hu.
rewrite (ulp_pred_succ_pt _ _ _ Fx Hd Hu) in Hxu, Hu.
destruct (Rnd_DN_or_UP_pt _ _ Hrnd _ _ _ Hd Hu) as [Hr|Hr] ;
rewrite Hr ; clear Hr.
rewrite <- Ropp_minus_distr.
rewrite Rabs_Ropp, Rabs_pos_eq.
apply Rplus_lt_reg_r with (rndd x).
now replace (rndd x + (x - rndd x))%R with x by ring.
apply Rplus_lt_reg_r with d.
now replace (d + (x - d))%R with x by ring.
apply Rle_0_minus.
apply Hd.
rewrite Rabs_pos_eq.
......@@ -172,9 +168,8 @@ Theorem ulp_half_error_pt :
Proof.
intros x xr Hxr.
assert (Hs := generic_format_satisfies_any beta _ prop_exp).
destruct (rounding_fun_of_pred _ (satisfies_any_imp_DN F Hs)) as (rndd, Hd).
specialize (Hd x).
destruct (Rle_lt_or_eq_dec (rndd x) x) as [Hxd|Hxd].
destruct (proj1 (satisfies_any_imp_DN F Hs) x) as (d, Hd).
destruct (Rle_lt_or_eq_dec d x) as [Hxd|Hxd].
(* x <> rnd x *)
apply Hd.
assert (Fx : ~F x).
......@@ -183,21 +178,20 @@ apply Rlt_not_le with (1 := Hxd).
apply Req_le.
apply sym_eq.
now apply Rnd_DN_pt_idempotent with (1 := Hd).
destruct (rounding_fun_of_pred _ (satisfies_any_imp_UP F Hs)) as (rndu, Hu).
specialize (Hu x).
destruct (proj1 (satisfies_any_imp_UP F Hs) x) as (u, Hu).
rewrite (ulp_pred_succ_pt _ _ _ Fx Hd Hu) in Hu.
destruct Hxr as (Hr1, Hr2).
assert (Hdx : (Rabs (rndd x - x) = x - rndd x)%R).
assert (Hdx : (Rabs (d - x) = x - d)%R).
rewrite <- Ropp_minus_distr.
rewrite Rabs_Ropp.
apply Rabs_pos_eq.
apply Rle_0_minus.
apply Hd.
assert (Hux : (Rabs (rndd x + ulp x - x) = rndd x + ulp x - x)%R).
assert (Hux : (Rabs (d + ulp x - x) = d + ulp x - x)%R).
apply Rabs_pos_eq.
apply Rle_0_minus.
apply Hu.
destruct (Rle_or_lt (x - rndd x) (rndd x + ulp x - x)) as [H|H].
destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H].
(* . rnd(x) = rndd(x) *)
apply Rle_trans with (1 := Hr2 _ (proj1 Hd)).
rewrite Hdx.
......@@ -205,7 +199,7 @@ apply Rmult_le_reg_l with 2%R.
now apply (Z2R_lt 0 2).
rewrite Rmult_plus_distr_r.
rewrite Rmult_1_l.
apply Rle_trans with (1 := Rplus_le_compat_l (x - rndd x) _ _ H).
apply Rle_trans with (1 := Rplus_le_compat_l (x - d) _ _ H).
field_simplify.
apply Rle_refl.
(* . rnd(x) = rndu(x) *)
......@@ -216,7 +210,7 @@ now apply (Z2R_lt 0 2).
rewrite Rmult_plus_distr_r.
rewrite Rmult_1_l.
apply Rlt_le.
apply Rlt_le_trans with (1 := Rplus_lt_compat_l (rndd x + ulp x - x) _ _ H).
apply Rlt_le_trans with (1 := Rplus_lt_compat_l (d + ulp x - x) _ _ H).
field_simplify.
apply Rle_refl.
(* x = rnd x *)
......
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