From 2dd133f9178ae285d3939f29479b4acd9dad394d Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sat, 25 Sep 2021 11:47:59 +0200
Subject: Update the vendored Flocq library to version 3.4.2

For compatibility with the upcoming Coq 8.14.
---
 flocq/Core/Raux.v      |  4 ++--
 flocq/Core/Zaux.v      | 46 ++++++++++++++--------------------------------
 flocq/IEEE754/Binary.v |  4 ++--
 flocq/IEEE754/Bits.v   |  4 ++--
 4 files changed, 20 insertions(+), 38 deletions(-)

(limited to 'flocq')

diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v
index 455190dc..221d84d6 100644
--- a/flocq/Core/Raux.v
+++ b/flocq/Core/Raux.v
@@ -18,7 +18,7 @@ COPYING file for more details.
 *)
 
 (** * Missing definitions/lemmas *)
-Require Export Psatz.
+Require Import Psatz.
 Require Export Reals ZArith.
 Require Export Zaux.
 
@@ -1277,7 +1277,7 @@ Theorem Zfloor_div :
   Zfloor (IZR x / IZR y) = (x / y)%Z.
 Proof.
 intros x y Zy.
-generalize (Z_div_mod_eq_full x y Zy).
+generalize (Z.div_mod x y Zy).
 intros Hx.
 rewrite Hx at 1.
 assert (Zy': IZR y <> 0%R).
diff --git a/flocq/Core/Zaux.v b/flocq/Core/Zaux.v
index b40b0c4f..5ca3971f 100644
--- a/flocq/Core/Zaux.v
+++ b/flocq/Core/Zaux.v
@@ -327,18 +327,10 @@ Theorem Zmod_mod_mult :
   forall n a b, (0 < a)%Z -> (0 <= b)%Z ->
   Zmod (Zmod n (a * b)) b = Zmod n b.
 Proof.
-intros n a [|b|b] Ha Hb.
-now rewrite 2!Zmod_0_r.
-rewrite (Zmod_eq n (a * Zpos b)).
-rewrite Zmult_assoc.
-unfold Zminus.
-rewrite Zopp_mult_distr_l.
-apply Z_mod_plus.
-easy.
-apply Zmult_gt_0_compat.
-now apply Z.lt_gt.
-easy.
-now elim Hb.
+  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,
+      Z.mul_0_l, Z.mod_0_l, Z.add_0_r, !Z.mod_mod; lia.
+  - subst. now rewrite Z.mul_0_r, !Zmod_0_r.
 Qed.
 
 Theorem ZOmod_eq :
@@ -370,24 +362,14 @@ Theorem Zdiv_mod_mult :
   (Z.div (Zmod n (a * b)) a) = Zmod (Z.div n a) b.
 Proof.
 intros n a b Ha Hb.
-destruct (Zle_lt_or_eq _ _ Ha) as [Ha'|Ha'].
-destruct (Zle_lt_or_eq _ _ Hb) as [Hb'|Hb'].
-rewrite (Zmod_eq n (a * b)).
-rewrite (Zmult_comm a b) at 2.
-rewrite Zmult_assoc.
-unfold Zminus.
-rewrite Zopp_mult_distr_l.
-rewrite Z_div_plus by now apply Z.lt_gt.
-rewrite <- Zdiv_Zdiv by easy.
-apply sym_eq.
-apply Zmod_eq.
-now apply Z.lt_gt.
-now apply Zmult_gt_0_compat ; apply Z.lt_gt.
-rewrite <- Hb'.
-rewrite Zmult_0_r, 2!Zmod_0_r.
-apply Zdiv_0_l.
-rewrite <- Ha'.
-now rewrite 2!Zdiv_0_r, Zmod_0_l.
+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)).
+    apply Z.add_0_r.
+    now apply Z.mod_pos_bound.
+  + now rewrite Z.mul_0_r, !Zmod_0_r, ?Zdiv_0_l.
+- now rewrite Z.mul_0_l, !Zdiv_0_r, Zmod_0_l.
 Qed.
 
 Theorem ZOdiv_mod_mult :
@@ -856,7 +838,7 @@ Definition Zfast_div_eucl (a b : Z) :=
   | Z0 => (0, 0)%Z
   | Zpos a' =>
     match b with
-    | Z0 => (0, 0)%Z
+    | Z0 => (0, (match (1 mod 0) with | 0 => 0 | _ => a end))%Z
     | Zpos b' => Zpos_div_eucl_aux a' b'
     | Zneg b' =>
       let (q, r) := Zpos_div_eucl_aux a' b' in
@@ -868,7 +850,7 @@ Definition Zfast_div_eucl (a b : Z) :=
     end
   | Zneg a' =>
     match b with
-    | Z0 => (0, 0)%Z
+    | Z0 => (0, (match (1 mod 0) with | 0 => 0 | _ => a end))%Z
     | Zpos b' =>
       let (q, r) := Zpos_div_eucl_aux a' b' in
       match r with
diff --git a/flocq/IEEE754/Binary.v b/flocq/IEEE754/Binary.v
index 35d15cb3..4516f0a0 100644
--- a/flocq/IEEE754/Binary.v
+++ b/flocq/IEEE754/Binary.v
@@ -2472,9 +2472,9 @@ case f.
     now revert Hover; unfold B2R, F2R; simpl; rewrite Rmult_assoc, bpow_plus.
 Qed.
 
-(** This hypothesis is needed to implement Bfrexp
+(** This hypothesis is needed to implement [Bfrexp]
     (otherwise, we have emin > - prec
-     and Bfrexp cannot fit the mantissa in interval [0.5, 1)) *)
+     and [Bfrexp] cannot fit the mantissa in interval #[0.5, 1)#) *)
 Hypothesis Hemax : (3 <= emax)%Z.
 
 Definition Ffrexp_core_binary s m e :=
diff --git a/flocq/IEEE754/Bits.v b/flocq/IEEE754/Bits.v
index 68bc541a..3c19e31b 100644
--- a/flocq/IEEE754/Bits.v
+++ b/flocq/IEEE754/Bits.v
@@ -163,11 +163,11 @@ Proof.
 intros x Hx.
 unfold split_bits, join_bits.
 rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
-pattern x at 4 ; rewrite Z_div_mod_eq_full with x (2^mw)%Z.
+pattern x at 4 ; rewrite Z.div_mod with x (2^mw)%Z.
 apply (f_equal (fun v => (v + _)%Z)).
 rewrite Zmult_comm.
 apply f_equal.
-pattern (x / (2^mw))%Z at 2 ; rewrite Z_div_mod_eq_full with (x / (2^mw))%Z (2^ew)%Z.
+pattern (x / (2^mw))%Z at 2 ; rewrite Z.div_mod with (x / (2^mw))%Z (2^ew)%Z.
 apply (f_equal (fun v => (v + _)%Z)).
 replace (x / 2 ^ mw / 2 ^ ew)%Z with (if Zle_bool (2 ^ mw * 2 ^ ew) x then 1 else 0)%Z.
 case Zle_bool.
-- 
cgit