Upgrade to flocq 2.4.0

4 files changed, 17 insertions, 436 deletions

diff --git a/flocq/Calc/Fcalc_bracket.v b/flocq/Calc/Fcalc_bracket.v
index 90a8588e..03ef7bd3 100644
--- a/flocq/Calc/Fcalc_bracket.v
+++ b/flocq/Calc/Fcalc_bracket.v
@@ -168,7 +168,7 @@ apply Rplus_lt_reg_r with (d * (v - 1))%R.
 ring_simplify.
 rewrite Rmult_comm.
 now apply Rmult_lt_compat_l.
-apply Rplus_lt_reg_r with (-u * v)%R.
+apply Rplus_lt_reg_l with (-u * v)%R.
 replace (- u * v + (d + v * (u - d)))%R with (d * (1 - v))%R by ring.
 replace (- u * v + u)%R with (u * (1 - v))%R by ring.
 apply Rmult_lt_compat_r.
diff --git a/flocq/Calc/Fcalc_digits.v b/flocq/Calc/Fcalc_digits.v
index 4f76cc2d..45133e81 100644
--- a/flocq/Calc/Fcalc_digits.v
+++ b/flocq/Calc/Fcalc_digits.v
@@ -29,8 +29,6 @@ Section Fcalc_digits.
 Variable beta : radix.
 Notation bpow e := (bpow beta e).
 
-
-
 Theorem Zdigits_ln_beta :
   forall n,
   n <> Z0 ->
@@ -62,321 +60,4 @@ apply sym_eq.
 now apply Zdigits_ln_beta.
 Qed.
 
