Update to Flocq 4.2.2

Author: xavierleroy

flocq/Calc/Bracket.v

@@ -626,7 +626,7 @@ Theorem inbetween_float_new_location :
   forall x m e l k,
   (0 < k)%Z ->
   inbetween_float m e x l ->
-  inbetween_float (Z.div m (Zpower beta k)) (e + k) x (new_location (Zpower beta k) (Zmod m (Zpower beta k)) l).
+  inbetween_float (Z.div m (Zpower beta k)) (e + k) x (new_location (Zpower beta k) (Z.modulo m (Zpower beta k)) l).
 Proof.
 intros x m e l k Hk Hx.
 unfold inbetween_float in *.
@@ -657,7 +657,7 @@ Qed.
 Theorem inbetween_float_new_location_single :
   forall x m e l,
   inbetween_float m e x l ->
-  inbetween_float (Z.div m beta) (e + 1) x (new_location beta (Zmod m beta) l).
+  inbetween_float (Z.div m beta) (e + 1) x (new_location beta (Z.modulo m beta) l).
 Proof.
 intros x m e l Hx.
 replace (radix_val beta) with (Zpower beta 1).

flocq/Calc/Round.v

@@ -609,7 +609,7 @@ Qed.
 Definition truncate_aux t k :=
   let '(m, e, l) := t in
   let p := Zpower beta k in
-  (Z.div m p, (e + k)%Z, new_location p (Zmod m p) l).
+  (Z.div m p, (e + k)%Z, new_location p (Z.modulo m p) l).
 
 Theorem truncate_aux_comp :
   forall t k1 k2,
@@ -1143,7 +1143,7 @@ Definition truncate_FIX t :=
   let k := (emin - e)%Z in
   if Zlt_bool 0 k then
     let p := Zpower beta k in
-    (Z.div m p, (e + k)%Z, new_location p (Zmod m p) l)
+    (Z.div m p, (e + k)%Z, new_location p (Z.modulo m p) l)
   else t.
 
 Theorem truncate_FIX_correct :

flocq/Core/Zaux.v

@@ -324,7 +324,7 @@ Section Div_Mod.
 
 Theorem Zmod_mod_mult :
   forall n a b, (0 < a)%Z -> (0 <= b)%Z ->
-  Zmod (Zmod n (a * b)) b = Zmod n b.
+  Z.modulo (Z.modulo n (a * b)) b = Z.modulo n b.
 Proof.
   intros n a b Ha Hb. destruct (Zle_lt_or_eq _ _ Hb) as [H'b|H'b].
   - rewrite (Z.mul_comm a b), Z.rem_mul_r, Z.add_mod, Z.mul_mod, Z.mod_same,
@@ -358,13 +358,13 @@ Qed.
 
 Theorem Zdiv_mod_mult :
   forall n a b, (0 <= a)%Z -> (0 <= b)%Z ->
