Proved satisfies_any_imp_NA.

src/Flocq_Raux.v

 Require Export Reals.
 Require Export ZArith.
 
+Lemma Rabs_right1 :
+  forall x, (0 <= x)%R -> Rabs x = x.
+Proof.
+intros.
+apply Rabs_right.
+now apply Rle_ge.
+Qed.
+
+Lemma Rle_0_minus :
+  forall x y, (x <= y)%R -> (0 <= y - x)%R.
+Proof.
+intros.
+apply Rge_le.
+apply Rge_minus.
+now apply Rle_ge.
+Qed.
+
 Section Z2R.
 
 Fixpoint P2R (p : positive) :=

src/Flocq_defs.v

@@ -18,18 +18,17 @@ Definition F2R {beta : radix} (f : float beta) :=
 (*    The domain will be used to formalize Overflow, flush to zero...      *)
 
 
-Definition MonotoneP (D: R -> Prop) (rnd : R -> R) :=
-  forall x y: R, D x -> D y ->
-     (x <= y)%R -> (rnd x <= rnd y)%R.
+Definition MonotoneP (rnd : R -> R) :=
+  forall x y : R,
+  (x <= y)%R -> (rnd x <= rnd y)%R.
 
 
-Definition InvolutiveP (D F : R -> Prop) (rnd : R -> R) :=
-    (forall x : R, D x -> F (rnd x))
-        /\ (forall x : R, D x -> F x -> rnd x = x). 
-
-Definition Rounding_for_Format (D:R->Prop) (F : R -> Prop) (rnd : R->R) :=
-   MonotoneP D rnd /\ InvolutiveP  D F rnd.
+Definition InvolutiveP (F : R -> Prop) (rnd : R -> R) :=
+    (forall x : R, F (rnd x))
+        /\ (forall x : R, F x -> rnd x = x). 
 
+Definition Rounding_for_Format (F : R -> Prop) (rnd : R -> R) :=
+   MonotoneP rnd /\ InvolutiveP F rnd.
 
 (* unbounded floating-point format *)
 Definition FLX_format (prec : Z) (x : R) :=
@@ -46,16 +45,14 @@ Definition FIX_format (emin : Z) (x : R) :=
   exists f : float beta,
   x = F2R f /\ (Fexp f = emin)%Z.
 
-Definition R_whole := fun _:R => True.
-
 Definition FLX_RoundingModeP (prec : Z) (rnd : R -> R):=
-  Rounding_for_Format R_whole (FLX_format prec) rnd.
+  Rounding_for_Format (FLX_format prec) rnd.
 
 Definition FLT_RoundingModeP (emin prec : Z) (rnd : R -> R):=
-  Rounding_for_Format R_whole (FLT_format emin prec) rnd.
+  Rounding_for_Format (FLT_format emin prec) rnd.
 
 Definition FIX_RoundingModeP (emin : Z) (rnd : R -> R):=
-  Rounding_for_Format R_whole (FIX_format emin) rnd.
+  Rounding_for_Format (FIX_format emin) rnd.
 
 End Def.
 
@@ -66,82 +63,72 @@ Definition Rnd_DN_pt (F : R -> Prop) (x f : R) :=
   F f /\ (f <= x)%R /\
   forall g : R, F g -> (g <= x)%R -> (g <= f)%R.
 
