From 62deca00248fb3b3f895efdff9a9ef6d4e94c837 Mon Sep 17 00:00:00 2001 From: Sylvie Boldo Date: Tue, 13 Dec 2016 14:44:54 +0100 Subject: [PATCH] Modified ln_beta_lt_pos + changes in Fprop_plus_error + minor stuff # Conflicts: # src/Prop/Plus_error.v --- examples/Triangle.v | 8 +- src/Core/Raux.v | 9 +- src/Prop/Double_rounding.v | 2 +- src/Prop/Plus_error.v | 229 +++++++++++++++++++++++++++------- src/Translate/Missing_theos.v | 30 ++++- 5 files changed, 223 insertions(+), 55 deletions(-) diff --git a/examples/Triangle.v b/examples/Triangle.v index 9abf4fe..9a36697 100644 --- a/examples/Triangle.v +++ b/examples/Triangle.v @@ -1,8 +1,8 @@ Require Import Reals. -Require Import Fcore. -Require Import Fprop_relative. -Require Import Fprop_Sterbenz. -Require Import Fcalc_ops. +Require Import Flocq.Core.Fcore. +Require Import Flocq.Prop.Fprop_relative. +Require Import Flocq.Prop.Fprop_Sterbenz. +Require Import Flocq.Calc.Fcalc_ops. Require Import Interval.Interval_tactic. Section Delta_FLX. diff --git a/src/Core/Raux.v b/src/Core/Raux.v index d340dfb..3080a47 100644 --- a/src/Core/Raux.v +++ b/src/Core/Raux.v @@ -1838,10 +1838,13 @@ Qed. Lemma ln_beta_lt_pos : forall x y, - (0 < x)%R -> (0 < y)%R -> + (0 < y)%R -> (ln_beta x < ln_beta y)%Z -> (x < y)%R. Proof. -intros x y Px Py. +intros x y Py. +case (Rle_or_lt x 0); intros Px. +intros H. +now apply Rle_lt_trans with 0%R. destruct (ln_beta x) as (ex, Hex). destruct (ln_beta y) as (ey, Hey). simpl. @@ -2096,7 +2099,7 @@ assert (Hbeta : (2 <= r)%Z). { destruct r as (beta_val,beta_prop). now apply Zle_bool_imp_le. } intros x y Px Py Hln. -assert (Oxy : (y < x)%R); [now apply ln_beta_lt_pos; [| |omega]|]. +assert (Oxy : (y < x)%R); [apply ln_beta_lt_pos;[assumption|omega]|]. destruct (ln_beta x) as (ex,Hex). destruct (ln_beta y) as (ey,Hey). simpl in Hln |- *. diff --git a/src/Prop/Double_rounding.v b/src/Prop/Double_rounding.v index f8ca3d2..60de0f0 100644 --- a/src/Prop/Double_rounding.v +++ b/src/Prop/Double_rounding.v @@ -783,7 +783,7 @@ Lemma ln_beta_minus_disj : \/ (ln_beta (x - y) = (ln_beta x - 1)%Z :> Z)). Proof. intros x y Px Py Hln. -assert (Hxy : y < x); [now apply (ln_beta_lt_pos beta); [| |omega]|]. +assert (Hxy : y < x); [now apply (ln_beta_lt_pos beta); [ |omega]|]. generalize (ln_beta_minus beta x y Py Hxy); intro Hln2. generalize (ln_beta_minus_lb beta x y Px Py Hln); intro Hln3. omega. diff --git a/src/Prop/Plus_error.v b/src/Prop/Plus_error.v index 18b116e..ffb477f 100644 --- a/src/Prop/Plus_error.v +++ b/src/Prop/Plus_error.v @@ -262,7 +262,7 @@ Qed. End Fprop_plus_FLT. -(* + Section Fprop_plus_multi. Variable beta : radix. @@ -278,7 +278,7 @@ Context { valid_rnd : Valid_rnd rnd }. Notation format := (generic_format beta fexp). Notation cexp := (cexp beta fexp). -Lemma toto: forall x e, format x -> (e <= cexp x)%Z -> +Lemma ex_shift: forall x e, format x -> (e <= cexp x)%Z -> exists m, (x = Z2R m*bpow e)%R. Proof with auto with typeclass_instances. intros x e Fx He. @@ -291,24 +291,9 @@ rewrite Z2R_Zpower. rewrite <- bpow_plus; f_equal; ring. Qed. -(*Lemma Fprop_plus_mutiple_aux: - forall x y, format x -> format y -> - (0 < x)%R -> (y < 0)%R -> - exists m', - (round beta fexp rnd (x+y) = Z2R m' * ulp beta fexp (x/Z2R beta))%R. -Proof with auto with typeclass_instances. - -ln_beta_minus_lb -*) - -Lemma Fprop_plus_mutiple: - forall x y, format x -> format y -> (x <> 0)%R -> - exists m, - (round beta fexp rnd (x+y) = Z2R m * ulp beta fexp (x/Z2R beta))%R. +Lemma ln_beta_minus1: + forall z, (z<>0)%R -> (ln_beta beta z -1 = ln_beta beta (z / Z2R beta))%Z. Proof with auto with typeclass_instances. -intros x y Fx Fy Zx. -(* *) -assert (H: forall z, (z<>0)%R -> (ln_beta beta z -1 = ln_beta beta (z / Z2R beta))%Z). intros z Hz; apply sym_eq, ln_beta_unique. destruct (ln_beta beta z) as (e,He); simpl. replace (z / Z2R beta)%R with (z*bpow (-1))%R. @@ -328,13 +313,20 @@ apply bpow_le; omega. apply Rle_ge, bpow_ge_0. simpl; unfold Rdiv; f_equal; f_equal; f_equal. unfold Z.pow_pos; simpl; ring. -(* *) +Qed. + +Lemma rnd_plus_mutiple: + forall x y, format x -> format y -> (x <> 0)%R -> + exists m, + (round beta fexp rnd (x+y) = Z2R m * ulp beta fexp (x/Z2R beta))%R. +Proof with auto with typeclass_instances. +intros x y Fx Fy Zx. case (Zle_or_lt (ln_beta beta (x/Z2R beta)) (ln_beta beta y)); intros H1. pose (e:=cexp (x / Z2R beta)). -destruct (toto x e) as (nx, Hnx); try exact Fx. +destruct (ex_shift x e) as (nx, Hnx); try exact Fx. apply monotone_exp. -rewrite <- (H x Zx); omega. -destruct (toto y e) as (ny, Hny); try assumption. +rewrite <- (ln_beta_minus1 x Zx); omega. +destruct (ex_shift y e) as (ny, Hny); try assumption. apply monotone_exp... destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn). exists n. @@ -348,19 +340,57 @@ apply Rinv_neq_0_compat. apply Rgt_not_eq. apply radix_pos. (* *) -destruct (toto (round beta fexp rnd (x + y)) (cexp (x/Z2R beta))) as (n,Hn). +destruct (ex_shift (round beta fexp rnd (x + y)) (cexp (x/Z2R beta))) as (n,Hn). apply generic_format_round... apply Zle_trans with (cexp (x+y)). apply monotone_exp. -rewrite <- H; try assumption. +rewrite <- ln_beta_minus1; try assumption. rewrite <- (ln_beta_abs beta (x+y)). +(* . *) assert (U:(Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y)=Rabs x - Rabs y)%R). - - - -admit. - - +assert (V: forall x y, (Rabs y <= Rabs x)%R -> + (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y)=Rabs x - Rabs y)%R). +clear; intros x y. +case (Rle_or_lt 0 y); intros Hy. +case Hy; intros Hy'. +case (Rle_or_lt 0 x); intros Hx. +intros _; rewrite (Rabs_right y); [idtac|now apply Rle_ge]. +rewrite (Rabs_right x); [idtac|now apply Rle_ge]. +left; apply Rabs_right. +apply Rle_ge; apply Rplus_le_le_0_compat; assumption. +rewrite (Rabs_right y); [idtac|now apply Rle_ge]. +rewrite (Rabs_left x); [idtac|assumption]. +intros H; right; split. +now apply Rgt_not_eq. +rewrite Rabs_left1. +ring. +apply Rplus_le_reg_l with (-x)%R; ring_simplify; assumption. +intros _; left. +now rewrite <- Hy', Rabs_R0, 2!Rplus_0_r. +case (Rle_or_lt 0 x); intros Hx. +rewrite (Rabs_left y); [idtac|assumption]. +rewrite (Rabs_right x); [idtac|now apply Rle_ge]. +intros H; right; split. +apply sym_not_eq; now apply Rgt_not_eq. +rewrite Rabs_right. +ring. +apply Rle_ge; apply Rplus_le_reg_l with (-y)%R; ring_simplify; assumption. +intros _; left. +rewrite (Rabs_left y); [idtac|assumption]. +rewrite (Rabs_left x); [idtac|assumption]. +rewrite Rabs_left1. +ring. +rewrite <- (Ropp_involutive (x+y)), <- Ropp_0. +apply Ropp_le_contravar; rewrite Ropp_plus_distr. +apply Rplus_le_le_0_compat. +rewrite <- Ropp_0; apply Ropp_le_contravar; now left. +rewrite <- Ropp_0; apply Ropp_le_contravar; now left. +apply V; left. +apply ln_beta_lt_pos with beta. +now apply Rabs_pos_lt. +rewrite <- ln_beta_minus1 in H1; try assumption. +rewrite 2!ln_beta_abs; omega. +(* . *) destruct U as [U|U]. rewrite U; apply Zle_trans with (ln_beta beta x);[omega|idtac]. rewrite <- ln_beta_abs. @@ -375,13 +405,13 @@ now apply Rabs_pos_lt. now apply Rabs_pos_lt. rewrite 2!ln_beta_abs. assert (ln_beta beta y < ln_beta beta x -1)%Z;[idtac|omega]. -now rewrite (H x Zx). -apply canonic_exp_round_ge... +now rewrite (ln_beta_minus1 x Zx). +apply cexp_round_ge... intros K. absurd (x+y=0)%R. intros K'. contradict H1; apply Zle_not_lt. -rewrite <- (H x Zx). +rewrite <- (ln_beta_minus1 x Zx). replace y with (-x)%R. rewrite ln_beta_opp; omega. apply Rplus_eq_reg_l with x; rewrite K'; ring. @@ -393,20 +423,129 @@ apply Rmult_integral_contrapositive_currified; try assumption. apply Rinv_neq_0_compat. apply Rgt_not_eq. apply radix_pos. -Admitted. +Qed. + +Lemma rnd_0_or_ge: Exp_not_FTZ fexp -> forall x y, format x -> format y -> + (round beta fexp rnd (x+y) = 0)%R \/ + (ulp beta fexp (x/Z2R beta) <= Rabs (round beta fexp rnd (x+y)))%R. +Proof with auto with typeclass_instances. +intros exp_not_FTZ x y Fx Fy. +case (Req_dec x 0); intros Zx. +(* *) +rewrite Zx, Rplus_0_l. +rewrite round_generic... +unfold Rdiv; rewrite Rmult_0_l. +rewrite Fy at 2. +unfold F2R; simpl; rewrite Rabs_mult. +rewrite (Rabs_right (bpow _)). +2: apply Rle_ge, bpow_ge_0. +case (Z.eq_dec (Ztrunc (scaled_mantissa beta fexp y)) 0); intros Hm. +left. +rewrite Fy, Hm; unfold F2R; simpl; ring. +right. +apply Rle_trans with (1*bpow (cexp y))%R. +rewrite Rmult_1_l. +rewrite <- ulp_neq_0. +apply ulp_ge_ulp_0... +intros K; apply Hm. +rewrite K, scaled_mantissa_0. +replace 0%R with (Z2R 0) by reflexivity. +apply Ztrunc_Z2R. +apply Rmult_le_compat_r. +apply bpow_ge_0. +rewrite <- Z2R_abs. +replace 1%R with (Z2R 1) by reflexivity. +apply Z2R_le. +assert (0 < Z.abs (Ztrunc (scaled_mantissa beta fexp y)))%Z;[|omega]. +now apply Z.abs_pos. +(* *) +destruct (rnd_plus_mutiple x y Fx Fy Zx) as (m,Hm). +case (Z.eq_dec m 0); intros Zm. +left. +rewrite Hm, Zm; simpl; ring. +right. +rewrite Hm, Rabs_mult. +rewrite (Rabs_right (ulp _ _ _)). +2: apply Rle_ge, ulp_ge_0. +apply Rle_trans with (1*ulp beta fexp (x/Z2R beta))%R. +right; ring. +apply Rmult_le_compat_r. +apply ulp_ge_0. +rewrite <- Z2R_abs. +replace 1%R with (Z2R 1) by reflexivity. +apply Z2R_le. +assert (0 < Z.abs m)%Z;[|omega]. +now apply Z.abs_pos. +Qed. -(* +End Fprop_plus_multi. +Section Fprop_plus_multii. +Variable beta : radix. +Notation bpow e := (bpow beta e). -x oplus y est un multiple de ulp (x / beta) +Variable rnd : R -> Z. +Context { valid_rnd : Valid_rnd rnd }. +Variable emin prec : Z. +Context { prec_gt_0_ : Prec_gt_0 prec }. -==> +Lemma rnd_0_or_ge_FLT: forall x y e, + generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y -> + (bpow e <= Rabs x)%R -> + (round beta (FLT_exp emin prec) rnd (x+y) = 0)%R \/ + (bpow (e - prec) <= Rabs (round beta (FLT_exp emin prec) rnd (x+y)))%R. +Proof with auto with typeclass_instances. +intros x y e Fx Fy He. +assert (Zx:(x <> 0)%R). +intros K; contradict He. +apply Rlt_not_le; rewrite K, Rabs_R0. +apply bpow_gt_0. +case rnd_0_or_ge with beta (FLT_exp emin prec) rnd x y... +intros H; right. +apply Rle_trans with (2:=H). +rewrite ulp_neq_0. +unfold cexp. +rewrite <- ln_beta_minus1; try assumption. +unfold FLT_exp; apply bpow_le. +apply Zle_trans with (2:=Z.le_max_l _ _). +destruct (ln_beta beta x) as (n,Hn); simpl. +assert (e < n)%Z; try omega. +apply lt_bpow with beta. +apply Rle_lt_trans with (1:=He). +now apply Hn. +apply Rmult_integral_contrapositive_currified; try assumption. +apply Rinv_neq_0_compat. +apply Rgt_not_eq. +apply radix_pos. +Qed. -x oplus y = 0 ou >= /beta * ulp x - -==> -|x| >= bpow e -> x oplus y = 0 ou >= bpow (e-p) +Lemma rnd_0_or_ge_FLX: forall x y e, + generic_format beta (FLX_exp prec) x -> generic_format beta (FLX_exp prec) y -> + (bpow e <= Rabs x)%R -> + (round beta (FLX_exp prec) rnd (x+y) = 0)%R \/ + (bpow (e - prec) <= Rabs (round beta (FLX_exp prec) rnd (x+y)))%R. +Proof with auto with typeclass_instances. +intros x y e Fx Fy He. +assert (Zx:(x <> 0)%R). +intros K; contradict He. +apply Rlt_not_le; rewrite K, Rabs_R0. +apply bpow_gt_0. +case rnd_0_or_ge with beta (FLX_exp prec) rnd x y... +intros H; right. +apply Rle_trans with (2:=H). +rewrite ulp_neq_0. +unfold cexp. +rewrite <- ln_beta_minus1; try assumption. +unfold FLX_exp; apply bpow_le. +destruct (ln_beta beta x) as (n,Hn); simpl. +assert (e < n)%Z; try omega. +apply lt_bpow with beta. +apply Rle_lt_trans with (1:=He). +now apply Hn. +apply Rmult_integral_contrapositive_currified; try assumption. +apply Rinv_neq_0_compat. +apply Rgt_not_eq. +apply radix_pos. +Qed. -*) -End Fprop_plus_multi. -*) +End Fprop_plus_multii. diff --git a/src/Translate/Missing_theos.v b/src/Translate/Missing_theos.v index 8cc3c39..e2a6758 100644 --- a/src/Translate/Missing_theos.v +++ b/src/Translate/Missing_theos.v @@ -963,9 +963,9 @@ Let r3 := (gamma+alpha2) -r2. (** Non-underflow hypotheses *) Hypothesis Und1: a * x = 0 \/ bpow radix2 (emin + 2 * prec - 1) <= Rabs (a * x). -Hypothesis Und2: alpha1 = 0 \/ bpow radix2 (emin + prec) <= Rabs alpha1. +(*Hypothesis Und2: alpha1 = 0 \/ bpow radix2 (emin + prec) <= Rabs alpha1.*) -Hypothesis Und4: beta1 = 0 \/ bpow radix2 (emin + prec+1) <= Rabs beta1. +(*Hypothesis Und4: beta1 = 0 \/ bpow radix2 (emin + prec+1) <= Rabs beta1.*) Hypothesis Und5: r1 = 0 \/ bpow radix2 (emin + prec-1) <= Rabs r1. @@ -988,7 +988,33 @@ apply Rle_trans with (2:=H). apply bpow_le; omega. Qed. +Lemma Und4: beta1 = 0 \/ bpow radix2 (emin + prec+1) <= Rabs beta1. +Proof with auto with typeclass_instances. +unfold beta1. +replace (emin+prec+1)%Z with ((emin+2*prec+1)-prec)%Z by ring. +apply rnd_0_or_ge_FLT... +apply generic_format_round... +apply generic_format_round... +apply Und3'. +TOTO. + +replace (u2) with (-(u1-(a*x))) by (unfold u2; ring). +apply generic_format_opp. +apply mult_error_FLT... + + +Lemma Und2: alpha1 = 0 \/ bpow radix2 (emin + prec) <= Rabs alpha1. +Proof with auto with typeclass_instances. +unfold alpha1. +replace (emin+prec)%Z with ((emin+2*prec)-prec)%Z by ring. +rewrite Rplus_comm. +apply rnd_0_or_ge_FLT... +replace (u2) with (-(u1-(a*x))) by (unfold u2; ring). +apply generic_format_opp. +apply mult_error_FLT... + +Hypothesis Und2: alpha1 = 0 \/ bpow radix2 (emin + prec) <= Rabs alpha1. -- 2.22.0