Update Flocq to version 2.5.2

This version of Flocq is compatible with Coq 8.6

8 files changed, 91 insertions, 132 deletions

diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v
index a4accfa5..6400304b 100644
--- a/flocq/Appli/Fappli_IEEE.v
+++ b/flocq/Appli/Fappli_IEEE.v
@@ -1,4 +1,3 @@
-Unset Bracketing Last Introduction Pattern.
 (**
 This file is part of the Flocq formalization of floating-point
 arithmetic in Coq: http://flocq.gforge.inria.fr/
@@ -416,8 +415,7 @@ Theorem is_finite_Bopp :
   forall opp_nan x,
   is_finite (Bopp opp_nan x) = is_finite x.
 Proof.
-intros opp_nan [| | |] ; try easy.
-intros s pl.
+intros opp_nan [| |s pl|] ; try easy.
 simpl.
 now case opp_nan.
 Qed.
@@ -446,8 +444,7 @@ Theorem is_finite_Babs :
   forall abs_nan x,
   is_finite (Babs abs_nan x) = is_finite x.
 Proof.
-  intros abs_nan [| | |] ; try easy.
-  intros s pl.
+  intros abs_nan [| |s pl|] ; try easy.
   simpl.
   now case abs_nan.
 Qed.
diff --git a/flocq/Calc/Fcalc_round.v b/flocq/Calc/Fcalc_round.v
index 19652d08..86422247 100644
--- a/flocq/Calc/Fcalc_round.v
+++ b/flocq/Calc/Fcalc_round.v
@@ -646,8 +646,9 @@ case Zlt_bool_spec ; intros Hk.
 (* *)
 unfold truncate_aux.
 rewrite Fx at 1.
-unshelve refine (let H := _ in conj _ H).
+assert (H: (e + k)%Z = canonic_exp beta fexp x).
 unfold k. ring.
+refine (conj _ H).
 rewrite <- H.
 apply F2R_eq_compat.
 replace (scaled_mantissa beta fexp x) with (Z2R (Zfloor (scaled_mantissa beta fexp x))).
diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v
index d728e0ba..939002cf 100644
--- a/flocq/Core/Fcore_Raux.v
+++ b/flocq/Core/Fcore_Raux.v
@@ -1673,7 +1673,7 @@ Qed.
 (** Another well-used function for having the logarithm of a real number x to the base #&beta;# *)
 Record ln_beta_prop x := {
   ln_beta_val :> Z ;
-   _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R
+  _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R
 }.
 
 Definition ln_beta :
diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v
index 7d1d490a..53743035 100644
--- a/flocq/Core/Fcore_digits.v
+++ b/flocq/Core/Fcore_digits.v
@@ -853,7 +853,8 @@ Proof.
 intros n Zn.
 rewrite <- (Zdigits_abs n).
 assert (Hn: (0 < Zabs n)%Z).
-destruct n ; now easy.
+destruct n ; [|easy|easy].
+now elim Zn.
 destruct (Zabs n) as [|p|p] ; try easy ; clear.
 simpl.
 generalize 1%Z (radix_val beta) (refl_equal Lt : (0 < 1)%Z).
diff --git a/flocq/Core/Fcore_generic_fmt.v b/flocq/Core/Fcore_generic_fmt.v
index bac65b9d..21e51890 100644
--- a/flocq/Core/Fcore_generic_fmt.v
+++ b/flocq/Core/Fcore_generic_fmt.v
@@ -136,9 +136,9 @@ Proof.
 intros e He.
 apply generic_format_bpow.
 destruct (Zle_lt_or_eq _ _ He).
-now apply valid_exp.
+now apply valid_exp_.
 rewrite <- H.
-apply valid_exp_.
+apply valid_exp.
 rewrite H.
 apply Zle_refl.
 Qed.
@@ -604,107 +604,6 @@ Qed.
 Definition round x :=
   F2R (Float beta (rnd (scaled_mantissa x)) (canonic_exp x)).
 
-Theorem round_le_pos :
-  forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R.
-Proof.
-intros x y Hx Hxy.
-unfold round, scaled_mantissa, canonic_exp.
-destruct (ln_beta beta x) as (ex, Hex). simpl.
-destruct (ln_beta beta y) as (ey, Hey). simpl.
-specialize (Hex (Rgt_not_eq _ _ Hx)).
-specialize (Hey (Rgt_not_eq _ _ (Rlt_le_trans _ _ _ Hx Hxy))).
-rewrite Rabs_pos_eq in Hex.
-2: now apply Rlt_le.
-rewrite Rabs_pos_eq in Hey.
-2: apply Rle_trans with (2:=Hxy); now apply Rlt_le.
-assert (He: (ex <= ey)%Z).
-cut (ex - 1 < ey)%Z. omega.
-apply (lt_bpow beta).
-apply Rle_lt_trans with (1 := proj1 Hex).
-apply Rle_lt_trans with (1 := Hxy).
-apply Hey.
-destruct (Zle_or_lt ey (fexp ey)) as [Hy1|Hy1].
-rewrite (proj2 (proj2 (valid_exp ey) Hy1) ex).
-apply F2R_le_compat.
-apply Zrnd_le.
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-exact Hxy.
-now apply Zle_trans with ey.
-destruct (Zle_lt_or_eq _ _ He) as [He'|He'].
-destruct (Zle_or_lt ey (fexp ex)) as [Hx2|Hx2].
-rewrite (proj2 (proj2 (valid_exp ex) (Zle_trans _ _ _ He Hx2)) ey Hx2).
-apply F2R_le_compat.
-apply Zrnd_le.
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-exact Hxy.
-apply Rle_trans with (F2R (Float beta (rnd (bpow (ey - 1) * bpow (- fexp ey))) (fexp ey))).
-rewrite <- bpow_plus.
-rewrite <- (Z2R_Zpower beta (ey - 1 + -fexp ey)). 2: omega.
-rewrite Zrnd_Z2R.
-destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1].
-apply Rle_trans with (F2R (Float beta 1 (fexp ex))).
-apply F2R_le_compat.
-rewrite <- (Zrnd_Z2R 1).
-apply Zrnd_le.
-apply Rlt_le.
-exact (proj2 (mantissa_small_pos _ _ Hex Hx1)).
-unfold F2R. simpl.
-rewrite Z2R_Zpower. 2: omega.
-rewrite <- bpow_plus, Rmult_1_l.
-apply bpow_le.
-omega.
-apply Rle_trans with (F2R (Float beta (rnd (bpow ex * bpow (- fexp ex))) (fexp ex))).
-apply F2R_le_compat.
-apply Zrnd_le.
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-apply Rlt_le.
-apply Hex.
-rewrite <- bpow_plus.
-rewrite <- Z2R_Zpower. 2: omega.
-rewrite Zrnd_Z2R.
-unfold F2R. simpl.
-rewrite 2!Z2R_Zpower ; try omega.
-rewrite <- 2!bpow_plus.
-apply bpow_le.
-omega.
-apply F2R_le_compat.
-apply Zrnd_le.
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-apply Hey.
-rewrite He'.
-apply F2R_le_compat.
-apply Zrnd_le.
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-exact Hxy.
-Qed.
-
-Theorem round_generic :
-  forall x,
-  generic_format x ->
-  round x = x.
-Proof.
-intros x Hx.
-unfold round.
-rewrite scaled_mantissa_generic with (1 := Hx).
-rewrite Zrnd_Z2R.
-now apply sym_eq.
-Qed.
-
-Theorem round_0 :
-  round 0 = R0.
-Proof.
-unfold round, scaled_mantissa.
-rewrite Rmult_0_l.
-fold (Z2R 0).
-rewrite Zrnd_Z2R.
-apply F2R_0.
-Qed.
-
 Theorem round_bounded_large_pos :
   forall x ex,
   (fexp ex < ex)%Z ->
@@ -792,6 +691,74 @@ refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))).
 now apply mantissa_small_pos.
 Qed.
 