-Definition Rnd_DN (D : R -> Prop) (F : R -> Prop) (rnd : R -> R) :=
-  forall x : R, D x ->
-  D (rnd x) /\ Rnd_DN_pt F x (rnd x).
+Definition Rnd_DN (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_DN_pt F x (rnd x).
 
 (* property of being a rounding toward +inf *)
 Definition Rnd_UP_pt (F : R -> Prop) (x f : R) :=
   F f /\ (x <= f)%R /\
   forall g : R, F g -> (x <= g)%R -> (f <= g)%R.
 
-Definition Rnd_UP (D : R -> Prop) (F : R -> Prop) (rnd : R -> R) :=
-  forall x : R, D x ->
-  D (rnd x) /\ Rnd_UP_pt F x (rnd x).
+Definition Rnd_UP (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_UP_pt F x (rnd x).
 
 (* property of being a rounding toward zero *)
-Definition Rnd_ZR (D:R->Prop) (F : R -> Prop) (rnd : R->R) :=
-     Rnd_DN (fun x => D x /\ (0 <= x)%R) F rnd
-  /\ Rnd_UP (fun x => D x /\ (x <= 0)%R) F rnd.
-      
-
-Theorem toto: forall (F : R -> Prop) (rnd: R-> R), 
-   Rnd_ZR R_whole F rnd ->
-   forall (x:R),  (Rabs (rnd x) <= Rabs x)%R.
-intros F rnd (H1,H2).
+Definition Rnd_ZR_pt (F : R -> Prop) (x f : R) :=
+  ( (0 <= x)%R -> Rnd_DN_pt F x f ) /\
+  ( (x <= 0)%R -> Rnd_UP_pt F x f ).
+
+Definition Rnd_ZR (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_ZR_pt F x (rnd x).
+
+Theorem toto :
+  forall (F : R -> Prop) (rnd: R-> R), 
+  Rnd_ZR F rnd ->
+  forall x : R,  (Rabs (rnd x) <= Rabs x)%R.
+Proof.
+intros F rnd H x.
 assert (F 0%R).
 replace 0%R with (rnd 0%R).
-eapply H1 ; repeat split ; apply Rle_refl.
+eapply H.
+apply Rle_refl.
+destruct (H 0%R) as (H1, H2).
 apply Rle_antisym.
-destruct (H1 0%R); repeat split ; auto with real.
-apply H0.
-destruct (H2 0%R); repeat split ; auto with real.
-apply H0.
-intros x.
+apply H1.
+apply Rle_refl.
+apply H2.
+apply Rle_refl.
+(* . *)
 destruct (Rle_or_lt 0 x).
 (* positive *)
 rewrite Rabs_right.
 rewrite Rabs_right; auto with real.
-eapply H1.
-now split.
+now apply (proj1 (H x)).
 apply Rle_ge.
-eapply H1.
-now split.
-exact H.
-exact H0.
+now apply (proj1 (H x)).
 (* negative *)
 rewrite Rabs_left1.
 rewrite Rabs_left1 ; auto with real.
 apply Ropp_le_contravar.
-eapply H2.
-repeat split.
-auto with real.
-eapply H2.
-repeat split.
-auto with real.
-exact H.
+apply (proj2 (H x)).
 auto with real.
+apply (proj2 (H x)) ; auto with real.
 Qed.
 
-
-
-
-
 (* property of being a rounding to nearest *)
 Definition Rnd_N_pt (F : R -> Prop) (x f : R) :=
   F f /\
   forall g : R, F g -> (Rabs (f - x) <= Rabs (g - x))%R.
 
-Definition Rnd_N (D : R -> Prop) (F : R -> Prop) (rnd : R -> R) :=
-  forall x : R, D x ->  
-  Rnd_N_pt F x (rnd x).
-
-Definition Rnd_NA (D:R->Prop) (F : R -> Prop) (rnd : R->R) :=
-   Rnd_N D F rnd /\
-    forall (x y:R), D x -> F y ->
-      (forall g : R, F g -> (Rabs (y-x) <= Rabs (g-x))%R)
-          -> (Rabs y <= Rabs (rnd x))%R.
+Definition Rnd_N (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_N_pt F x (rnd x).
 
+Definition Rnd_NA_pt (F : R -> Prop) (x f : R) :=
+  Rnd_N_pt F x f /\
+  forall f2 : R, Rnd_N_pt F x f2 ->
+  (Rabs f2 <= Rabs f)%R.
 
+Definition Rnd_NA (F : R -> Prop) (rnd : R -> R) :=
+  forall x : R, Rnd_NA_pt F x (rnd x).
 
 End RND.

src/Flocq_rnd_ex.v

@@ -22,15 +22,13 @@ now eapply H2.
 Qed.
 
 Theorem Rnd_DN_unicity :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,
   forall rnd1 rnd2 : R -> R,
-  Rnd_DN D F rnd1 -> Rnd_DN D F rnd2 ->
-  forall x, D x -> rnd1 x = rnd2 x.
+  Rnd_DN F rnd1 -> Rnd_DN F rnd2 ->
+  forall x, rnd1 x = rnd2 x.
 Proof.
-intros D F rnd1 rnd2 H1 H2 x Hx.
-eapply Rnd_DN_pt_unicity.
-now eapply H1.
-now eapply H2.
+intros F rnd1 rnd2 H1 H2 x.
+now eapply Rnd_DN_pt_unicity.
 Qed.
 
 Theorem Rnd_UP_pt_unicity :
@@ -50,309 +48,379 @@ now eapply H2.
 Qed.
 
 Theorem Rnd_UP_unicity :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,
   forall rnd1 rnd2 : R -> R,
-  Rnd_UP D F rnd1 -> Rnd_UP D F rnd2 ->
-  forall x, D x -> rnd1 x = rnd2 x.
+  Rnd_UP F rnd1 -> Rnd_UP F rnd2 ->
+  forall x, rnd1 x = rnd2 x.
 Proof.
-intros D F rnd1 rnd2 H1 H2 x Hx.
-eapply Rnd_UP_pt_unicity.
-now eapply H1.
-now eapply H2.
+intros F rnd1 rnd2 H1 H2 x.
+now eapply Rnd_UP_pt_unicity.
 Qed.
 
 Theorem Rnd_DN_UP_pt_sym :
   forall F : R -> Prop,
   ( forall x, F x -> F (- x) ) ->
-  forall x f1 f2 : R,
-  Rnd_DN_pt F (-x) f1 -> Rnd_UP_pt F x f2 ->
-  f1 = - f2.
+  forall x f : R,
+  Rnd_DN_pt F (-x) (-f) -> Rnd_UP_pt F x f.
 Proof.
-intros F HF x f1 f2 H1 H2.
-eapply Rnd_DN_pt_unicity.
-apply H1.
+intros F HF x f H.
+rewrite <- (Ropp_involutive f).
 repeat split.
 apply HF.
-apply H2.
-apply Ropp_le_contravar.
-apply H2.
+apply H.
+apply Ropp_le_cancel.
+rewrite Ropp_involutive.
+apply H.
 intros.
 apply Ropp_le_cancel.
 rewrite Ropp_involutive.
-apply H2.
+apply H.
 now apply HF.
-apply Ropp_le_cancel.
-now rewrite Ropp_involutive.
+now apply Ropp_le_contravar.
 Qed.
 
 Theorem Rnd_DN_UP_sym :
-  forall D F : R -> Prop,
-  ( forall x, D x -> D (- x) ) ->
+  forall F : R -> Prop,
   ( forall x, F x -> F (- x) ) ->
   forall rnd1 rnd2 : R -> R,
-  Rnd_DN D F rnd1 -> Rnd_UP D F rnd2 ->
-  forall x, D x -> rnd1 (- x) = - rnd2 x.
+  Rnd_DN F rnd1 -> Rnd_UP F rnd2 ->
+  forall x, rnd1 (- x) = - rnd2 x.
 Proof.
-intros D F HD HF rnd1 rnd2 H1 H2 x Hx.
-eapply Rnd_DN_UP_pt_sym.
+intros F HF rnd1 rnd2 H1 H2 x.
+rewrite <- (Ropp_involutive (rnd1 (-x))).
+apply f_equal.
+apply (Rnd_UP_unicity F (fun x => - rnd1 (-x))) ; trivial.
+intros y.
+apply Rnd_DN_UP_pt_sym.
 apply HF.
-eapply H1.
-now apply HD.
-now eapply H2.
+rewrite Ropp_involutive.
+apply H1.
 Qed.
 
 Theorem Rnd_DN_involutive :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,
   forall rnd : R -> R,
-  Rnd_DN D F rnd ->
-  InvolutiveP D F rnd.
+  Rnd_DN F rnd ->
+  InvolutiveP F rnd.
 Proof.
-intros D F rnd Hrnd.
+intros F rnd Hrnd.
 split.
-intros x Hx.
+intros x.
 now eapply Hrnd. 
-intros x Hx Hxx.
-destruct (Hrnd x Hx) as (H1,(H2,(H3,H4))).
+intros x Hx.
+destruct (Hrnd x) as (H1,(H2,H3)).
 apply Rle_antisym; trivial.
-apply H4; auto with real.
+apply H3; auto with real.
 Qed.
 
 Theorem Rnd_DN_monotone :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,
   forall rnd : R -> R,
-  Rnd_DN D F rnd ->
-  MonotoneP D rnd.
+  Rnd_DN F rnd ->
+  MonotoneP rnd.
 Proof.
-intros D F rnd Hrnd x y Hx Hy Hxy.
+intros F rnd Hrnd x y Hxy.
 destruct (Rle_or_lt x (rnd y)).
 apply Rle_trans with (2 := H).
 now eapply Hrnd.
 eapply Hrnd.
-apply Hy.
 now eapply Hrnd.
 apply Rle_trans with (2 := Hxy).
 now eapply Hrnd.
 Qed.
 
 Theorem Rnd_UP_monotone :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,
   forall rnd : R -> R,
-  Rnd_UP D F rnd ->
-  MonotoneP D rnd.
+  Rnd_UP F rnd ->
+  MonotoneP rnd.
 Proof.
-intros D F rnd Hrnd x y Hx Hy Hxy.
+intros F rnd Hrnd x y Hxy.
 destruct (Rle_or_lt (rnd x) y).
 apply Rle_trans with (1 := H).
 now eapply Hrnd.
 eapply Hrnd.
-apply Hx.
 now eapply Hrnd.
 apply Rle_trans with (1 := Hxy).
 now eapply Hrnd.
 Qed.
 
 Theorem Rnd_UP_involutive :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,
   forall rnd : R -> R,
-  Rnd_UP D F rnd ->
-  InvolutiveP D F rnd.
+  Rnd_UP F rnd ->
+  InvolutiveP F rnd.
 Proof.
-intros D F rnd Hrnd.
+intros F rnd Hrnd.
 split.
-intros x Hx.
+intros x.
 now eapply Hrnd. 
-intros x Hx Hxx.
-destruct (Hrnd x Hx) as (H1,(H2,(H3,H4))).
+intros x Hx.
+destruct (Hrnd x) as (H1,(H2,H3)).
 apply Rle_antisym; trivial.
-apply H4; auto with real.
+apply H3; auto with real.
 Qed.
 
 Theorem Rnd_DN_pt_le_rnd :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,
   forall rnd : R -> R,
-  Rounding_for_Format D F rnd -> 
+  Rounding_for_Format F rnd -> 
   forall x fd : R,
-  D x ->
-  D fd ->
   Rnd_DN_pt F x fd ->
   fd <= rnd x.
 Proof.
-intros D F rnd (Hr1,(Hr2,Hr3)) x fd Hx Hd1 Hd2.
+intros F rnd (Hr1,(Hr2,Hr3)) x fd Hd.
 replace fd with (rnd fd).
-apply Hr1 ; trivial.
-apply Hd2.
+apply Hr1.
+apply Hd.
 apply Hr3.
-exact Hd1.
-apply Hd2.
+apply Hd.
 Qed.
 
 Theorem Rnd_DN_le_rnd :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,
   forall rndd rnd: R -> R,
-  Rnd_DN D F rndd -> 
-  Rounding_for_Format D F rnd -> 
-  forall x, D x -> rndd x <= rnd x.
+  Rnd_DN F rndd -> 
+  Rounding_for_Format F rnd -> 
+  forall x, rndd x <= rnd x.
 Proof.
-intros D F rndd rnd Hd Hr x Hx.
+intros F rndd rnd Hd Hr x.
 eapply Rnd_DN_pt_le_rnd.
 apply Hr.
-apply Hx.
-now eapply Hd.
-now eapply Hd.
+apply Hd.
+Qed.
 
-intros D F rndd rnd Hd (Hr1,(Hr2,Hr3)) x Hx.
-destruct (Hd x Hx) as (H1,(H2,(H3,H4))).
-replace (rndd x) with (rnd (rndd x)).
-now apply Hr1.
-now apply Hr3.
+Theorem Rnd_UP_pt_ge_rnd :
+  forall F : R -> Prop,
+  forall rnd : R -> R,
+  Rounding_for_Format F rnd -> 
+  forall x fu : R,
+  Rnd_UP_pt F x fu ->
+  rnd x <= fu.
+Proof.
+intros F rnd (Hr1,(Hr2,Hr3)) x fu Hu.
+replace fu with (rnd fu).
+apply Hr1.
+apply Hu.
+apply Hr3.
+apply Hu.
 Qed.
 
 Theorem Rnd_UP_ge_rnd :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,
   forall rndu rnd: R -> R,
-  Rnd_UP D F rndu ->
-  Rounding_for_Format D F rnd -> 
-  forall x, D x -> rnd x <= rndu x.
-Proof.
-intros D F rndu rnd Hu (Hr1,(Hr2,Hr3)) x Hx.
-destruct (Hu x Hx) as (H1,(H2,(H3,H4))).
-replace (rndu x) with (rnd (rndu x)).
-now apply Hr1.
-now apply Hr3.
-Qed.
-
-Theorem Rnd_UP_or_DN: 
-  forall D F : R -> Prop,
-  forall rndd rndu rnd: R -> R,
-  Rnd_DN D F rndd -> Rnd_UP D F rndu ->
-  Rounding_for_Format D F rnd ->
-  forall x, D x -> rnd x = rndd x \/ rnd x = rndu x.
-Proof.
-intros D F rndd rndu rnd Hd Hu Hr x Hx.
-destruct (Rnd_DN_le_rnd _ _ _ _ Hd Hr x Hx) as [Hdlt|H].
+  Rnd_UP F rndu ->
+  Rounding_for_Format F rnd -> 
+  forall x, rnd x <= rndu x.
+Proof.
+intros F rndu rnd Hu Hr x.
+eapply Rnd_UP_pt_ge_rnd.
+apply Hr.
+apply Hu.
+Qed.
+
+Lemma Only_DN_or_UP :
+  forall F : R -> Prop,
+  forall x fd fu f : R,
+  Rnd_DN_pt F x fd -> Rnd_UP_pt F x fu ->
+  F f -> (fd <= f <= fu)%R ->
+  f = fd \/ f = fu.
+Proof.
+intros F x fd fu f Hd Hu Hf ([Hdf|Hdf], Hfu).
 2 : now left.
-destruct (Rnd_UP_ge_rnd _ _ _ _ Hu Hr x Hx) as [Hugt|H].
+destruct Hfu.
 2 : now right.
-destruct Hr as (Hr1,(Hr2,Hr3)).
-destruct (Rle_or_lt x (rnd x)).
-elim Rlt_not_le with (1 := Hugt).
-eapply Hu ; trivial.
-now apply Hr2.
-elim Rlt_not_le with (1 := Hdlt).
-eapply Hd ; auto with real.
+destruct (Rle_or_lt x f).
+elim Rlt_not_le with (1 := H).
+now apply Hu.
+elim Rlt_not_le with (1 := Hdf).
+apply Hd ; auto with real.
+Qed.
+
+Theorem Rnd_DN_or_UP_pt :
+  forall F : R -> Prop,
+  forall rnd : R -> R,
+  Rounding_for_Format F rnd ->
+  forall x fd fu : R,
+  Rnd_DN_pt F x fd -> Rnd_UP_pt F x fu ->
+  rnd x = fd \/ rnd x = fu.
+Proof.
+intros F rnd Hr x fd fu Hd Hu.
+eapply Only_DN_or_UP ; try eassumption.
+apply Hr.
+split.
+eapply Rnd_DN_pt_le_rnd ; eassumption.
+eapply Rnd_UP_pt_ge_rnd ; eassumption.
+Qed.
+
+Theorem Rnd_DN_or_UP :
+  forall F : R -> Prop,
+  forall rndd rndu rnd : R -> R,
+  Rnd_DN F rndd -> Rnd_UP F rndu ->
+  Rounding_for_Format F rnd ->
+  forall x, rnd x = rndd x \/ rnd x = rndu x.
+Proof.
+intros F rndd rndu rnd Hd Hu Hr x.
+eapply Rnd_DN_or_UP_pt.
+apply Hr.
+apply Hd.
+apply Hu.
 Qed.
 
+Theorem Rnd_N_pt_DN_or_UP :
+  forall F : R -> Prop,
+  forall x fd fu f : R,
+  Rnd_DN_pt F x fd -> Rnd_UP_pt F x fu ->
+  Rnd_N_pt F x f ->
+  f = fd \/ f = fu.
+Proof.
+intros F x fd fu f Hd Hu Hf.
+eapply Only_DN_or_UP ; try eassumption.
+apply Hf.
+split.
+(* fd <= f *)
+destruct (Rle_or_lt x f).
+apply Rle_trans with (2 := H).
+apply Hd.
+assert (Hd' := proj2 Hf fd).
+apply Ropp_le_cancel.
+apply Rplus_le_reg_l with x.
+replace (x + -f) with (Rabs (f - x)).
+replace (x + -fd) with (Rabs (fd - x)).
+apply Hd'.
+apply Hd.
+rewrite Rabs_left1.
+ring.
+apply Rle_minus.
+apply Hd.
+rewrite Rabs_left.
+ring.
+now apply Rlt_minus.
+(* f <= fu *)
+destruct (Rle_or_lt x f).
+assert (Hu' := proj2 Hf fu).
+apply Rplus_le_reg_l with (-x).
+replace (-x + f) with (Rabs (f - x)).
+replace (-x + fu) with (Rabs (fu - x)).
+apply Hu'.
+apply Hu.
+rewrite Rabs_right1.
+ring.
+apply Rle_0_minus.
+apply Hu.
+rewrite Rabs_right1.
+ring.
+now apply Rle_0_minus.
+apply Rlt_le.
+apply Rlt_le_trans with (1 := H).
+apply Hu.
+Qed.
+
+(*
+Theorem Rnd_N_pt_monotone :
+  forall F : R -> Prop,
+  forall x y f g : R,
+  Rnd_N_pt F x f -> Rnd_N_pt F y g ->
+  x < y -> f <= g.
+Proof.
+intros F x y f g Hx Hy Hxy.
+*)
+
 Theorem Rnd_0 :
-  forall D F : R -> Prop,
+  forall F : R -> Prop,