Commit c146b544 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Changed NE to generic NE (abs-based) and finished proof.

parent 9004703e
......@@ -434,16 +434,32 @@ apply epow_gt_0.
exact Hx.
Qed.
Theorem generic_format_0 :
generic_format 0.
Proof.
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
Qed.
Theorem canonic_sym :
forall x m e,
canonic x (Float beta m e) ->
canonic (-x) (Float beta (-m) e).
Proof.
intros x m e (H1,H2).
split.
rewrite H1.
apply opp_F2R.
now rewrite Rabs_Ropp.
Qed.
Theorem generic_format_sym :
forall x, generic_format x -> generic_format (-x).
Proof.
intros x ((m,e),(H1,H2)).
exists (Float beta (-m) _) ; repeat split.
rewrite H1 at 1.
rewrite Rabs_Ropp.
rewrite opp_F2R.
apply (f_equal (fun v => F2R (Float beta (- m) v))).
exact H2.
intros x ((m,e),H).
exists (Float beta (-m) e).
now apply canonic_sym.
Qed.
Theorem generic_format_satisfies_any :
......@@ -451,9 +467,7 @@ Theorem generic_format_satisfies_any :
Proof.
refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
(* symmetric set *)
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
exact generic_format_0.
exact generic_format_sym.
(* rounding down *)
exists (fun x =>
......
......@@ -19,17 +19,19 @@ Variable prop_exp : valid_exp fexp.
Notation generic_format := (generic_format beta fexp).
Notation canonic := (canonic beta fexp).
Definition Rnd_NE_pt (x f : R) :=
Definition Rnd_gNE_pt (x f : R) :=
Rnd_N_pt generic_format x f /\
( ( exists g : float beta, canonic f g /\ Zeven (Fnum g) ) \/
( forall f2 : R, Rnd_N_pt generic_format x f2 -> f2 = f ) ).
( ( exists g : float beta, canonic f g /\ Zeven (Fnum g) /\
forall f2 : R, forall g : float beta, Rnd_N_pt generic_format x f2 ->
canonic f2 g -> Zeven (Fnum g) -> (Rabs f2 <= Rabs f)%R ) \/
( forall f2 : R, Rnd_N_pt generic_format x f2 -> f = f2 ) ).
Definition Rnd_NE (rnd : R -> R) :=
forall x : R, Rnd_NE_pt x (rnd x).
Definition Rnd_gNE (rnd : R -> R) :=
forall x : R, Rnd_gNE_pt x (rnd x).
Theorem Rnd_NE_pt_sym :
Theorem Rnd_gNE_pt_sym :
forall x f : R,
Rnd_NE_pt (-x) (-f) -> Rnd_NE_pt x f.
Rnd_gNE_pt (-x) (-f) -> Rnd_gNE_pt x f.
Proof.
intros x f (H1,H2).
split.
......@@ -47,6 +49,17 @@ now rewrite H3, Rabs_Ropp.
simpl in H4 |- *.
rewrite Zopp_eq_mult_neg_1.
now apply Zeven_mult_Zeven_l.
intros f2 g Hx Hxg Hg.
rewrite <- (Rabs_Ropp f), <- (Rabs_Ropp f2).
eapply H4.
apply Rnd_N_pt_sym.
apply generic_format_sym.
now rewrite 2!Ropp_involutive.
eapply canonic_sym.
eexact Hxg.
simpl.
rewrite Zopp_eq_mult_neg_1.
now apply Zeven_mult_Zeven_l.
(* . *)
right.
intros f2 H3.
......@@ -58,87 +71,121 @@ apply generic_format_sym.
now rewrite 2!Ropp_involutive.
Qed.
Theorem Rnd_NE_pt_unicity :
forall x f1 f2 : R,
Rnd_NE_pt x f1 -> Rnd_NE_pt x f2 ->
f1 = f2.
Lemma canonic_imp_Fnum :
forall x, forall f : float beta,
x <> R0 ->
canonic x f ->
(Zabs (Fnum f) < Zpower (radix_val beta) (projT1 (ln_beta beta (Rabs x)) - Fexp f))%Z.
Proof.
intros x f1 f2 (H1,[H2|H2]) (H3,H4).
destruct H4 as [H4|H4].
destruct (Req_dec x f1) as [H5|H5].
intros x f Hx.
unfold Flocq_rnd_generic.canonic.
destruct (ln_beta beta (Rabs x)) as (ex, H).
simpl.
specialize (H (Rabs_pos_lt x Hx)).
intros (H1, H2).
destruct (Zle_or_lt (Fexp f) ex) as [He|He].
(* . *)
rewrite <- H5.
apply sym_eq.
apply (Rnd_N_pt_idempotent generic_format).
exact H3.
rewrite H5.
apply H1.
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow (Fexp f)).
apply epow_gt_0.
replace (Z2R (Zabs (Fnum f)) * bpow (Fexp f))%R with (Rabs x).
rewrite Z2R_Zpower, <- epow_add.
now ring_simplify (ex - Fexp f + Fexp f)%Z.
omega.
rewrite H1.
apply abs_F2R.
(* . *)
destruct (satisfies_any_imp_DN _ (generic_format_satisfies_any beta fexp prop_exp)) as (rndD, Hd).
destruct (satisfies_any_imp_UP _ (generic_format_satisfies_any beta fexp prop_exp)) as (rndU, Hu).
assert (forall d u, canonic (rndD x) d -> canonic (rndU x) u -> d <> u ->
Zeven (Fnum d) -> Zeven (Fnum u) -> False).
clear -prop_exp Hd Hu.
intros d u Cd Cu Hdu Ed Eu.
apply (Zeven_not_Zodd (Fnum u)).
exact Eu.
Check (ulp_pred_succ_pt beta fexp prop_exp x (rndU x)).
admit.
elim (Rlt_not_ge _ _ (proj2 H)).
apply Rle_ge.
rewrite H1.
destruct f as (xm, xe).
rewrite abs_F2R.
unfold F2R. simpl.
rewrite <- (Rmult_1_l (bpow ex)).
apply Rmult_le_compat.
now apply (Z2R_le 0 1).
apply epow_ge_0.
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow xe).
apply epow_gt_0.
rewrite Rmult_0_l.
replace (Z2R (Zabs xm) * bpow xe)%R with (Rabs x).
now apply Rabs_pos_lt.
rewrite H1.
apply abs_F2R.
apply -> epow_le.
now apply Zlt_le_weak.
Qed.
Theorem Rnd_gNE_pt_unicity :
forall x f1 f2 : R,
Rnd_gNE_pt x f1 -> Rnd_gNE_pt x f2 ->
f1 = f2.
Proof.
intros x f1 f2 (H1,[Hf1|Hf1]) (H2,Hf2).
destruct Hf2 as [Hf2|Hf2].
(* . *)
destruct (Rnd_N_pt_DN_or_UP generic_format x (rndD x) (rndU x) f1) as [H6|H6].
apply Hd.
apply Hu.
apply H1.
destruct (Rnd_N_pt_DN_or_UP generic_format x (rndD x) (rndU x) f2) as [H7|H7].
apply Hd.
apply Hu.
apply H3.
now rewrite H6, H7.
destruct H2 as (d,(H2a,H2b)).
destruct H4 as (u,(H4a,H4b)).
elim (H d u) ; try assumption.
now rewrite <- H6.
now rewrite <- H7.
intros H8. apply H5.
apply Rle_antisym.
rewrite (proj1 H2a), H8, <- (proj1 H4a), H7.
eapply Hu.
rewrite H6.
eapply Hd.
destruct (Rnd_N_pt_DN_or_UP generic_format x (rndD x) (rndU x) f2) as [H7|H7].
apply Hd.
apply Hu.
apply H3.
destruct H2 as (u,(H2a,H2b)).
destruct H4 as (d,(H4a,H4b)).
elim (H d u) ; try assumption.
now rewrite <- H7.
now rewrite <- H6.
intros H8. apply H5.
destruct Hf1 as (g1, (Hg1a, (Hg1b, Hg1c))).
destruct Hf2 as (g2, (Hg2a, (Hg2b, Hg2c))).
assert (Rabs f1 = Rabs f2).
apply Rle_antisym.
rewrite H6.
eapply Hu.
rewrite (proj1 H2a), <- H8, <- (proj1 H4a), H7.
eapply Hd.
now rewrite H6, H7.
now apply Hg2c with g1.
now apply Hg1c with g2.
destruct (Rle_or_lt 0 x) as [Hx|Hx].
rewrite (Rabs_pos_eq f1) in H.
rewrite H.
apply Rabs_pos_eq.
apply Rnd_N_pt_pos with generic_format x.
apply generic_format_0.
exact Hx.
exact H2.
apply Rnd_N_pt_pos with generic_format x.
apply generic_format_0.
exact Hx.
exact H1.
rewrite (Rabs_left1 f1) in H.
rewrite <- (Ropp_involutive f1), <- (Ropp_involutive f2).
rewrite H.
apply f_equal.
apply Rabs_left1.
apply Rnd_N_pt_neg with generic_format x.
apply generic_format_0.
now apply Rlt_le.
exact H2.
apply Rnd_N_pt_neg with generic_format x.
apply generic_format_0.
now apply Rlt_le.
exact H1.
(* . *)
now apply H4.
apply sym_eq.
now apply H2.
now apply Hf2.
now apply Hf1.
Qed.
Theorem Rnd_NE_pt_monotone :
Theorem Rnd_gNE_pt_monotone :
forall x y f g : R,
Rnd_NE_pt x f -> Rnd_NE_pt y g ->
Rnd_gNE_pt x f -> Rnd_gNE_pt y g ->
(x <= y)%R -> (f <= g)%R.
Proof.
intros x y f g (Hx1,Hx2) (Hy1,Hy2) [Hxy|Hxy].
eapply Rnd_N_pt_monotone ; eassumption.
apply Req_le.
apply Rnd_NE_pt_unicity with x.
apply Rnd_gNE_pt_unicity with x.
now split.
rewrite Hxy.
now split.
Qed.
Theorem Rnd_gNE_pt_idempotent :
forall x f : R,
Rnd_gNE_pt x f -> generic_format x ->
f = x.
Proof.
intros x f Hxf Hx.
destruct Hxf as (Hxf1,_).
now apply Rnd_N_pt_idempotent with generic_format.
Qed.
End Flocq_rnd_NE.
......@@ -490,6 +490,50 @@ intros x Hx.
now apply Rnd_N_pt_idempotent with F.
Qed.
Theorem Rnd_N_pt_0 :
forall F : R -> Prop,
F 0 ->
Rnd_N_pt F 0 0.
Proof.
intros F HF.
split.
exact HF.
intros g _.
rewrite 2!Rminus_0_r, Rabs_R0.
apply Rabs_pos.
Qed.
Theorem Rnd_N_pt_pos :
forall F : R -> Prop, F 0 ->
forall x f, 0 <= x ->
Rnd_N_pt F x f ->
0 <= f.
Proof.
intros F HF x f [Hx|Hx] Hxf.
eapply Rnd_N_pt_monotone ; try eassumption.
now apply Rnd_N_pt_0.
right.
apply sym_eq.
apply Rnd_N_pt_idempotent with F.
now rewrite Hx.
exact HF.
Qed.
Theorem Rnd_N_pt_neg :
forall F : R -> Prop, F 0 ->
forall x f, x <= 0 ->
Rnd_N_pt F x f ->
f <= 0.
Proof.
intros F HF x f [Hx|Hx] Hxf.
eapply Rnd_N_pt_monotone ; try eassumption.
now apply Rnd_N_pt_0.
right.
apply Rnd_N_pt_idempotent with F.
now rewrite <- Hx.
exact HF.
Qed.
Theorem Rnd_NA_pt_monotone :
forall F : R -> Prop,
F 0 ->
......
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