Merge PR coq#19801: make Zeq_bool an alias for Z.eqb, deprecate ZArit…

…h_base Reviewed-by: proux01 Co-authored-by: proux01 <[email protected]>
SkySkimmer · Jan 9, 2025 · f1fc014 · f1fc014
2 parents bc8831b + 9af8e67
commit f1fc014
Show file tree

Hide file tree

Showing 93 changed files with 562 additions and 480 deletions.
diff --git a/dev/ci/user-overlays/19801-andres-erbsen-Zeq_bool.sh b/dev/ci/user-overlays/19801-andres-erbsen-Zeq_bool.sh
@@ -0,0 +1,4 @@
+overlay flocq https://github.com/proux01/flocq coq_19801 19801
+overlay vst https://github.com/andres-erbsen/VST less-ZArith_base 19801
+overlay compcert https://github.com/andres-erbsen/CompCert less-ZArith_base 19801
+overlay coquelicot https://github.com/proux01/coquelicot coq_19801 19801
diff --git a/doc/changelog/11-standard-library/19801-less-ZArith_base.rst b/doc/changelog/11-standard-library/19801-less-ZArith_base.rst
@@ -0,0 +1,10 @@
+- **Deprecated:** module :g:`ZArith_Base`, module :g:`Ztac`, and :g:`Zeq_bool`.
+  Use :g:`ZArith` (or :g:`BinInt`), :g:`Lia`, and :g:`Z.eqb` instead.
+  Reducing use of the deprecated modules in stdlib **changed** the transitive
+  dependencies of several stdlib files; you may now need to ``Require`` or
+  ``Import`` :g:`ZArith` or :g:`Lia`.
+  The definition of :g:`Zeq_bool` was also **changed** to be an alias for
+  :g:`Z.eqb`; this is expected to simplify simultaneous compatibility with 8.20
+  and 9.0
+  (`#19801 <https://github.com/coq/coq/pull/19801>`_,
+  by Andres Erbsen).
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
@@ -53,7 +53,7 @@ let z_spec =
   ; zero = Mc.Z0
   ; unit = Mc.Zpos Mc.XH
   ; mult = Mc.Z.mul
-  ; eqb = Mc.zeq_bool }
+  ; eqb = Mc.Z.eqb }
 
 let q_spec =
   { bigint_to_number = (fun x -> {Mc.qnum = Ml2C.bigint x; Mc.qden = Mc.XH})
@@ -677,7 +677,7 @@ let rec term_to_z_expr = function
 
 let term_to_z_pol e =
   Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.Z.add Mc.Z.mul Mc.Z.sub Mc.Z.opp
-    Mc.zeq_bool (term_to_z_expr e)
+    Mc.Z.eqb (term_to_z_expr e)
 
 let z_cert_of_pos pos =
   let s, pos = scale_certificate pos in

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
@@ -1509,7 +1509,7 @@ let zz_domain_spec =
     ; undump_coeff = parse_z
     ; proof_typ = Lazy.force rocq_proofTerm
     ; dump_proof = dump_proof_term
-    ; coeff_eq = Mc.zeq_bool }
+    ; coeff_eq = Mc.Z.eqb }
 
 let qq_domain_spec =
   lazy

diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
@@ -292,6 +292,20 @@ module Coq_Pos =
     | Gt -> p
     | _ -> p'
 
+  (** val eqb : positive -> positive -> bool **)
+
+  let rec eqb p q0 =
+    match p with
+    | XI p2 -> (match q0 with
+                | XI q1 -> eqb p2 q1
+                | _ -> false)
+    | XO p2 -> (match q0 with
+                | XO q1 -> eqb p2 q1
+                | _ -> false)
+    | XH -> (match q0 with
+             | XH -> true
+             | _ -> false)
+
   (** val leb : positive -> positive -> bool **)
 
   let leb x y =
@@ -486,6 +500,20 @@ module Z =
     | Gt -> true
     | _ -> false
 
