Split properties.

src/Flocq_rnd_FIX.v

+Require Import Flocq_Raux.
+Require Import Flocq_defs.
+Require Import Flocq_rnd_ex.
+
+Section RND_FIX.
+
+Open Scope R_scope.
+
+(*
+Theorem exp_ln_powerRZ :
+ forall u v : Z, (0 < u)%Z -> exp (ln (IZR u) * (IZR v)) = powerRZ (IZR u) v.
+admit.
+Qed.
+
+(*
+Theorem exp_monotone : forall x y : R, (x <= y)%R -> (exp x <= exp y)%R.
+intros x y H; case H; intros H2.
+left; apply exp_increasing; auto.
+right; auto with real.
+Qed.*)
+
+
+Definition floor_int (r : R) :=(up r-1)%Z.
+
+
+Theorem floor_int_pos : forall r : R, (0 <= r)%R -> (0 <=  IZR (floor_int r))%R.
+Proof.
+intros r H1; unfold floor_int in |- *.
+generalize (archimed r); intros T; elim T; intros H3 H2; clear T.
+replace 0%R with (IZR 0); auto with real; apply IZR_le.
+assert (0 < up r)%Z; auto with zarith.
+apply lt_IZR; apply Rle_lt_trans with r; auto with real zarith.
+Qed.
+
+
+Theorem  floor_int_correct1 : forall r : R, (IZR (floor_int r) <= r)%R. 
+Proof.
+intros r; unfold  floor_int in |- *.
+generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
+apply Rplus_le_reg_l with (1 + - r)%R.
+ring_simplify (1 + - r + r)%R.
+apply Rle_trans with (2 := H2).
+unfold Zminus; rewrite plus_IZR; right; simpl in |- *; ring.
+Qed.
+
+Theorem floor_int_correct2 : forall r : R, (r < IZR (floor_int r+1))%R.
+intros r; unfold floor_int in |- *.
+generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
+ring_simplify (up r - 1 + 1)%Z; auto.
+Qed.
+
+Theorem floor_int_correct3 : forall r : R, (r - 1 < IZR (floor_int r))%R.
+intros r; unfold floor_int in |- *.
+generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
+unfold Rminus, Zminus; rewrite plus_IZR; simpl in |- *; auto with real. 
+Qed.
+*)
+
+Variable beta : radix.
+
+Notation bpow := (epow beta).
+
+Variable emin prec : Z.
+
+(*
+Definition RND_DN_pos_fn (r : R) :=
+  match Rle_dec (powerRZ (IZR radix) (prec-1+emin)) r with
+  | left _ =>
+      let e := floor_int (ln r / ln (IZR radix) + IZR (- prec+1)) in
+      Float radix (floor_int (r * powerRZ (IZR radix) (- e))) e
+  | right _ => Float radix (floor_int (r * powerRZ (IZR radix) (-emin))) emin
+  end.
+
+Variable radix_gt_0 : (0 < radix)%Z.
+
+Lemma FLT_format_satisfies_DN_aux:
+ forall x : R, (0 <= x)%R -> exists f : R, Rnd_DN (FLT_format radix emin prec) x f.
+Proof.
+intros; exists (F2R (RND_DN_pos_fn x)); split.
+exists (RND_DN_pos_fn x); split; auto; split.
+unfold RND_DN_pos_fn; case (Rle_dec (powerRZ (IZR radix) (prec-1+emin)) x); simpl; intros H1.
+rewrite Zabs_eq.
+2: apply le_IZR; apply floor_int_pos; apply Rmult_le_pos; auto.
+2: admit. (* cf apres *)
+apply lt_IZR.
+apply Rle_lt_trans with (1:=floor_int_correct1 _).
+rewrite <- exp_ln_powerRZ; auto.
+apply Rlt_le_trans with  (x *
+    (exp (-ln x) * exp (ln (IZR radix) * IZR (prec))))%R.
+apply Rmult_lt_compat_l; auto with real.
+apply Rlt_le_trans with (2:=H1); auto with real zarith.
+admit. (* cf apres *)
+rewrite <- exp_plus.
+apply exp_increasing.
+apply Rmult_lt_reg_l with (/ln (IZR radix))%R.
+admit.
+apply Rle_lt_trans with (IZR (- floor_int (ln x / ln (IZR radix) + IZR (- prec+1)))).
+right; field.
+admit.
+apply Rlt_le_trans with (-(ln x / ln (IZR radix) - IZR (prec)))%R.
+2: right; field.
+2: admit.
+rewrite Ropp_Ropp_IZR.
+apply Ropp_lt_contravar.
+apply Rle_lt_trans with (2:= floor_int_correct3 _).
+rewrite plus_IZR; rewrite Ropp_Ropp_IZR; simpl; right; ring.
+rewrite exp_Ropp; rewrite exp_ln; auto.
+2: admit.
+rewrite  exp_ln_powerRZ.
+admit.
+auto.
+rewrite Zabs_eq.
+2: apply le_IZR; apply floor_int_pos; apply Rmult_le_pos; auto.
+2: admit. (* cf apres *)
+apply lt_IZR.
+apply Rle_lt_trans with (1:=floor_int_correct1 _).
+apply Rlt_le_trans with (powerRZ (IZR radix) (prec - 1 + emin)* powerRZ (IZR radix) (- emin))%R.
+apply Rmult_lt_compat_r.
+admit.
+auto with real.
+rewrite <- powerRZ_add; auto with real.
+(* apply Rle_ powerRZ.*)
+admit.
+admit.
+unfold RND_DN_pos_fn; case (Rle_dec (powerRZ (IZR radix) (prec-1+emin)) x); 
+  simpl; auto with zarith; intros H1.
+assert (emin-1  < floor_int (ln x / ln (IZR radix) + IZR (- prec + 1)))%Z; auto with zarith.
+apply lt_IZR.
+apply Rle_lt_trans with (2:= floor_int_correct3 _).
+apply Rplus_le_reg_l with (IZR prec).
+apply Rmult_le_reg_l with (ln (IZR radix)).
+admit.
+apply Rle_trans with (ln x).
+exp
+ln
+
+
+rewrite <- exp_ln_powerRZ; auto.
+apply Rlt_le_trans with  (x *
+    (exp (-ln x) * exp (ln (IZR radix) * IZR (prec))))%R.
+apply Rmult_lt_compat_l; auto with real.
+apply Rlt_le_trans with (2:=H1); auto with real zarith.
+admit. (* cf apres *)
+rewrite <- exp_plus.
+apply exp_increasing.
+apply Rmult_lt_reg_l with (/ln (IZR radix))%R.
+admit.
+apply Rle_lt_trans with (IZR (- floor_int (ln x / ln (IZR radix) + IZR (- prec+1)))).
+right; field.
+admit.
+apply Rlt_le_trans with (-(ln x / ln (IZR radix) - IZR (prec)))%R.
+2: right; field.
+2: admit.
+rewrite Ropp_Ropp_IZR.
+apply Ropp_lt_contravar.
+apply Rle_lt_trans with (2:= floor_int_correct3 _).
+rewrite plus_IZR; rewrite Ropp_Ropp_IZR; simpl; right; ring.
+rewrite exp_Ropp; rewrite exp_ln; auto.
+2: admit.
+rewrite  exp_ln_powerRZ.
+admit.
+auto.
+
+
+
+      (ln (IZR radix) *
+       IZR (- (ln x / ln (IZR radix) + IZR (- Zpred prec))))
+
+
+apply Rle_lt_trans with (x *
+    powerRZ (IZR radix)
+      (- floor_int (ln x / ln (IZR radix) + IZR (- Zpred prec)))
+
+rewrite powerRZ_add; auto with real zarith.
+
+
+rewrite Zpower_powerRZ; rewrite <- Rabsolu_Zabs.
+
+
+
+unfold FLT_format.
+
+
+
+Theorem FLT_format_satisfies_DN : satisfies_DN (FLT_format radix emin prec).
+Proof.
+unfold satisfies_DN.
+intros.
+
+
+Theorem FLT_format_satisfies_DN_UP :
+  satisfies_DN_UP (FLT_format radix emin prec).
+Proof.
+intros.
+assert (Hdn: satisfies_DN (FLT_format radix emin prec)) by admit.
+apply satisfies_DN_imp_UP.
+intros x (f,(Hx,(Hm,He))).
+exists (Float radix (-(Fnum f))%Z (Fexp f)).
+repeat split.
+rewrite Hx.
+unfold F2R.
+simpl.
+rewrite Ropp_Ropp_IZR.
+now rewrite Ropp_mult_distr_l_reverse.
+simpl.
+now rewrite Zabs_Zopp.
+exact He.
+exact Hdn.
+Qed.
+
+Variable radix_gt_0 : (0 < radix)%Z.
+
+Lemma powerRZ_radix_ge_0 :
+  forall e : Z, (0 <= powerRZ (IZR radix) e)%R.
+Proof.
+intros.
+apply powerRZ_le.
+change R0 with (IZR 0).
+apply IZR_lt.
+exact radix_gt_0.
+Qed.
+
+Lemma powerRZ_radix_gt_0 :
+  forall e : Z, (0 < powerRZ (IZR radix) e)%R.
+Proof.
+intros.
+apply powerRZ_lt.
+change R0 with (IZR 0).
+apply IZR_lt.
+exact radix_gt_0.
+Qed.
+
+Lemma IZR_radix_neq_0 :
+  IZR radix <> R0.
+Proof.
+apply Rgt_not_eq.
+change R0 with (IZR 0).
+apply IZR_lt.
+exact radix_gt_0.
+Qed.
+*)
+
+Theorem FIX_format_satisfies_any :
+  satisfies_any (FIX_format beta emin).
+Proof.
+refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
+(* symmetric set *)
+exists (Float beta 0 emin).
+split.
+unfold F2R.
+now rewrite Rmult_0_l.
+apply refl_equal.
+intros x ((m,e),(H1,H2)).
+exists (Float beta (-m) emin).
+split.
+rewrite H1.
+unfold F2R.
+simpl.
+rewrite opp_Z2R, Ropp_mult_distr_l_reverse.
+now rewrite <- H2.
+apply refl_equal.
+(* rounding down *)
+exists (fun x => F2R (Float beta (up (x * bpow (Zopp emin)) - 1) emin)).
+intros x.
+set (m := up (x * bpow (Zopp emin))).
+set (f := Float beta (m - 1) emin).
+split.
+now exists f.
+split.
+unfold F2R, f, m.
+simpl.
+pattern x at 2 ; rewrite <- Rmult_1_r.
+change 1 with (bpow Z0).
+rewrite <- (Zplus_opp_l emin).
+rewrite epow_add.
+rewrite <- Rmult_assoc.
+apply Rmult_le_compat_r.
+apply epow_ge_0.
+generalize (x * bpow (- emin)%Z)%R.
+clear.
+intros.
+rewrite minus_Z2R.
+simpl.
+apply Rminus_le.
+replace (Z2R (up r) - 1 - r) with ((Z2R (up r) - r) - 1) by ring.
+apply Rle_minus.
+rewrite Z2R_IZR.
+eapply for_base_fp.
+intros g ((mx,ex),(H1,H2)) H3.
+rewrite H1.
+unfold F2R.
+rewrite H2.
+simpl.
+apply Rmult_le_compat_r.
+apply epow_ge_0.
+apply Z2R_le.
+apply Zlt_succ_le.
+apply lt_Z2R.
+apply Rmult_lt_reg_r with (bpow emin).
+apply epow_gt_0.
+apply Rle_lt_trans with x.
+rewrite <- H2.
+change (F2R (Float beta mx ex) <= x).
+now rewrite <- H1.
+pattern x ; rewrite <- Rmult_1_r.
+change R1 with (bpow Z0).
+rewrite <- (Zplus_opp_l emin).
+rewrite epow_add.
+rewrite <- Rmult_assoc.
+apply Rmult_lt_compat_r.
+apply epow_gt_0.
+change (m - 1)%Z with (Zpred m).
+rewrite <- Zsucc_pred.
+rewrite Z2R_IZR.
+eapply archimed.
+Qed.
+
+End RND_FIX.

src/Flocq_rnd_ex.v

 Require Import Flocq_Raux.
 Require Import Flocq_defs.
-
-Open Scope R_scope.
+Require Import Flocq_rnd_prop.
 
 Section RND_ex.
 
-Theorem Rnd_DN_pt_unicity :
-  forall F : R -> Prop,
-  forall x f1 f2 : R,
-  Rnd_DN_pt F x f1 -> Rnd_DN_pt F x f2 ->
-  f1 = f2.
-Proof.
-intros F x f1 f2 H1 H2.
-apply Rle_antisym.
-eapply H2.
-now eapply H1.
-now eapply H1.
-eapply H1.
-now eapply H2.
-now eapply H2.
-Qed.
-
-Theorem Rnd_DN_unicity :
-  forall F : R -> Prop,
-  forall rnd1 rnd2 : R -> R,
-  Rnd_DN F rnd1 -> Rnd_DN F rnd2 ->
-  forall x, rnd1 x = rnd2 x.
-Proof.
-intros F rnd1 rnd2 H1 H2 x.
-now eapply Rnd_DN_pt_unicity.
-Qed.
-
-Theorem Rnd_UP_pt_unicity :
-  forall F : R -> Prop,
-  forall x f1 f2 : R,
-  Rnd_UP_pt F x f1 -> Rnd_UP_pt F x f2 ->
-  f1 = f2.
-Proof.
-intros F x f1 f2 H2 H1.
-apply Rle_antisym.
-eapply H2.
-now eapply H1.
-now eapply H1.
-eapply H1.
-now eapply H2.
-now eapply H2.
-Qed.
-
-Theorem Rnd_UP_unicity :
-  forall F : R -> Prop,
-  forall rnd1 rnd2 : R -> R,
-  Rnd_UP F rnd1 -> Rnd_UP F rnd2 ->
-  forall x, rnd1 x = rnd2 x.
-Proof.
-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 f : R,
-  Rnd_DN_pt F (-x) (-f) -> Rnd_UP_pt F x f.
-Proof.
-intros F HF x f H.
-rewrite <- (Ropp_involutive f).
-repeat split.
-apply HF.
-apply H.
-apply Ropp_le_cancel.
-rewrite Ropp_involutive.
-apply H.
-intros.
-apply Ropp_le_cancel.
-rewrite Ropp_involutive.
-apply H.
-now apply HF.
-now apply Ropp_le_contravar.
-Qed.
-
-Theorem Rnd_DN_UP_sym :
-  forall F : R -> Prop,
-  ( forall x, F x -> F (- x) ) ->
-  forall rnd1 rnd2 : R -> R,
-  Rnd_DN F rnd1 -> Rnd_UP F rnd2 ->
-  forall x, rnd1 (- x) = - rnd2 x.
-Proof.
-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.
-rewrite Ropp_involutive.
-apply H1.
-Qed.
-
-Theorem Rnd_DN_pt_monotone :
-  forall F : R -> Prop,
-  forall x y f g : R,
-  Rnd_DN_pt F x f -> Rnd_DN_pt F y g ->
-  x <= y -> f <= g.
-Proof.
-intros F x y f g (Hx1,(Hx2,_)) (Hy1,(_,Hy2)) Hxy.
-apply Hy2.
-apply Hx1.
-now apply Rle_trans with (2 := Hxy).
-Qed.
-
-Theorem Rnd_DN_monotone :
-  forall F : R -> Prop,
-  forall rnd : R -> R,
-  Rnd_DN F rnd ->
-  MonotoneP rnd.
-Proof.
-intros F rnd Hr x y Hxy.
-now eapply Rnd_DN_pt_monotone.
-Qed.
-
-Theorem Rnd_DN_pt_idempotent :
-  forall F : R -> Prop,
-  forall x f : R,
-  Rnd_DN_pt F x f -> F x ->
-  f = x.
-Proof.
-intros F x f (_,(Hx1,Hx2)) Hx.
-apply Rle_antisym.
-exact Hx1.
-apply Hx2.
-exact Hx.
-apply Rle_refl.
-Qed.
-
-Theorem Rnd_DN_idempotent :
-  forall F : R -> Prop,
-  forall rnd : R -> R,
-  Rnd_DN F rnd ->
-  IdempotentP F rnd.
-Proof.
-intros F rnd Hr.
-split.
-intros.
-eapply Hr.
-intros x Hx.
-now apply Rnd_DN_pt_idempotent with (2 := Hx).
-Qed.
-
-Theorem Rnd_UP_pt_monotone :
-  forall F : R -> Prop,
-  forall x y f g : R,
-  Rnd_UP_pt F x f -> Rnd_UP_pt F y g ->
-  x <= y -> f <= g.
-Proof.
-intros F x y f g (Hx1,(_,Hx2)) (Hy1,(Hy2,_)) Hxy.
-apply Hx2.
-apply Hy1.
-now apply Rle_trans with (1 := Hxy).
-Qed.
-
-Theorem Rnd_UP_monotone :
-  forall F : R -> Prop,
-  forall rnd : R -> R,
-  Rnd_UP F rnd ->
-  MonotoneP rnd.
-Proof.
-intros F rnd Hr x y Hxy.
-now eapply Rnd_UP_pt_monotone.
-Qed.
-
-Theorem Rnd_UP_pt_idempotent :
-  forall F : R -> Prop,
-  forall x f : R,
-  Rnd_UP_pt F x f -> F x ->
-  f = x.
-Proof.
-intros F x f (_,(Hx1,Hx2)) Hx.
-apply Rle_antisym.
-apply Hx2.
-exact Hx.
-apply Rle_refl.
-exact Hx1.
-Qed.
-
-Theorem Rnd_UP_idempotent :
-  forall F : R -> Prop,
-  forall rnd : R -> R,
-  Rnd_UP F rnd ->
-  IdempotentP F rnd.
-Proof.
-intros F rnd Hr.
-split.
-intros.
-eapply Hr.
-intros x Hx.
-now apply Rnd_UP_pt_idempotent with (2 := Hx).
-Qed.
-
-Theorem Rnd_DN_pt_le_rnd :
-  forall F : R -> Prop,
-  forall rnd : R -> R,
-  Rounding_for_Format F rnd -> 
-  forall x fd : R,
-  Rnd_DN_pt F x fd ->
-  fd <= rnd x.
-Proof.
-intros F rnd (Hr1,(Hr2,Hr3)) x fd Hd.
-replace fd with (rnd fd).
-apply Hr1.
-apply Hd.
-apply Hr3.
-apply Hd.
-Qed.
-
-Theorem Rnd_DN_le_rnd :
-  forall F : R -> Prop,
-  forall rndd rnd: R -> R,
-  Rnd_DN F rndd -> 
-  Rounding_for_Format F rnd -> 
-  forall x, rndd x <= rnd x.
-Proof.
-intros F rndd rnd Hd Hr x.
-eapply Rnd_DN_pt_le_rnd.
-apply Hr.
-apply Hd.
-Qed.
-
-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 F : R -> Prop,
-  forall rndu rnd: R -> R,
-  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 Hfu.
-2 : now right.
-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,