-Theorem Zdigits_mult_Zpower :
-  forall m e,
-  m <> Z0 -> (0 <= e)%Z ->
-  Zdigits beta (m * Zpower beta e) = (Zdigits beta m + e)%Z.
-Proof.
-intros m e Hm He.
-rewrite <- ln_beta_F2R_Zdigits with (1 := Hm).
-rewrite Zdigits_ln_beta.
-rewrite Z2R_mult.
-now rewrite Z2R_Zpower with (1 := He).
-contradict Hm.
-apply Zmult_integral_l with (2 := Hm).
-apply neq_Z2R.
-rewrite Z2R_Zpower with (1 := He).
-apply Rgt_not_eq.
-apply bpow_gt_0.
-Qed.
-
-Theorem Zdigits_Zpower :
-  forall e,
-  (0 <= e)%Z ->
-  Zdigits beta (Zpower beta e) = (e + 1)%Z.
-Proof.
-intros e He.
-rewrite <- (Zmult_1_l (Zpower beta e)).
-rewrite Zdigits_mult_Zpower ; try easy.
-apply Zplus_comm.
-Qed.
-
-Theorem Zdigits_le :
-  forall x y,
-  (0 <= x)%Z -> (x <= y)%Z ->
-  (Zdigits beta x <= Zdigits beta y)%Z.
-Proof.
-intros x y Hx Hxy.
-case (Z_lt_le_dec 0 x).
-clear Hx. intros Hx.
-rewrite 2!Zdigits_ln_beta.
-apply ln_beta_le.
-now apply (Z2R_lt 0).
-now apply Z2R_le.
-apply Zgt_not_eq.
-now apply Zlt_le_trans with x.
-now apply Zgt_not_eq.
-intros Hx'.
-rewrite (Zle_antisym _ _ Hx' Hx).
-apply Zdigits_ge_0.
-Qed.
-
-Theorem lt_Zdigits :
-  forall x y,
-  (0 <= y)%Z ->
-  (Zdigits beta x < Zdigits beta y)%Z ->
-  (x < y)%Z.
-Proof.
-intros x y Hy.
-cut (y <= x -> Zdigits beta y <= Zdigits beta x)%Z. omega.
-now apply Zdigits_le.
-Qed.
-
-Theorem Zpower_le_Zdigits :
-  forall e x,
-  (e < Zdigits beta x)%Z ->
-  (Zpower beta e <= Zabs x)%Z.
-Proof.
-intros e x Hex.
-destruct (Zdigits_correct beta x) as (H1,H2).
-apply Zle_trans with (2 := H1).
-apply Zpower_le.
-clear -Hex ; omega.
-Qed.
-
-Theorem Zdigits_le_Zpower :
-  forall e x,
-  (Zabs x < Zpower beta e)%Z ->
-  (Zdigits beta x <= e)%Z.
-Proof.
-intros e x.
-generalize (Zpower_le_Zdigits e x).
-omega.
-Qed.
-
-Theorem Zpower_gt_Zdigits :
-  forall e x,
-  (Zdigits beta x <= e)%Z ->
-  (Zabs x < Zpower beta e)%Z.
-Proof.
-intros e x Hex.
-destruct (Zdigits_correct beta x) as (H1,H2).
-apply Zlt_le_trans with (1 := H2).
-now apply Zpower_le.
-Qed.
-
-Theorem Zdigits_gt_Zpower :
-  forall e x,
-  (Zpower beta e <= Zabs x)%Z ->
-  (e < Zdigits beta x)%Z.
-Proof.
-intros e x Hex.
-generalize (Zpower_gt_Zdigits e x).
-omega.
-Qed.
-
-(** Characterizes the number digits of a product.
-
-This strong version is needed for proofs of division and square root
-algorithms, since they involve operation remainders.
-*)
-
-Theorem Zdigits_mult_strong :
-  forall x y,
-  (0 <= x)%Z -> (0 <= y)%Z ->
-  (Zdigits beta (x + y + x * y) <= Zdigits beta x + Zdigits beta y)%Z.
-Proof.
-intros x y Hx Hy.
-case (Z_lt_le_dec 0 x).
-clear Hx. intros Hx.
-case (Z_lt_le_dec 0 y).
-clear Hy. intros Hy.
-(* . *)
-assert (Hxy: (0 < Z2R (x + y + x * y))%R).
-apply (Z2R_lt 0).
-change Z0 with (0 + 0 + 0)%Z.
-apply Zplus_lt_compat.
-now apply Zplus_lt_compat.
-now apply Zmult_lt_0_compat.
-rewrite 3!Zdigits_ln_beta ; try now (apply sym_not_eq ; apply Zlt_not_eq).
-apply ln_beta_le_bpow with (1 := Rgt_not_eq _ _ Hxy).
-rewrite Rabs_pos_eq with (1 := Rlt_le _ _ Hxy).
-destruct (ln_beta beta (Z2R x)) as (ex, Hex). simpl.
-specialize (Hex (Rgt_not_eq _ _ (Z2R_lt _ _ Hx))).
-destruct (ln_beta beta (Z2R y)) as (ey, Hey). simpl.
-specialize (Hey (Rgt_not_eq _ _ (Z2R_lt _ _ Hy))).
-apply Rlt_le_trans with (Z2R (x + 1) * Z2R (y + 1))%R.
-rewrite <- Z2R_mult.
-apply Z2R_lt.
-apply Zplus_lt_reg_r with (- (x + y + x * y + 1))%Z.
-now ring_simplify.
-rewrite bpow_plus.
-apply Rmult_le_compat ; try (apply (Z2R_le 0) ; omega).
-rewrite <- (Rmult_1_r (Z2R (x + 1))).
-change (F2R (Float beta (x + 1) 0) <= bpow ex)%R.
-apply F2R_p1_le_bpow.
-exact Hx.
-unfold F2R. rewrite Rmult_1_r.
-apply Rle_lt_trans with (Rabs (Z2R x)).
-apply RRle_abs.
-apply Hex.
-rewrite <- (Rmult_1_r (Z2R (y + 1))).
-change (F2R (Float beta (y + 1) 0) <= bpow ey)%R.
-apply F2R_p1_le_bpow.
-exact Hy.
-unfold F2R. rewrite Rmult_1_r.
-apply Rle_lt_trans with (Rabs (Z2R y)).
-apply RRle_abs.
-apply Hey.
-apply neq_Z2R.
-now apply Rgt_not_eq.
-(* . *)
-intros Hy'.
-rewrite (Zle_antisym _ _ Hy' Hy).
-rewrite Zmult_0_r, 3!Zplus_0_r.
-apply Zle_refl.
-intros Hx'.
-rewrite (Zle_antisym _ _ Hx' Hx).
-rewrite Zmult_0_l, Zplus_0_r, 2!Zplus_0_l.
-apply Zle_refl.
-Qed.
-
-Theorem Zdigits_mult :
-  forall x y,
-  (Zdigits beta (x * y) <= Zdigits beta x + Zdigits beta y)%Z.
-Proof.
-intros x y.
-rewrite <- Zdigits_abs.
-rewrite <- (Zdigits_abs _ x).
-rewrite <- (Zdigits_abs _ y).
-apply Zle_trans with (Zdigits beta (Zabs x + Zabs y + Zabs x * Zabs y)).
-apply Zdigits_le.
-apply Zabs_pos.
-rewrite Zabs_Zmult.
-generalize (Zabs_pos x) (Zabs_pos y).
-omega.
-apply Zdigits_mult_strong ; apply Zabs_pos.
-Qed.
-
-Theorem Zdigits_mult_ge :
-  forall x y,
-  (x <> 0)%Z -> (y <> 0)%Z ->
-  (Zdigits beta x + Zdigits beta y - 1 <= Zdigits beta (x * y))%Z.
-Proof.
-intros x y Zx Zy.
-cut ((Zdigits beta x - 1) + (Zdigits beta y - 1) < Zdigits beta (x * y))%Z. omega.
-apply Zdigits_gt_Zpower.
-rewrite Zabs_Zmult.
-rewrite Zpower_exp.
-apply Zmult_le_compat.
-apply Zpower_le_Zdigits.
-apply Zlt_pred.
-apply Zpower_le_Zdigits.
-apply Zlt_pred.
-apply Zpower_ge_0.
-apply Zpower_ge_0.
-generalize (Zdigits_gt_0 beta x). omega.
-generalize (Zdigits_gt_0 beta y). omega.
-Qed.
-
-Theorem Zdigits_div_Zpower :
-  forall m e,
-  (0 <= m)%Z ->
-  (0 <= e <= Zdigits beta m)%Z ->
-  Zdigits beta (m / Zpower beta e) = (Zdigits beta m - e)%Z.
-Proof.
-intros m e Hm He.
-destruct (Zle_lt_or_eq 0 m Hm) as [Hm'|Hm'].
-(* *)
-destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He'].
-(* . *)
-unfold Zminus.
-rewrite <- ln_beta_F2R_Zdigits.
-2: now apply Zgt_not_eq.
-assert (Hp: (0 < Zpower beta e)%Z).
-apply lt_Z2R.
-rewrite Z2R_Zpower with (1 := proj1 He).
-apply bpow_gt_0.
-rewrite Zdigits_ln_beta.
-rewrite <- Zfloor_div with (1 := Zgt_not_eq _ _ Hp).
-rewrite Z2R_Zpower with (1 := proj1 He).
-unfold Rdiv.
-rewrite <- bpow_opp.
-change (Z2R m * bpow (-e))%R with (F2R (Float beta m (-e))).
-destruct (ln_beta beta (F2R (Float beta m (-e)))) as (e', E').
-simpl.
-specialize (E' (Rgt_not_eq _ _ (F2R_gt_0_compat beta (Float beta m (-e)) Hm'))).
-apply ln_beta_unique.
-rewrite Rabs_pos_eq in E'.
-2: now apply F2R_ge_0_compat.
-rewrite Rabs_pos_eq.
-split.
-assert (H': (0 <= e' - 1)%Z).
-(* .. *)
-cut (1 <= e')%Z. omega.
-apply bpow_lt_bpow with beta.
-apply Rle_lt_trans with (2 := proj2 E').
-simpl.
-rewrite <- (Rinv_r (bpow e)).
-rewrite <- bpow_opp.
-unfold F2R. simpl.
-apply Rmult_le_compat_r.
-apply bpow_ge_0.
-rewrite <- Z2R_Zpower with (1 := proj1 He).
-apply Z2R_le.
-rewrite <- Zabs_eq with (1 := Hm).
-now apply Zpower_le_Zdigits.
-apply Rgt_not_eq.
-apply bpow_gt_0.
-(* .. *)
-rewrite <- Z2R_Zpower with (1 := H').
-apply Z2R_le.
-apply Zfloor_lub.
-rewrite Z2R_Zpower with (1 := H').
-apply E'.
-apply Rle_lt_trans with (2 := proj2 E').
-apply Zfloor_lb.
-apply (Z2R_le 0).
-apply Zfloor_lub.
-now apply F2R_ge_0_compat.
-apply Zgt_not_eq.
-apply Zlt_le_trans with (beta^e / beta^e)%Z.
-rewrite Z_div_same_full.
-apply refl_equal.
-now apply Zgt_not_eq.
-apply Z_div_le.
-now apply Zlt_gt.
-rewrite <- Zabs_eq with (1 := Hm).
-now apply Zpower_le_Zdigits.
-(* . *)
-unfold Zminus.
-rewrite He', Zplus_opp_r.
-rewrite Zdiv_small.
-apply refl_equal.
-apply conj with (1 := Hm).
-pattern m at 1 ; rewrite <- Zabs_eq with (1 := Hm).
-apply Zpower_gt_Zdigits.
-apply Zle_refl.
-(* *)
-revert He.
-rewrite <- Hm'.
-intros (H1, H2).
-simpl.
-now rewrite (Zle_antisym _ _ H2 H1).
-Qed.
-
 End Fcalc_digits.
-
-Definition radix2 := Build_radix 2 (refl_equal _).
-
-Theorem Z_of_nat_S_digits2_Pnat :
-  forall m : positive,
-  Z_of_nat (S (digits2_Pnat m)) = Zdigits radix2 (Zpos m).
-Proof.
-intros m.
-rewrite Zdigits_ln_beta. 2: easy.
-apply sym_eq.
-apply ln_beta_unique.
-generalize (digits2_Pnat m) (digits2_Pnat_correct m).
-intros d H.
-simpl in H.
-replace (Z_of_nat (S d) - 1)%Z with (Z_of_nat d).
-rewrite <- Z2R_abs.
-rewrite <- 2!Z2R_Zpower_nat.
-split.
-now apply Z2R_le.
-now apply Z2R_lt.
-rewrite inj_S.
-apply Zpred_succ.
-Qed.
-
diff --git a/flocq/Calc/Fcalc_ops.v b/flocq/Calc/Fcalc_ops.v
index 7ece6832..e3b059d1 100644
--- a/flocq/Calc/Fcalc_ops.v
+++ b/flocq/Calc/Fcalc_ops.v
@@ -28,6 +28,8 @@ Variable beta : radix.
 
 Notation bpow e := (bpow beta e).
 
+Implicit Arguments Float [[beta]].
+
 Definition Falign (f1 f2 : float beta) :=
   let '(Float m1 e1) := f1 in
   let '(Float m2 e2) := f2 in
@@ -38,7 +40,7 @@ Definition Falign (f1 f2 : float beta) :=
 Theorem Falign_spec :
   forall f1 f2 : float beta,
   let '(m1, m2, e) := Falign f1 f2 in
-  F2R f1 = F2R (Float beta m1 e) /\ F2R f2 = F2R (Float beta m2 e).
+  F2R f1 = @F2R beta (Float m1 e) /\ F2R f2 = @F2R beta (Float m2 e).
 Proof.
 unfold Falign.
 intros (m1, e1) (m2, e2).
@@ -61,9 +63,9 @@ case (Zmin_spec e1 e2); intros (H1,H2); easy.
 case (Zmin_spec e1 e2); intros (H1,H2); easy.
 Qed.
 
-Definition Fopp (f1: float beta) :=
+Definition Fopp (f1 : float beta) : float beta :=
   let '(Float m1 e1) := f1 in
-  Float beta (-m1)%Z e1.
+  Float (-m1)%Z e1.
 
 Theorem F2R_opp :
   forall f1 : float beta,
@@ -72,9 +74,9 @@ intros (m1,e1).
 apply F2R_Zopp.
 Qed.
 
-Definition Fabs (f1: float beta) :=
+Definition Fabs (f1 : float beta) : float beta :=
   let '(Float m1 e1) := f1 in
-  Float beta (Zabs m1)%Z e1.
+  Float (Zabs m1)%Z e1.
 
 Theorem F2R_abs :
   forall f1 : float beta,
@@ -83,9 +85,9 @@ intros (m1,e1).
 apply F2R_Zabs.
 Qed.
 
-Definition Fplus (f1 f2 : float beta) :=
+Definition Fplus (f1 f2 : float beta) : float beta :=
   let '(m1, m2 ,e) := Falign f1 f2 in
-  Float beta (m1 + m2) e.
+  Float (m1 + m2) e.
 
 Theorem F2R_plus :
   forall f1 f2 : float beta,
@@ -104,7 +106,7 @@ Qed.
 
 Theorem Fplus_same_exp :
   forall m1 m2 e,
-  Fplus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 + m2) e.
+  Fplus (Float m1 e) (Float m2 e) = Float (m1 + m2) e.
 Proof.
 intros m1 m2 e.
 unfold Fplus.
@@ -136,17 +138,17 @@ Qed.
 
 Theorem Fminus_same_exp :
   forall m1 m2 e,
-  Fminus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 - m2) e.
+  Fminus (Float m1 e) (Float m2 e) = Float (m1 - m2) e.
 Proof.
 intros m1 m2 e.
 unfold Fminus.
 apply Fplus_same_exp.
 Qed.
 
-Definition Fmult (f1 f2 : float beta) :=
+Definition Fmult (f1 f2 : float beta) : float beta :=
   let '(Float m1 e1) := f1 in
   let '(Float m2 e2) := f2 in
-  Float beta (m1 * m2) (e1 + e2).
+  Float (m1 * m2) (e1 + e2).
 
 Theorem F2R_mult :
   forall f1 f2 : float beta,
diff --git a/flocq/Calc/Fcalc_sqrt.v b/flocq/Calc/Fcalc_sqrt.v
index 2ed32347..5f541d83 100644
--- a/flocq/Calc/Fcalc_sqrt.v
+++ b/flocq/Calc/Fcalc_sqrt.v
@@ -28,108 +28,6 @@ Require Import Fcalc_digits.
 
 Section Fcalc_sqrt.
 
-Fixpoint Zsqrt_aux (p : positive) : Z * Z :=
-  match p with
-  | xH => (1, 0)%Z
-  | xO xH => (1, 1)%Z
-  | xI xH => (1, 2)%Z
-  | xO (xO p) =>
-    let (q, r) := Zsqrt_aux p in
-    let r' := (4 * r)%Z in
-    let d := (r' - (4 * q + 1))%Z in
-    if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z
-  | xO (xI p) =>
-    let (q, r) := Zsqrt_aux p in
-    let r' := (4 * r + 2)%Z in
-    let d := (r' - (4 * q + 1))%Z in
-    if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z
-  | xI (xO p) =>
-    let (q, r) := Zsqrt_aux p in
-    let r' := (4 * r + 1)%Z in
-    let d := (r' - (4 * q + 1))%Z in
-    if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z
-  | xI (xI p) =>
-    let (q, r) := Zsqrt_aux p in
-    let r' := (4 * r + 3)%Z in
-    let d := (r' - (4 * q + 1))%Z in
-    if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z
-  end.
-
-Lemma Zsqrt_ind :
-  forall P : positive -> Prop,
-  P xH -> P (xO xH) -> P (xI xH) ->
-  ( forall p, P p -> P (xO (xO p)) /\ P (xO (xI p)) /\ P (xI (xO p)) /\ P (xI (xI p)) ) ->
-  forall p, P p.
-Proof.
-intros P H1 H2 H3 Hp.
-fix 1.
-intros [[p|p|]|[p|p|]|].
-refine (proj2 (proj2 (proj2 (Hp p _)))).
-apply Zsqrt_ind.
-refine (proj1 (proj2 (proj2 (Hp p _)))).
-apply Zsqrt_ind.
-exact H3.
-refine (proj1 (proj2 (Hp p _))).
-apply Zsqrt_ind.
-refine (proj1 (Hp p _)).
-apply Zsqrt_ind.
-exact H2.
-exact H1.
-Qed.
-
-Lemma Zsqrt_aux_correct :
-  forall p,
-  let (q, r) := Zsqrt_aux p in
-  Zpos p = (q * q + r)%Z /\ (0 <= r <= 2 * q)%Z.
-Proof.
-intros p.
-elim p using Zsqrt_ind ; clear p.
-now repeat split.
-now repeat split.
-now repeat split.
-intros p.
-Opaque Zmult. simpl. Transparent Zmult.
-destruct (Zsqrt_aux p) as (q, r).
-intros (Hq, Hr).
-change (Zpos p~0~0) with (4 * Zpos p)%Z.
-change (Zpos p~0~1) with (4 * Zpos p + 1)%Z.
-change (Zpos p~1~0) with (4 * Zpos p + 2)%Z.
-change (Zpos p~1~1) with (4 * Zpos p + 3)%Z.
-rewrite Hq. clear Hq.
-repeat split.
-generalize (Zlt_cases (4 * r - (4 * q + 1)) 0).
-case Zlt_bool ; ( split ; [ ring | omega ] ).
-generalize (Zlt_cases (4 * r + 2 - (4 * q + 1)) 0).
-case Zlt_bool ; ( split ; [ ring | omega ] ).
-generalize (Zlt_cases (4 * r + 1 - (4 * q + 1)) 0).
-case Zlt_bool ; ( split ; [ ring | omega ] ).
-generalize (Zlt_cases (4 * r + 3 - (4 * q + 1)) 0).
-case Zlt_bool ; ( split ; [ ring | omega ] ).
-Qed.
-
-(** Computes the integer square root and its remainder, but
-    without carrying a proof, contrarily to the operation of
-    the standard libary. *)
-
-Definition Zsqrt p :=
-  match p with
-  | Zpos p => Zsqrt_aux p
-  | _ => (0, 0)%Z
-  end.
-
-Theorem Zsqrt_correct :
-  forall x,
-  (0 <= x)%Z ->
-  let (q, r) := Zsqrt x in
-  x = (q * q + r)%Z /\ (0 <= r <= 2 * q)%Z.
-Proof.
-unfold Zsqrt.
-intros [|p|p] Hx.
-now repeat split.
-apply Zsqrt_aux_correct.
-now elim Hx.
-Qed.
-
 Variable beta : radix.
 Notation bpow e := (bpow beta e).
 
@@ -160,7 +58,7 @@ Definition Fsqrt_core prec m e :=
     | Zpos p => (m * Zpower_pos beta p)%Z
     | _ => m
     end in
-  let (q, r) := Zsqrt m' in
+  let (q, r) := Z.sqrtrem m' in
   let l :=
     if Zeq_bool r 0 then loc_Exact
     else loc_Inexact (if Zle_bool r q then Lt else Gt) in
@@ -236,8 +134,8 @@ now apply Zpower_gt_0.
 now elim He2.
 clearbody m'.
 destruct Hs as (Hs1, (Hs2, Hs3)).
-generalize (Zsqrt_correct m' (Zlt_le_weak _ _ Hs3)).
-destruct (Zsqrt m') as (q, r).
+generalize (Z.sqrtrem_spec m' (Zlt_le_weak _ _ Hs3)).
+destruct (Z.sqrtrem m') as (q, r).
 intros (Hq, Hr).
 rewrite <- Hs1. clear Hs1.
 split.