+  (** val eqb : z -> z -> bool **)
+
+  let eqb x y =
+    match x with
+    | Z0 -> (match y with
+             | Z0 -> true
+             | _ -> false)
+    | Zpos p -> (match y with
+                 | Zpos q0 -> Coq_Pos.eqb p q0
+                 | _ -> false)
+    | Zneg p -> (match y with
+                 | Zneg q0 -> Coq_Pos.eqb p q0
+                 | _ -> false)
+
   (** val max : z -> z -> z **)
 
   let max n0 m =
@@ -581,13 +609,6 @@ module Z =
        | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0))
  end
 
-(** val zeq_bool : z -> z -> bool **)
-
-let zeq_bool x y =
-  match Z.compare x y with
-  | Eq -> true
-  | _ -> false
-
 type 'c pExpr =
 | PEc of 'c
 | PEX of positive
@@ -2045,7 +2066,7 @@ type q = { qnum : z; qden : positive }
 (** val qeq_bool : q -> q -> bool **)
 
 let qeq_bool x y =
-  zeq_bool (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
+  Z.eqb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
 
 (** val qle_bool : q -> q -> bool **)
 
@@ -2153,12 +2174,12 @@ type zWitness = z psatz
 (** val zWeakChecker : z nFormula list -> z psatz -> bool **)
 
 let zWeakChecker =
-  check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb
+  check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb
 
 (** val psub1 : z pol -> z pol -> z pol **)
 
 let psub1 =
-  psub0 Z0 Z.add Z.sub Z.opp zeq_bool
+  psub0 Z0 Z.add Z.sub Z.opp Z.eqb
 
 (** val popp1 : z pol -> z pol **)
 
@@ -2168,22 +2189,22 @@ let popp1 =
 (** val padd1 : z pol -> z pol -> z pol **)
 
 let padd1 =
-  padd0 Z0 Z.add zeq_bool
+  padd0 Z0 Z.add Z.eqb
 
 (** val normZ : z pExpr -> z pol **)
 
 let normZ =
-  norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp zeq_bool
+  norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp Z.eqb
 
 (** val zunsat : z nFormula -> bool **)
 
 let zunsat =
-  check_inconsistent Z0 zeq_bool Z.leb
+  check_inconsistent Z0 Z.eqb Z.leb
 
 (** val zdeduce : z nFormula -> z nFormula -> z nFormula option **)
 
 let zdeduce =
-  nformula_plus_nformula Z0 Z.add zeq_bool
+  nformula_plus_nformula Z0 Z.add Z.eqb
 
 (** val xnnormalise : z formula -> z nFormula **)
 
@@ -2300,7 +2321,7 @@ let genCuttingPlane = function
    | Equal ->
      let g,c = zgcd_pol e in
      if (&&) (Z.gtb g Z0)
-          ((&&) (negb (zeq_bool c Z0)) (negb (zeq_bool (Z.gcd g c) g)))
+          ((&&) (negb (Z.eqb c Z0)) (negb (Z.eqb (Z.gcd g c) g)))
      then None
      else Some ((makeCuttingPlane e),Equal)
    | NonEqual -> Some ((e,Z0),op)
@@ -2323,7 +2344,7 @@ let is_pol_Z0 = function
 (** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **)
 
 let eval_Psatz0 =
-  eval_Psatz Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb
+  eval_Psatz Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb
 
 (** val valid_cut_sign : op1 -> bool **)
 

diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
@@ -143,6 +143,8 @@ module Z :
 
   val compare : z -> z -> comparison
 
+  val eqb : z -> z -> bool
+
   val leb : z -> z -> bool
 
   val ltb : z -> z -> bool
@@ -168,8 +170,6 @@ module Z :
   val gcd : z -> z -> z
  end
 
-val zeq_bool : z -> z -> bool
-
 type 'c pExpr =
 | PEc of 'c
 | PEX of positive

diff --git a/stdlib/test-suite/bugs/bug_4187.v b/stdlib/test-suite/bugs/bug_4187.v
@@ -7,6 +7,8 @@ Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
 From Stdlib Require Import List.
 From Stdlib Require Import Setoid.
+From Stdlib Require Import BinNat.
+From Stdlib Require Import Sumbool.
 Global Set Implicit Arguments.
 Global Generalizable All Variables.
 Coercion is_true : bool >-> Sortclass.

diff --git a/stdlib/test-suite/bugs/bug_5359.v b/stdlib/test-suite/bugs/bug_5359.v
@@ -1,4 +1,6 @@
 From Stdlib Require Import Nsatz.
+From Stdlib Require Import BinNat.
+
 Goal False.
 
   (* the first (succeeding) goal was reached by clearing one hypothesis in the second goal which overflows 6GB of stack space *)

diff --git a/stdlib/test-suite/output/Fixpoint.v b/stdlib/test-suite/output/Fixpoint.v
@@ -16,7 +16,7 @@ Check
     end
   in f 0.
 
-From Stdlib Require Import ZArith_base Lia.
+From Stdlib Require Import BinInt Lia.
 Open Scope Z_scope.
 
 Inductive even: Z -> Prop :=

diff --git a/stdlib/test-suite/output/Intuition.v b/stdlib/test-suite/output/Intuition.v
@@ -1,4 +1,4 @@
-From Stdlib Require Import ZArith_base.
+From Stdlib Require Import BinInt.
 Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z.
 intros; intuition.
 Show.

diff --git a/stdlib/test-suite/output/MExtraction.out b/stdlib/test-suite/output/MExtraction.out
@@ -206,6 +206,20 @@ module Pos =
   let compare =
     compare_cont Eq
 
+  (** val eqb : positive -> positive -> bool **)
+
+  let rec eqb p q0 =
+    match p with
+    | XI p2 -> (match q0 with
+                | XI q1 -> eqb p2 q1
+                | _ -> false)
+    | XO p2 -> (match q0 with
+                | XO q1 -> eqb p2 q1
+                | _ -> false)
+    | XH -> (match q0 with
+             | XH -> true
+             | _ -> false)
+
   (** val of_succ_nat : nat -> positive **)
 
   let rec of_succ_nat = function
@@ -560,6 +574,20 @@ module Z =
     | Lt -> true
     | _ -> false
 
+  (** val eqb : z -> z -> bool **)
+
+  let eqb x y =
+    match x with
+    | Z0 -> (match y with
+             | Z0 -> true
+             | _ -> false)
+    | Zpos p -> (match y with
+                 | Zpos q0 -> Pos.eqb p q0
+                 | _ -> false)
+    | Zneg p -> (match y with
+                 | Zneg q0 -> Pos.eqb p q0
+                 | _ -> false)
+
   (** val max : z -> z -> z **)
 
   let max n0 m =
@@ -662,13 +690,6 @@ module Z =
        | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0))
  end
 
