Partial of proof of FLX_format_satisfies_any.

src/Flocq_Raux.v

@@ -40,6 +40,17 @@ exact H.
 now rewrite 2!(Rmult_comm r).
 Qed.
 
+Lemma exp_increasing_weak :
+  forall x y : R,
+  (x <= y)%R -> (exp x <= exp y)%R.
+Proof.
+intros x y [H|H].
+apply Rlt_le.
+now apply exp_increasing.
+rewrite H.
+apply Rle_refl.
+Qed.
+
 End Rmissing.
 
 Section Z2R.
@@ -183,7 +194,7 @@ End Z2R.
 
 Section pow.
 
-Record radix :=  { radix_val :Z ; radix_prop :  (2 <= radix_val )%Z }.
+Record radix :=  { radix_val : Z ; radix_prop :  (2 <= radix_val )%Z }.
 
 Variable r: radix.
 
@@ -245,7 +256,7 @@ destruct r; simpl; auto with zarith.
 Qed.
 
 Lemma epow_add :
-  forall e1 e2 : Z, (epow (e1+e2) = epow e1 * epow e2)%R.
+  forall e1 e2 : Z, (epow (e1 + e2) = epow e1 * epow e2)%R.
 Proof.
 intros.
 repeat rewrite epow_powerRZ.
@@ -262,5 +273,197 @@ unfold epow, Zpower_pos, iter_pos.
 now rewrite Zmult_1_r.
 Qed.
 
