Finished proof of DN_UP_parity_FLT_pos.

src/Flocq_Raux.v

@@ -775,6 +775,21 @@ now apply Rlt_le.
 now apply Rlt_le.
 Qed.
 
+Theorem ln_beta_bpow :
+  forall e, projT1 (ln_beta (bpow e)) = (e + 1)%Z.
+Proof.
+intros e.
+apply ln_beta_unique.
+rewrite Rabs_right.
+replace (e + 1 - 1)%Z with e by ring.
+split.
+apply Rle_refl.
+apply -> bpow_lt.
+apply Zlt_succ.
+apply Rle_ge.
+apply bpow_ge_0.
+Qed.
+
 Theorem Zpower_pos_gt_0 :
   forall b p, (0 < b)%Z ->
   (0 < Zpower_pos b p)%Z.

src/Flocq_rnd_FLT.v

@@ -156,6 +156,32 @@ apply Rle_lt_trans with (1 := Hx1).
 now apply Hx5.
 Qed.
 
+(* TODO: vérifier si ça implique ^^ *)
+Theorem FLT_canonic_FLX :
+  forall x : R,
+  (bpow (emin + prec - 1) <= Rabs x)%R ->
+  forall f : float beta,
+  ( canonic beta FLT_exp x f <-> canonic beta (FLX_exp prec) x f ).
+Proof.
+intros x Hx f.
+unfold canonic.
+replace (FLT_exp (projT1 (ln_beta beta x))) with (FLX_exp prec (projT1 (ln_beta beta x))).
+apply iff_refl.
+unfold FLX_exp, FLT_exp.
+apply sym_eq.
+apply Zmax_left.
+destruct (ln_beta beta x) as (ex, He).
+simpl.
+assert (emin + prec - 1 < ex)%Z. 2: omega.
+apply <- (bpow_lt beta).
+apply Rle_lt_trans with (1 := Hx).
+apply He.
+intros H.
+elim Rlt_not_le with (2 := Hx).
+rewrite H, Rabs_R0.
+apply bpow_gt_0.
+Qed.
+
 Theorem FLT_format_FIX :
   forall x,
   (Rabs x <= bpow (emin + prec))%R ->

src/Flocq_rnd_generic.v

@@ -35,6 +35,23 @@ exists (Float beta 0 _) ; repeat split.
 now rewrite F2R_0.
 Qed.
 
+Theorem generic_format_bpow :
+  forall e, (fexp (e + 1) <= e)%Z ->
+  generic_format (bpow e).
+Proof.
+intros e H.
+exists (Float beta (1 * Zpower (radix_val beta) (e - fexp (e + 1))) (fexp (e + 1))).
+split.
+rewrite <- F2R_change_exp.
+apply sym_eq.
+apply F2R_bpow.
+exact H.
+simpl.
+apply f_equal.
+apply sym_eq.
+apply ln_beta_bpow.
+Qed.
+
 Theorem generic_DN_pt_large_pos_ge_pow :
   forall x ex,
   (fexp ex < ex)%Z ->

src/Flocq_rnd_ne.v

@@ -561,9 +561,89 @@ Proof.
 intros x xd xu cd cu Hx0 Hfx Hd Hu Hxd Hxu Hed Heu.
 destruct (Rlt_or_le (bpow (emin + prec - 1)) x) as [Hx|Hx].
 (* . *)