-(** val zeq_bool : z -> z -> bool **)
-
-let zeq_bool x y =
-  match Z.compare x y with
-  | Eq -> true
-  | _ -> false
-
 type 'c pExpr =
 | PEc of 'c
 | PEX of positive
@@ -2126,7 +2147,7 @@ type q = { qnum : z; qden : positive }
 (** val qeq_bool : q -> q -> bool **)
 
 let qeq_bool x y =
-  zeq_bool (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
+  Z.eqb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
 
 (** val qle_bool : q -> q -> bool **)
 
@@ -2234,12 +2255,12 @@ type zWitness = z psatz
 (** val zWeakChecker : z nFormula list -> z psatz -> bool **)
 
 let zWeakChecker =
-  check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb
+  check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb
 
 (** val psub1 : z pol -> z pol -> z pol **)
 
 let psub1 =
-  psub0 Z0 Z.add Z.sub Z.opp zeq_bool
+  psub0 Z0 Z.add Z.sub Z.opp Z.eqb
 
 (** val popp1 : z pol -> z pol **)
 
@@ -2249,22 +2270,22 @@ let popp1 =
 (** val padd1 : z pol -> z pol -> z pol **)
 
 let padd1 =
-  padd0 Z0 Z.add zeq_bool
+  padd0 Z0 Z.add Z.eqb
 
 (** val normZ : z pExpr -> z pol **)
 
 let normZ =
-  norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp zeq_bool
+  norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp Z.eqb
 
 (** val zunsat : z nFormula -> bool **)
 
 let zunsat =
-  check_inconsistent Z0 zeq_bool Z.leb
+  check_inconsistent Z0 Z.eqb Z.leb
 
 (** val zdeduce : z nFormula -> z nFormula -> z nFormula option **)
 
 let zdeduce =
-  nformula_plus_nformula Z0 Z.add zeq_bool
+  nformula_plus_nformula Z0 Z.add Z.eqb
 
 (** val xnnormalise : z formula -> z nFormula **)
 
@@ -2381,7 +2402,7 @@ let genCuttingPlane = function
    | Equal ->
      let g,c = zgcd_pol e in
      if (&&) (Z.gtb g Z0)
-          ((&&) (negb (zeq_bool c Z0)) (negb (zeq_bool (Z.gcd g c) g)))
+          ((&&) (negb (Z.eqb c Z0)) (negb (Z.eqb (Z.gcd g c) g)))
      then None
      else Some ((makeCuttingPlane e),Equal)
    | NonEqual -> Some ((e,Z0),op)
@@ -2404,7 +2425,7 @@ let is_pol_Z0 = function
 (** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **)
 
 let eval_Psatz0 =
-  eval_Psatz Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb
+  eval_Psatz Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb
 
 (** val valid_cut_sign : op1 -> bool **)
 

diff --git a/stdlib/test-suite/output/MExtraction.v b/stdlib/test-suite/output/MExtraction.v
@@ -61,7 +61,7 @@ Recursive Extraction
            ZMicromega.cnfZ  ZMicromega.Zeval_const QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)
            denorm QArith_base.Qpower vm_add