-End pow.
+Lemma Z2R_Zpower :
+  forall e : Z,
+  (0 <= e)%Z ->
+  Z2R (Zpower (radix_val r) e) = epow e.
+Proof.
+intros [|e|e] H.
+split.
+split.
+now elim H.
+Qed.
+
+Lemma epow_lt_aux :
+  forall e1 e2 : Z,
+  (e1 < e2)%Z -> (epow e1 < epow e2)%R.
+Proof.
+intros e1 e2 H.
+replace e2 with (e1 + (e2 - e1))%Z by ring.
+rewrite <- (Rmult_1_r (epow e1)).
+rewrite epow_add.
+apply Rmult_lt_compat_l.
+apply epow_gt_0.
+assert (0 < e2 - e1)%Z by omega.
+destruct (e2 - e1)%Z ; try discriminate H0.
+clear.
+unfold epow.
+apply (Z2R_lt 1).
+rewrite Zpower_pos_nat.
+case_eq (nat_of_P p).
+intros H.
+elim (lt_irrefl 0).
+pattern O at 2 ; rewrite <- H.
+apply lt_O_nat_of_P.
+intros n _.
+assert (1 < Zpower_nat (radix_val r) 1)%Z.
+unfold Zpower_nat, iter_nat.
+rewrite Zmult_1_r.
+generalize (radix_prop r).
+omega.
+induction n.
+exact H.
+change (S (S n)) with (1 + (S n))%nat.
+rewrite Zpower_nat_is_exp.
+change 1%Z with (1 * 1)%Z.
+apply Zmult_lt_compat.
+now split.
+now split.
+Qed.
+
+Lemma epow_lt :
+  forall e1 e2 : Z,
+  (e1 < e2)%Z <-> (epow e1 < epow e2)%R.
+Proof.
+intros e1 e2.
+split.
+apply epow_lt_aux.
+intros H.
+apply Zgt_lt.
+apply Znot_le_gt.
+intros H'.
+apply Rlt_not_le with (1 := H).
+destruct (Zle_lt_or_eq _ _ H').
+apply Rlt_le.
+now apply epow_lt_aux.
+apply Req_le.
+now apply f_equal.
+Qed.
+
+Lemma epow_le :
+  forall e1 e2 : Z,
+  (e1 <= e2)%Z <-> (epow e1 <= epow e2)%R.
+Proof.
+intros e1 e2.
+split.
+intros H.
+apply Rnot_lt_le.
+intros H'.
+apply Zle_not_gt with (1 := H).
+apply Zlt_gt.
+now apply <- epow_lt.
+intros H.
+apply Znot_gt_le.
+intros H'.
+apply Rle_not_lt with (1 := H).
+apply -> epow_lt.
+now apply Zgt_lt.
+Qed.
 
+Lemma epow_eq :
+  forall e1 e2 : Z,
+  e1 = e2 -> epow e1 = epow e2.
+Proof.
+intros.
+apply Rle_antisym.
+apply -> epow_le.
+now apply Zeq_le.
+apply -> epow_le.
+apply Zeq_le.
+now apply eq_sym.
+Qed.
+
+Lemma epow_exp :
+  forall e : Z,
+  epow e = exp (Z2R e * ln (Z2R (radix_val r))).
+Proof.
+(* positive case *)
+assert (forall e, epow (Zpos e) = exp (Z2R (Zpos e) * ln (Z2R (radix_val r)))).
+intros e.
+unfold epow.
+rewrite Zpower_pos_nat.
+unfold Z2R at 2.
+rewrite P2R_INR.
+induction (nat_of_P e).
+rewrite Rmult_0_l.
+unfold Zpower_nat, iter_nat.
+now rewrite exp_0.
+change (S n) with (1 + n)%nat.
+rewrite plus_INR.
+rewrite Zpower_nat_is_exp.
+rewrite Rmult_plus_distr_r.
+rewrite exp_plus.
+rewrite Rmult_1_l.
+rewrite exp_ln.
+rewrite <- IHn.
+rewrite <- mult_Z2R.
+apply f_equal.
+unfold Zpower_nat at 1, iter_nat.
+now rewrite Zmult_1_r.
+apply (Z2R_lt 0).
+generalize (radix_prop r).
+omega.
+(* general case *)
+intros [|e|e].
+rewrite Rmult_0_l.
+now rewrite exp_0.
+apply H.
+unfold epow.
+change (Z2R (Zpower_pos (radix_val r) e)) with (epow (Zpos e)).
+rewrite H.
+rewrite <- exp_Ropp.
+rewrite <- Ropp_mult_distr_l_reverse.
+now rewrite <- opp_Z2R.
+Qed.
+
+Lemma ln_beta :
+  forall x : R, (0 < x)%R ->
+  {e | (epow (e - 1)%Z <= x < epow e)%R}.
+Proof.
+intros x Hx.
+set (fact := ln (Z2R (radix_val r))).
+(* . *)
+assert (0 < fact)%R.
+apply exp_lt_inv.
+rewrite exp_0.
+unfold fact.
+rewrite exp_ln.
+apply (Z2R_lt 1).
+generalize (radix_prop r).
+omega.
+apply (Z2R_lt 0).
+generalize (radix_prop r).
+omega.
+(* . *)
+exists (up (ln x / fact))%Z.
+rewrite 2!epow_exp.
+fold fact.
+pattern x at 2 3 ; replace x with (exp (ln x / fact * fact)).
+split.
+rewrite minus_Z2R.
+apply exp_increasing_weak.
+apply Rmult_le_compat_r.
+now apply Rlt_le.
+simpl (Z2R 1).
+pattern (ln x / fact)%R at 2 ; replace (ln x / fact)%R with (1 + (ln x / fact - 1))%R by ring.
+replace (Z2R (up (ln x / fact)) - 1)%R with ((Z2R (up (ln x / fact)) - ln x / fact) + (ln x / fact - 1))%R by ring.
+apply Rplus_le_compat_r.
+rewrite Z2R_IZR.
+eapply for_base_fp.
+apply exp_increasing.
+apply Rmult_lt_compat_r.
+exact H.
+rewrite Z2R_IZR.
+apply Rplus_lt_reg_r with (- (ln x / fact))%R.
+rewrite Rplus_opp_l.
+rewrite Rplus_comm.
+eapply for_base_fp.
+unfold Rdiv.
+rewrite Rmult_assoc.
+rewrite Rinv_l.
+rewrite Rmult_1_r.
+now apply exp_ln.
+now apply Rgt_not_eq.
+Qed.
+
+End pow.

src/Flocq_rnd_FLX.v

+Require Import Flocq_Raux.
+Require Import Flocq_defs.
+Require Import Flocq_rnd_ex.
+Require Import Flocq_rnd_prop.
+Require Import Flocq_rnd_FIX.
+
+Section RND_FIX.
+
+Open Scope R_scope.
+
+Variable beta : radix.
+
+Notation bpow := (epow beta).
+
+Lemma F2R_pos_imp_Fnum_pos :
+  forall f : float beta,
+  0 <= F2R f ->
+  (0 <= Fnum f)%Z.
+Proof.
+intros f H.
+apply le_Z2R.
+apply Rmult_le_reg_l with (bpow (Fexp f)).
+apply epow_gt_0.
+rewrite Rmult_0_r.
+now rewrite Rmult_comm.
+Qed.
+
+Lemma F2R_constrain :
+  forall m e e' p : Z,
+  (Zabs m < Zpower (radix_val beta) p)%Z ->
+  bpow e' <= F2R (Float beta m e) ->
+  exists m' : Z,
+  F2R (Float beta m e) = F2R (Float beta m' (e' - (p - 1))).
+Proof.
+intros m e e' p Hm Hf.
+exists (m * Zpower (radix_val beta) (e - (e' - (p - 1))))%Z.
+unfold F2R.
+simpl.
+rewrite mult_Z2R.
+rewrite Rmult_assoc.
+apply Rmult_eq_compat_l.
+rewrite Z2R_Zpower.
+rewrite <- epow_add.
+apply f_equal.
+ring.
+assert (e' <= e + (p - 1))%Z.
+2: omega.
+apply Zlt_succ_le.
+unfold Zsucc.
+replace (e + (p - 1) + 1)%Z with (e + p)%Z by ring.
+apply <- epow_lt.
+apply Rle_lt_trans with (1 := Hf).
+unfold F2R.
+rewrite epow_add.
+rewrite Rmult_comm.
+apply Rmult_lt_compat_l.
+apply epow_gt_0.
+simpl.
+apply Rle_lt_trans with (1 := RRle_abs _).
+rewrite Z2R_IZR.
+rewrite Rabs_Zabs.
+rewrite <- Z2R_IZR.
+replace (bpow p) with (Z2R (Zpower (radix_val beta) p)).
+now apply Z2R_lt.
+rewrite Z2R_Zpower.
+apply refl_equal.
+clear -Hm.
+destruct p as [_|p|p] ; try discriminate.
+simpl in Hm.
+elim Zlt_not_le with (1 := Hm).
+apply Zabs_pos.
+Qed.
+
+Variable prec : Z.
+Variable Hp : Zlt 0 prec.
+
+Theorem FLX_format_satisfies_any :
+  satisfies_any (FLX_format beta prec).
+Proof.
+refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
+(* symmetric set *)
+exists (Float beta 0 0).
+split.
+unfold F2R.
+now rewrite Rmult_0_l.
+apply lt_Z2R.
+rewrite Z2R_Zpower.
+apply epow_gt_0.
+now apply Zlt_le_weak.
+intros x ((m,e),(H1,H2)).
+exists (Float beta (-m) e).
+split.
+rewrite H1.
+unfold F2R.
+simpl.
+now rewrite opp_Z2R, Ropp_mult_distr_l_reverse.
+simpl.
+now rewrite Zabs_Zopp.
+(* rounding down *)
+assert (Hh : forall x, 0 > x -> 0 < -x).
+intros x Hx.
+apply Ropp_gt_lt_0_contravar.
+exact Hx.
+exists (fun x =>
+  let e :=
+  Zminus match total_order_T 0 x with
+  | inleft (left Hx) => projS1 (ln_beta beta _ Hx)
+  | inleft (right Hx) => Z0
+  | inright Hx => projS1 (ln_beta beta _ (Hh _ Hx))
+  end prec in
+  match FIX_format_satisfies_any beta e with
+  | Satisfies_any _ _ rnd Hr => rnd x
+  end).
+intros x.
+destruct (total_order_T 0 x) as [[Hx|Hx]|Hx].
+(* x positive *)
+clear Hh.
+set (e := (projT1 (ln_beta beta x Hx) - prec)%Z).
+destruct (FIX_format_satisfies_any beta e) as (_,_,rnd,Hr).
+destruct (Hr x) as ((f,(Hr1,Hr2)),(Hr3,Hr4)).
+destruct (ln_beta beta x Hx) as (e', Hb).
+simpl in e.
+split.
+(* - f is compatible with the format *)
+assert (Hm: (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z).
+apply Zgt_lt.
+apply Znot_le_gt.
+intros Hm.
+apply Rlt_not_le with (1 := proj2 Hb).
+apply Rle_trans with (2 := Hr3).
+rewrite Hr1.
+unfold F2R.
+rewrite Hr2.
+replace e' with (prec + e)%Z by ( unfold e ; ring ).
+rewrite epow_add.
+apply Rmult_le_compat_r.
+apply epow_ge_0.
+rewrite <- Z2R_Zpower.
+apply Z2R_le.
+rewrite <- (Zabs_eq (Fnum f)).
+exact Hm.
+apply F2R_pos_imp_Fnum_pos.
+rewrite <- Hr1.
+apply Rnd_pos_imp_pos with (FIX_format beta e).
+exists (Float beta 0 e).
+repeat split.
+unfold F2R.
+now rewrite Rmult_0_l.
+split.
+now apply Rnd_DN_monotone with (FIX_format beta e).
+now apply Rnd_DN_idempotent.
+now apply Rlt_le.
+now apply Zlt_le_weak.
+now exists f ; split.
+(* - f is the biggest float smaller than x *)
+split.
+exact Hr3.
+intros g ((mg,eg),(Hg1,Hg2)) Hgx.
+destruct (Rle_or_lt g (bpow (e' - 1)%Z)).
+apply Rle_trans with (1 := H).
+apply Hr4.
+exists (Float beta (Zpower (radix_val beta) (prec - 1)) e).
+repeat split.
+unfold F2R.
+simpl.
+rewrite Z2R_Zpower.
+rewrite <- epow_add.
+unfold e.
+apply f_equal.
+ring.
+omega.
+apply Hb.
+apply Hr4.
+destruct (F2R_constrain mg eg (e' - 1) prec Hg2) as (mg',Hg).
+rewrite <- Hg1.
+now apply Rlt_le.
+rewrite Hg1, Hg.
+replace (e' - 1 - (prec - 1))%Z with (e' - prec)%Z by ring.
+now exists (Float beta mg' (e' - prec)).
+exact Hgx.
+(* x zero *)
+admit.
+(* x negative *)
+admit.
+Qed.
+
+End RND_FIX.

src/Makefile.am

@@ -2,6 +2,7 @@ FILES = \
 	Flocq_Raux.v \
 	Flocq_defs.v \
 	Flocq_rnd_FIX.v \
+	Flocq_rnd_FLX.v \
 	Flocq_rnd_ex.v \
 	Flocq_rnd_prop.v
 
@@ -13,7 +14,7 @@ datadir = $(libdir)
 
 .v.vo:
 	@echo COQC $<
-	@$(COQC) $(COQRFLAG) $<
+	@$(COQC) $(COQRFLAG) -dont-load-proofs $<
 
 .v.vd:
 	@echo COQDEP $<