+Theorem round_le_pos :
+  forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R.
+Proof.
+intros x y Hx Hxy.
+destruct (ln_beta beta x) as [ex Hex].
+destruct (ln_beta beta y) as [ey Hey].
+specialize (Hex (Rgt_not_eq _ _ Hx)).
+specialize (Hey (Rgt_not_eq _ _ (Rlt_le_trans _ _ _ Hx Hxy))).
+rewrite Rabs_pos_eq in Hex.
+2: now apply Rlt_le.
+rewrite Rabs_pos_eq in Hey.
+2: apply Rle_trans with (2:=Hxy); now apply Rlt_le.
+assert (He: (ex <= ey)%Z).
+  apply bpow_lt_bpow with beta.
+  apply Rle_lt_trans with (1 := proj1 Hex).
+  now apply Rle_lt_trans with y.
+assert (Heq: fexp ex = fexp ey -> (round x <= round y)%R).
+  intros H.
+  unfold round, scaled_mantissa, canonic_exp.
+  rewrite ln_beta_unique_pos with (1 := Hex).
+  rewrite ln_beta_unique_pos with (1 := Hey).
+  rewrite H.
+  apply F2R_le_compat.
+  apply Zrnd_le.
+  apply Rmult_le_compat_r with (2 := Hxy).
+  apply bpow_ge_0.
+destruct (Zle_or_lt ey (fexp ey)) as [Hy1|Hy1].
+  apply Heq.
+  apply valid_exp with (1 := Hy1).
+  now apply Zle_trans with ey.
+destruct (Zle_lt_or_eq _ _ He) as [He'|He'].
+2: now apply Heq, f_equal.
+apply Rle_trans with (bpow (ey - 1)).
+2: now apply round_bounded_large_pos.
+destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1].
+  destruct (round_bounded_small_pos _ _ Hx1 Hex) as [-> | ->].
+  apply bpow_ge_0.
+  apply bpow_le.
+  apply valid_exp, proj2 in Hx1.
+  specialize (Hx1 ey).
+  omega.
+apply Rle_trans with (bpow ex).
+now apply round_bounded_large_pos.
+apply bpow_le.
+now apply Z.lt_le_pred.
+Qed.
+
+Theorem round_generic :
+  forall x,
+  generic_format x ->
+  round x = x.
+Proof.
+intros x Hx.
+unfold round.
+rewrite scaled_mantissa_generic with (1 := Hx).
+rewrite Zrnd_Z2R.
+now apply sym_eq.
+Qed.
+
+Theorem round_0 :
+  round 0 = R0.
+Proof.
+unfold round, scaled_mantissa.
+rewrite Rmult_0_l.
+fold (Z2R 0).
+rewrite Zrnd_Z2R.
+apply F2R_0.
+Qed.
 
 Theorem exp_small_round_0_pos :
   forall x ex,
