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 ++++++++++++++--------------------------------
 2 files changed, 16 insertions(+), 34 deletions(-)

(limited to 'flocq/Core')

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
-- 
cgit