-  (Z.div (Zmod n (a * b)) a) = Zmod (Z.div n a) b.
+  (Z.div (Z.modulo n (a * b)) a) = Z.modulo (Z.div n a) b.
 Proof.
 intros n a b Ha Hb.
 destruct (Zle_lt_or_eq _ _ Ha) as [Ha'|<-].
 - destruct (Zle_lt_or_eq _ _ Hb) as [Hb'|<-].
   + rewrite Z.rem_mul_r, Z.add_comm, Z.mul_comm, Z.div_add_l by lia.
-    rewrite (Zdiv_small (Zmod n a)).
+    rewrite (Zdiv_small (Z.modulo n a)).
     apply Z.add_0_r.
     now apply Z.mod_pos_bound.
   + now rewrite Z.mul_0_r, !Zmod_0_r, ?Zdiv_0_l.
@@ -852,10 +852,10 @@ Section faster_div.
 
 Lemma Zdiv_eucl_unique :
   forall a b,
-  Z.div_eucl a b = (Z.div a b, Zmod a b).
+  Z.div_eucl a b = (Z.div a b, Z.modulo a b).
 Proof.
 intros a b.
-unfold Z.div, Zmod.
+unfold Z.div, Z.modulo.
 now case Z.div_eucl.
 Qed.
 

flocq/IEEE754/Bits.v

@@ -77,7 +77,7 @@ Qed.
 Definition split_bits x :=
   let mm := Zpower 2 mw in
   let em := Zpower 2 ew in
-  (Zle_bool (mm * em) x, Zmod x mm, Zmod (Z.div x mm) em)%Z.
+  (Zle_bool (mm * em) x, Z.modulo x mm, Z.modulo (Z.div x mm) em)%Z.
 
 Theorem split_join_bits :
   forall s m e,

flocq/Prop/Double_rounding.v

@@ -91,7 +91,7 @@ assert (Hx2 : x - round beta fexp1 Zfloor x
 set (x'' := round beta fexp2 (Znearest choice2) x).
 assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (mag x))).
 apply Rle_trans with (/ 2 * ulp beta fexp2 x).
-now unfold x''; apply error_le_half_ulp...
+now unfold x''; apply error_le_half_ulp.
 rewrite ulp_neq_0;[now right|now apply Rgt_not_eq].
 assert (Pxx' : 0 <= x - x').
 { apply Rle_0_minus.
@@ -189,7 +189,7 @@ assert (Pxx' : 0 <= x - x').
   apply round_DN_pt.
   exact Vfexp1. }
 assert (x < bpow (mag x) - / 2 * bpow (fexp2 (mag x)));
-  [|apply round_round_lt_mid_further_place'; try assumption]...
+  [|apply round_round_lt_mid_further_place'; try assumption].
 2: rewrite ulp_neq_0;[assumption|now apply Rgt_not_eq].
 destruct (Req_dec x' 0) as [Zx'|Nzx'].
 - (* x' = 0 *)
@@ -348,7 +348,7 @@ set (x'' := round beta fexp2 (Znearest choice2) x).
 intros Hx1 Hx2.
 assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (mag x))).
   apply Rle_trans with (/2* ulp beta fexp2 x).
-  now unfold x''; apply error_le_half_ulp...
+  now unfold x''; apply error_le_half_ulp.
   rewrite ulp_neq_0;[now right|now apply Rgt_not_eq].
 assert (Px'x : 0 <= x' - x).
 { apply Rle_0_minus.

flocq/Prop/Round_odd.v

@@ -443,11 +443,11 @@ apply trans_eq with (negb (Z.even (Fnum ff))).
 rewrite K3; easy.
 apply sym_eq.
 generalize (DN_UP_parity_generic beta fexp).
-unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption...
-rewrite <- K1; apply Rnd_DN_pt_unique with (generic_format beta fexp) x; try easy...
-now apply round_DN_pt...
-rewrite <- L1; apply Rnd_UP_pt_unique with (generic_format beta fexp) x; try easy...
-now apply round_UP_pt...
+unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption.
+rewrite <- K1; apply Rnd_DN_pt_unique with (generic_format beta fexp) x; try easy.
+now apply round_DN_pt.
+rewrite <- L1; apply Rnd_UP_pt_unique with (generic_format beta fexp) x; try easy.
+now apply round_UP_pt.
 (* *)
 destruct H1' as (ff,(K1,(K2,K3))).
 destruct H2' as (gg,(L1,(L2,L3))).
@@ -457,11 +457,11 @@ apply trans_eq with (negb (Z.even (Fnum gg))).
 rewrite L3; easy.
 apply sym_eq.
 generalize (DN_UP_parity_generic beta fexp).
-unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption...
-rewrite <- L1; apply Rnd_DN_pt_unique with (generic_format beta fexp) x; try easy...
-now apply round_DN_pt...
-rewrite <- K1; apply Rnd_UP_pt_unique with (generic_format beta fexp) x; try easy...
-now apply round_UP_pt...
+unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption.
+rewrite <- L1; apply Rnd_DN_pt_unique with (generic_format beta fexp) x; try easy.
+now apply round_DN_pt.
+rewrite <- K1; apply Rnd_UP_pt_unique with (generic_format beta fexp) x; try easy.
+now apply round_UP_pt.
 apply Rnd_UP_pt_unique with format x; assumption.
 Qed.
 

flocq/Version.v

@@ -18,8 +18,8 @@ COPYING file for more details.
 *)
 
 (** Helper for detecting the version of Flocq *)
-Require Import BinNat.
-Require Import Ascii String.
+From Coq Require Import BinNat.
+From Coq Require Import Ascii String.
 
 Definition Flocq_version := Eval vm_compute in
   let fix parse s major minor :=
@@ -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
     | EmptyString => (major * 100 + minor)%N
     end in
-  parse "4.2.1"%string N0 N0.
+  parse "4.2.2"%string N0 N0.