-admit.
+assert (Hn : generic_format beta FLTf (bpow (emin + prec - 1))).
+apply generic_format_bpow.
+unfold FLT_exp.
+replace (emin + prec - 1 + 1 - prec)%Z with emin by ring.
+rewrite Zmax_idempotent.
+omega.
+apply DN_UP_parity_FLX_pos with prec x xd xu cd cu ; try easy.
+(* .. *)
+intros H.
+apply Hfx.
+apply -> FLT_format_generic. 2: exact Hp.
+apply <- FLT_format_FLX. 3: exact Hp.
+now apply <- FLX_format_generic.
+rewrite Rabs_pos_eq.
+now apply Rlt_le.
+now apply Rlt_le.
+(* .. *)
+apply -> FLT_canonic_FLX.
+eexact Hd.
+rewrite Rabs_pos_eq.
+apply Hxd.
+exact Hn.
+now apply Rlt_le.
+apply Hxd.
+apply generic_format_0.
+now apply Rlt_le.
+(* .. *)
+apply -> FLT_canonic_FLX.
+eexact Hu.
+rewrite Rabs_pos_eq.
+apply Rlt_le.
+apply Rlt_le_trans with (1 := Hx).
+apply Hxu.
+apply Rlt_le.
+apply Rlt_le_trans with (1 := Hx0).
+apply Hxu.
+(* .. *)
+apply Rnd_DN_pt_equiv_format with (a := bpow (emin + prec - 1)) (b := x) (4 := Hxd).
+exact Hn.
+intros a (Ha, _).
+apply iff_trans with (2 := FLX_format_generic beta prec Hp a).
+assert (Ha' : (bpow (emin + prec - 1) <= Rabs a)%R).
+rewrite Rabs_pos_eq.
+exact Ha.
+apply Rle_trans with (2 := Ha).
+apply bpow_ge_0.
+apply iff_trans with (2 := FLT_format_FLX beta emin prec Hp a Ha').
+apply iff_sym.
+now apply FLT_format_generic.
+split.
+now apply Rlt_le.
+apply Rle_refl.
+(* .. *)
+destruct (ln_beta beta x) as (ex, He).
+specialize (He (Rgt_not_eq _ _ Hx0)).
+rewrite Rabs_pos_eq in He.
+2: now apply Rlt_le.
+apply Rnd_UP_pt_equiv_format with (a := x) (b := bpow ex) (4 := Hxu).
+apply generic_format_bpow.
+unfold FLT_exp.
+rewrite Zmax_left.
+omega.
+assert (emin + prec - 1 <= ex)%Z. 2 : omega.
+apply <- (bpow_le beta).
+apply Rlt_le.
+now apply Rlt_trans with (2 := proj2 He).
+intros b (Hb, _).
+apply iff_trans with (2 := FLX_format_generic beta prec Hp b).
+assert (Hb' : (bpow (emin + prec - 1) <= Rabs b)%R).
+rewrite Rabs_pos_eq.
+apply Rle_trans with (2 := Hb).
+now apply Rlt_le.
+apply Rle_trans with (2 := Hb).
+now apply Rlt_le.
+apply iff_trans with (2 := FLT_format_FLX beta emin prec Hp b Hb').
+apply iff_sym.
+now apply FLT_format_generic.
+split.
+apply Rle_refl.
+now apply Rlt_le.
 (* . *)
 apply (DN_UP_parity_FIX emin x xd xu cd cu) ; trivial.
+(* .. *)
 intros H.
 apply Hfx.
 apply generic_format_fun_eq with (2 := H).
@@ -577,6 +657,7 @@ apply Rle_lt_trans with (1 := Hx).
 apply -> bpow_lt.
 apply Zlt_pred.
 now apply Rlt_le.
+(* .. *)
 apply canonic_fun_eq with (2 := Hd).
 apply sym_eq.
 apply FIX_FLT_exp_subnormal.
@@ -625,6 +706,7 @@ apply Zlt_pred.
 apply Hxd.
 apply generic_format_0.
 now apply Rlt_le.
+(* .. *)
 apply canonic_fun_eq with (2 := Hu).
 apply sym_eq.
 apply FIX_FLT_exp_subnormal.
@@ -634,16 +716,57 @@ apply Hxu.
 rewrite Rabs_pos_eq.
 apply Rle_lt_trans with (bpow (emin + prec - 1)).
 apply Hxu.
-exists (Float beta (Zpower (radix_val beta) (prec - 1)) emin).
-admit.
+apply generic_format_bpow.
+unfold FLT_exp.
+replace (emin + prec - 1 + 1 - prec)%Z with emin by ring.
+rewrite Zmax_idempotent.
+omega.
 exact Hx.
 apply -> bpow_lt.
 apply Zlt_pred.
 apply Rlt_le.
 apply Rlt_le_trans with (1 := Hx0).
 apply Hxu.
-admit.
-admit.
+(* .. *)
+apply Rnd_DN_pt_equiv_format with (a := R0) (b := x) (4 := Hxd).
+apply generic_format_0.
+intros a (Ha1, Ha2).
+apply iff_trans with (2 := FIX_format_generic beta emin a).
+assert (Ha' : (Rabs a <= bpow (emin + prec))%R).
+rewrite Rabs_pos_eq.
+apply Rle_trans with (1 := Ha2).
+apply Rle_trans with (1 := Hx).
+apply -> bpow_le.
+apply Zle_pred.
+exact Ha1.
+apply iff_trans with (2 := FLT_format_FIX beta emin prec Hp a Ha').
+apply iff_sym.
+now apply FLT_format_generic.
+split.
+now apply Rlt_le.
+apply Rle_refl.
+(* .. *)
+apply Rnd_UP_pt_equiv_format with (a := x) (b := bpow (emin + prec - 1)) (4 := Hxu).
+apply generic_format_bpow.
+unfold FLT_exp.
+replace (emin + prec - 1 + 1 - prec)%Z with emin by ring.
+rewrite Zmax_idempotent.
+omega.
+intros a (Ha1, Ha2).
+apply iff_trans with (2 := FIX_format_generic beta emin a).
+assert (Ha' : (Rabs a <= bpow (emin + prec))%R).
+rewrite Rabs_pos_eq.
+apply Rle_trans with (1 := Ha2).
+apply -> bpow_le.
+apply Zle_pred.
+apply Rle_trans with (2 := Ha1).
+now apply Rlt_le.
+apply iff_trans with (2 := FLT_format_FIX beta emin prec Hp a Ha').
+apply iff_sym.
+now apply FLT_format_generic.
+split.
+apply Rle_refl.
+exact Hx.
 Qed.
 
 Theorem Rnd_NE_pt_FLT :

src/Flocq_rnd_prop.v

@@ -1037,4 +1037,64 @@ rewrite <- Rnd_0 with (2 := H) ; trivial.
 now apply H.
 Qed.
 
+Theorem Rnd_DN_pt_equiv_format :
+  forall F1 F2 : R -> Prop,
+  forall a b : R,
+  F1 a ->
+  ( forall x, a <= x <= b -> (F1 x <-> F2 x) ) ->
+  forall x f, a <= x <= b -> Rnd_DN_pt F1 x f -> Rnd_DN_pt F2 x f.
+Proof.
+intros F1 F2 a b Ha HF x f Hx (H1, (H2, H3)).
+split.
+apply -> HF.
+exact H1.
+split.
+now apply H3.
+now apply Rle_trans with (1 := H2).
+split.
+exact H2.
+intros k Hk Hl.
+destruct (Rlt_or_le k a) as [H|H].
+apply Rlt_le.
+apply Rlt_le_trans with (1 := H).
+now apply H3.
+apply H3.
+apply <- HF.
+exact Hk.
+split.
+exact H.
+now apply Rle_trans with (1 := Hl).
+exact Hl.
+Qed.
+
+Theorem Rnd_UP_pt_equiv_format :
+  forall F1 F2 : R -> Prop,
+  forall a b : R,
+  F1 b ->
+  ( forall x, a <= x <= b -> (F1 x <-> F2 x) ) ->
+  forall x f, a <= x <= b -> Rnd_UP_pt F1 x f -> Rnd_UP_pt F2 x f.
+Proof.
+intros F1 F2 a b Hb HF x f Hx (H1, (H2, H3)).
+split.
+apply -> HF.
+exact H1.
+split.
+now apply Rle_trans with (2 := H2).
+now apply H3.
+split.
+exact H2.
+intros k Hk Hl.
+destruct (Rle_or_lt k b) as [H|H].
+apply H3.
+apply <- HF.
+exact Hk.
+split.
+now apply Rle_trans with (2 := Hl).
+exact H.
+exact Hl.
+apply Rlt_le.
+apply Rle_lt_trans with (2 := H).
+now apply H3.
+Qed.
+
 End RND_prop.