-   normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+   normZ normQ normQ Z.to_N N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
 
 (* Local Variables: *)
 (* coding: utf-8 *)

diff --git a/stdlib/test-suite/success/Nsatz.v b/stdlib/test-suite/success/Nsatz.v
@@ -1,5 +1,6 @@
 
 (* compile en user    3m39.915s sur cachalot *)
+From Stdlib Require Import BinNat.
 From Stdlib Require Import Nsatz.
 From Stdlib Require List.
 Import List.ListNotations.

diff --git a/stdlib/theories/Floats/FloatLemmas.v b/stdlib/theories/Floats/FloatLemmas.v
@@ -55,8 +55,7 @@ Proof.
   rewrite Bool.andb_true_iff.
   intro H'.
   destruct H' as (H1,H2).
-  rewrite Z.eqb_compare in H1.
-  apply Zeq_bool_eq in H1.
+  apply Z.eqb_eq in H1.
   apply Z.max_case_strong.
   1:apply Z.min_case_strong.
   - reflexivity.

diff --git a/stdlib/theories/Lists/ListTactics.v b/stdlib/theories/Lists/ListTactics.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import BinPos.
+Require Import BinPosDef.
 Require Import List.
 
 Ltac list_fold_right fcons fnil l :=

diff --git a/stdlib/theories/Numbers/DecimalQ.v b/stdlib/theories/Numbers/DecimalQ.v
@@ -14,6 +14,7 @@
     are bijections. *)
 
 Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith.
+Import PeanoNat.
 
 Lemma of_IQmake_to_decimal num den :
   match IQmake_to_decimal num den with

diff --git a/stdlib/theories/Numbers/DecimalR.v b/stdlib/theories/Numbers/DecimalR.v
@@ -14,6 +14,7 @@
     are bijections. *)
 
 Require Import Decimal DecimalFacts DecimalPos DecimalZ DecimalQ Rdefinitions.
+Require Import PeanoNat.
 
 Lemma of_IQmake_to_decimal num den :
   match IQmake_to_decimal num den with