@@ -807,9 +774,6 @@ apply bpow_gt_0.
 apply  (round_bounded_large_pos); assumption.
 Qed.
 
-
-
-
 Theorem generic_format_round_pos :
   forall x,
   (0 < x)%R ->
@@ -832,14 +796,11 @@ destruct (Rle_or_lt (bpow ex) (round x)) as [Hr|Hr].
 rewrite <- (Rle_antisym _ _ Hr Hr2).
 apply generic_format_bpow.
 now apply valid_exp.
-assert (Hr' := conj Hr1 Hr).
-unfold generic_format, scaled_mantissa.
-rewrite (canonic_exp_fexp_pos _ _ Hr').
-unfold round, scaled_mantissa.
+apply generic_format_F2R.
+intros _.
+rewrite (canonic_exp_fexp_pos (F2R _) _ (conj Hr1 Hr)).
 rewrite (canonic_exp_fexp_pos _ _ Hex).
-unfold F2R at 3. simpl.
-rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
-now rewrite Ztrunc_Z2R.
+now apply Zeq_le.
 Qed.
 
 End Fcore_generic_round_pos.
diff --git a/flocq/Core/Fcore_rnd.v b/flocq/Core/Fcore_rnd.v
index 171c27fc..e5091684 100644
--- a/flocq/Core/Fcore_rnd.v
+++ b/flocq/Core/Fcore_rnd.v
@@ -275,15 +275,13 @@ Theorem Only_DN_or_UP :
   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).
+intros F x fd fu f Hd Hu Hf [Hdf Hfu].
+destruct (Rle_or_lt x f) ; [right|left].
+apply Rle_antisym with (1 := Hfu).
 now apply Hu.
-elim Rlt_not_le with (1 := Hdf).
-apply Hd ; auto with real.
+apply Rlt_le in H.
+apply Rle_antisym with (2 := Hdf).
+now apply Hd.
 Qed.
 
 Theorem Rnd_ZR_abs :
diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v
index 1c27de31..28d2bc35 100644
--- a/flocq/Core/Fcore_ulp.v
+++ b/flocq/Core/Fcore_ulp.v
@@ -35,6 +35,7 @@ Variable fexp : Z -> Z.
 (** Definition and basic properties about the minimal exponent, when it exists *)
 
 Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z.
+Proof.
 intros.
 destruct (Z_le_dec x y).
 now left.
@@ -158,8 +159,7 @@ rewrite ulp_neq_0.
 unfold F2R; simpl.
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
-replace 1%R with (Z2R (Zsucc 0)) by reflexivity.
-apply Z2R_le.
+apply (Z2R_le (Zsucc 0)).
 apply Zlt_le_succ.
 apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
 now rewrite <- Fx.
@@ -206,6 +206,7 @@ Qed.
 
 Theorem ulp_bpow :
   forall e, ulp (bpow e) = bpow (fexp (e + 1)).
+Proof.
 intros e.
 rewrite ulp_neq_0.
 apply f_equal.
diff --git a/flocq/Flocq_version.v b/flocq/Flocq_version.v
index c391f590..b01a08f9 100644
--- a/flocq/Flocq_version.v
+++ b/flocq/Flocq_version.v
@@ -29,4 +29,4 @@ Definition Flocq_version := Eval vm_compute in
       parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N
     | Empty_string => (major * 100 + minor)%N
     end in
-  parse "2.5.0"%string N0 N0.
+  parse "2.5.2"%string N0 N0.