split Zdivisibility from Znumtheory, deprecate most of Znumtheory

.nix/rocq-overlays/stdlib-subcomponents/default.nix

@@ -26,9 +26,9 @@ let
     "lia" = [ "arith" "narith" ];
     "zarith" = [ "lia" ];
     "qarith-base" = [ "ring" ];
-    "field" = [ "qarith-base" "zarith" ];
-    "lqa" = [ "field" ];
-    "qarith" = [ "field" ];
+    "field" = [ "zarith" ];
+    "lqa" = [ "field" "qarith-base" ];
+    "qarith" = [ "lqa" ];
     "nsatz" = [ "zarith" "qarith-base" ];
     "classical-logic" = [ "arith" ];
     "sets" = [ "classical-logic" ];
@@ -40,7 +40,7 @@ let
     "primitive-floats" = [ "primitive-int" ];
     "primitive-array" = [ "primitive-int" ];
     "primitive-string" = [ "primitive-int" "orders-ex" ];
-    "reals" = [ "nsatz" "lqa" "qarith" "classical-logic" "vectors" ];
+    "reals" = [ "nsatz" "qarith" "classical-logic" "vectors" ];
     "fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
     "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
     "funind" = [ "arith-base" ];

doc/changelog/01-changed/136-less-znumtheory.rst

@@ -0,0 +1,20 @@
+- in `ZArith,v` and dependencies
+
+  + Reducing reliance on :g:`Znumtheory` within stdlib changed the internal
+    dependencies between files, code relying on files being transitively
+    required in stdlib may need to now explicitly ``Require``
+    `Znumtheory`,
+    `BinInt`,
+    `BinList`,
+    `BinNat`,
+    `BinNums`,
+    `BinPos`,
+    `Setoid`,
+    `Tauto`,
+    `Zhints`,
+    `Zpow_def`,
+    `Zpow_facts`,
+    or `Zbool`
+    (`#136 <https://github.com/coq/stdlib/pull/136>`_,
+    by Andres Erbsen).
+

doc/changelog/02-added/136-less-znumtheory.rst

@@ -0,0 +1,7 @@
+- `Zdivisibility.v`
+
+  + Refactored theory of integer divisibility including primality and
+    coprimality. This file is intended to replace `Znumtheory`
+    (`#136 <https://github.com/coq/stdlib/pull/136>`_,
+    by Andres Erbsen).
+

doc/changelog/05-deprecated/136-less-znumtheory.rst

@@ -0,0 +1,7 @@
+- in `Znumtheory.v`
+
+  + Deprecated most definitions in favor of `Zdivisibility.v` or appropriate
+    established files
+    (`#136 <https://github.com/coq/stdlib/pull/136>`_,
+    by Andres Erbsen).
+

doc/stdlib/depends.dot

@@ -15,12 +15,11 @@ digraph stdlib_deps {
 	strings -> arith;
 	reals -> qarith;
 	reals -> vectors;
-	reals -> lqa;
 	reals -> "classical-logic";
 	reals -> nsatz;
 	"arith-base" -> structures;
 	zarith -> lia;
-	qarith -> field;
+	qarith -> lqa;
 	positive -> "arith-base";
 	narith -> ring;
 	ring -> lists;
@@ -49,8 +48,8 @@ digraph stdlib_deps {
 	"primitive-string" -> "orders-ex";
 	vectors -> lists;
 	field -> zarith;
-	field -> "qarith-base";
 	lqa -> field;
+	lqa -> "qarith-base";
 	"qarith-base" -> ring;
 	"classical-logic" -> arith;
 	nsatz -> zarith;

doc/stdlib/index-list.html.template

@@ -262,6 +262,7 @@ through the <tt>From Stdlib Require Import</tt> command.</p>
     theories/ZArith/Zpow_def.v
     theories/ZArith/Zdiv.v
     theories/ZArith/Znumtheory.v
+    theories/ZArith/Zdivisibility.v
   </dd>
 
   <dt> <a name="arith"></a><b>Arith</b>:

theories/All/All.v

@@ -107,6 +107,7 @@ From Stdlib Require Export ZArith.Zbitwise.
 From Stdlib Require Export ZArith.Zbool.
 From Stdlib Require Export ZArith.Zcompare.
 From Stdlib Require Export ZArith.Zcomplements.
+From Stdlib Require Export ZArith.Zdivisibility.
 From Stdlib Require Export ZArith.Zdiv.
 From Stdlib Require Export ZArith.Zdiv_facts.
 From Stdlib Require Export ZArith.ZModOffset.

theories/Make.field

@@ -1,12 +1,5 @@
-QArith/_Field/Qfield.v
-QArith/_Field/Qround.v
-QArith/_Field/Qring.v
-QArith/_Field/Qpower.v
-QArith/_Field/Qcanon.v
 setoid_ring/_Field/Field_theory.v
 setoid_ring/_Field/Field_tac.v
-setoid_ring/_Field/Rings_Q.v
 setoid_ring/_Field/Field.v
 
--Q QArith/_Field Stdlib.QArith
 -Q setoid_ring/_Field Stdlib.setoid_ring

theories/Make.lqa

@@ -1,5 +1,10 @@
 micromega/_Lqa/QMicromega.v
 micromega/_Lqa/Lqa.v
 micromega/_Lqa/DeclConstant.v
+QArith/_Lqa/Qfield.v
+QArith/_Lqa/Qring.v
+setoid_ring/_QArith/Rings_Q.v
 
 -Q micromega/_Lqa Stdlib.micromega
+-Q QArith/_Lqa Stdlib.QArith
+-Q setoid_ring/_QArith Stdlib.setoid_ring

theories/Make.qarith

@@ -1,6 +1,9 @@
 QArith/_All/Qcabs.v
+QArith/_All/Qround.v
 QArith/_All/Qabs.v
 QArith/_All/QArith.v
+QArith/_All/Qpower.v
+QArith/_All/Qcanon.v
 Numbers/_QArith/DecimalQ.v
 Numbers/_QArith/HexadecimalQ.v
 

theories/Make.ring

@@ -1,5 +1,4 @@
 ZArith/_Ring/Zpow_def.v
-ZArith/_Ring/Znumtheory.v
 ZArith/_Ring/Zcomplements.v
 ZArith/_Ring/Zdiv.v
 setoid_ring/_Ring/Ncring_polynom.v

theories/Make.zarith

@@ -8,6 +8,8 @@ ZArith/_All/Zwf.v
 ZArith/_All/ZArith.v
 ZArith/_All/Zbitwise.v
 ZArith/_All/ZModOffset.v
+ZArith/_All/Zdivisibility.v
+ZArith/_All/Znumtheory.v
 Numbers/Integer/Binary/ZBinary.v
 Numbers/Integer/NatPairs/ZNatPairs.v
 Numbers/_ZArith/DecimalN.v

theories/Numbers/Cyclic/Int63/Sint63.v

@@ -9,7 +9,7 @@
 (************************************************************************)
 
 From Stdlib Require Import ZArith.
-Import Znumtheory.
+Local Open Scope Z_scope.
 From Stdlib Require Export Uint63 Sint63Axioms.
 From Stdlib Require Import Lia.
 

theories/Numbers/Cyclic/Int63/Uint63.v

@@ -543,10 +543,7 @@ Lemma eqm_sub x y : x ≡ y → x - y ≡ 0.
 Proof. intros h; unfold eqm; rewrite Zminus_mod, h, Z.sub_diag; reflexivity. Qed.
 
 Lemma eqmE x y : x ≡ y → ∃ k, x - y = k * wB.
-Proof.
-  intros h.
-  exact (Zmod_divide (x - y) wB (λ e, let 'eq_refl := e in I) (eqm_sub _ _ h)).
-Qed.
+Proof. intros h%Z.cong_iff_ex; trivial. Qed.
 
 Lemma eqm_subE x y : x ≡ y ↔ x - y ≡ 0.
 Proof.
@@ -963,11 +960,13 @@ Proof.
        assert (F2: 0 < wB) by (apply refl_equal).
        assert (F3: φ (bit x 0 + bit y 0) mod 2 = φ (bit x 0 || bit y 0) mod 2). {
          apply trans_equal with ((φ ((x>>1 + y>>1) << 1) + φ (bit x 0 + bit y 0)) mod 2).
-         - rewrite lsl_spec, Zplus_mod, <-Zmod_div_mod; auto with zarith.
+         - rewrite lsl_spec, Zplus_mod, Z.mod_mod_divide; auto with zarith.
            rewrite Z.pow_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith.
-         - rewrite (Zmod_div_mod 2 wB), <-add_spec, Heq; auto with zarith.
-           rewrite add_spec, <-Zmod_div_mod; auto with zarith.
-           rewrite lsl_spec, Zplus_mod, <-Zmod_div_mod; auto with zarith.
+         - assert (forall a, a mod 2 = (a mod wB) mod 2) as ->.
+           { intros. rewrite Z.mod_mod_divide; trivial. }
+           rewrite <-add_spec, Heq; auto with zarith.
+           rewrite add_spec, Z.mod_mod_divide; auto with zarith.
+           rewrite lsl_spec, Zplus_mod, Z.mod_mod_divide; auto with zarith.
            rewrite Z.pow_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith.
        }
        generalize F3; do 2 case bit; try discriminate; auto.

theories/QArith/Qabs.v

@@ -88,7 +88,7 @@ intros [xn xd] [yn yd].
 unfold Qplus.
 unfold Qle.
 simpl.
-apply Z.mul_le_mono_nonneg_r;auto with *.
+apply Z.mul_le_mono_nonneg_r; auto using Pos2Z.is_nonneg.
 change (Zpos yd)%Z with (Z.abs (Zpos yd)).
 change (Zpos xd)%Z with (Z.abs (Zpos xd)).
 repeat rewrite <- Z.abs_mul.

theories/QArith/Qcanon.v

@@ -10,7 +10,6 @@
 
 From Stdlib Require Import Field.
 From Stdlib Require Import QArith_base Qreduction.
-From Stdlib Require Import Znumtheory.
 From Stdlib Require Import Eqdep_dec.
 
 (** [Qc] : A canonical representation of rational numbers.

theories/QArith/Qpower.v

@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-From Stdlib Require Import Zpow_facts Qfield Qreduction.
+From Stdlib Require Import Qfield Qreduction.
 
 (** * Properties of Qpower_positive *)
 
@@ -438,7 +438,7 @@ induction n using Pos.peano_ind.
   ring.
 - rewrite Pos2Z.inj_succ.
   unfold Z.succ.
-  rewrite Zpower_exp; auto with *; try discriminate.
+  rewrite Z.pow_add_r; auto with *; try discriminate.
   rewrite Qpower_plus' by discriminate.
   rewrite <- IHn by discriminate.
   replace (a^Zpos n*a^1)%Z with (a^Zpos n*a)%Z by ring.
@@ -468,8 +468,8 @@ Proof.
   intros q.
   destruct (Qarchimedean q) as [pexp Hpexp].
   exists (Pos.size pexp).
-  pose proof Pos.size_gt pexp as H1.
-  unfold Qlt in *. cbn in *; Zify.zify.
-  apply (Z.mul_lt_mono_pos_r (QDen q)) in H1; [|assumption].
-  apply (Z.lt_trans _ _ _ Hpexp H1).
+  cbv [Qlt] in *; cbn [Qnum Qden] in *.
+  etransitivity; [exact Hpexp|].
+  rewrite <-Z.mul_lt_mono_pos_r by reflexivity.
+  apply Pos.size_gt.
 Qed.

theories/QArith/Qreduction.v

@@ -11,11 +11,12 @@
 (** Normalisation functions for rational numbers. *)
 
 From Stdlib Require Export QArith_base.
-From Stdlib Require Import Znumtheory.
 
 Notation Z2P := Z.to_pos (only parsing).
 Notation Z2P_correct := Z2Pos.id (only parsing).
 
+Local Coercion Z.pos : positive >-> Z.
+
 (** Simplification of fractions using [Z.gcd].
   This version can compute within Coq. *)
 
@@ -40,60 +41,37 @@ Proof.
     Close Scope Z_scope.
 Qed.
 
+Lemma Qeq_Qred_iff q q' : Qred q == Qred q' <-> q == q'.
+Proof. rewrite 2Qred_correct; reflexivity. Qed.
+
+Lemma gcd_Qred q : Z.gcd (Qnum (Qred q)) (Qden (Qred q)) = 1%Z.
+Proof.
+  case q as [a b]; cbv [Qred Qnum Qden].
+  pose proof Z.ggcd_correct_divisors a b as Hg.
+  pose proof Z.ggcd_gcd a b as Hgg.
+  destruct (Z.ggcd a b) as (g&a'&b'); cbn [fst snd] in *; subst g; case Hg as [Ha Hb].
+  assert (Z.gcd a b <> 0)%Z by (rewrite Z.gcd_eq_0; intros []; discriminate).
+
+  erewrite <-(Z.gcd_div_gcd a b); trivial; trivial.
+  rewrite Ha, Z.mul_comm, Z.div_mul at 1; trivial.
+  rewrite Hb, Z.mul_comm, Z.div_mul at 1; trivial.
+  rewrite Z2Pos.id; trivial.
+  eapply Z.mul_pos_cancel_l; try rewrite <-Hb; trivial using Pos2Z.is_pos.
+  pose proof Z.gcd_nonneg a b as HH; apply Z.le_lteq in HH; intuition congruence.
+Qed.
+
 Lemma Qred_complete : forall p q,  p==q -> Qred p = Qred q.
 Proof.
-  intros (a,b) (c,d).
-  unfold Qred, Qeq in *; simpl in *.
-  Open Scope Z_scope.
-  intros H.
-  generalize (Z.ggcd_gcd a (Zpos b)) (Zgcd_is_gcd a (Zpos b))
-    (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).
-  destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)).
-  simpl. intros <- Hg1 Hg2 (Hg3,Hg4).
-  assert (Hg0 : g <> 0) by (intro; now subst g).
-  generalize (Z.ggcd_gcd c (Zpos d)) (Zgcd_is_gcd c (Zpos d))
-    (Z.gcd_nonneg c (Zpos d)) (Z.ggcd_correct_divisors c (Zpos d)).
-  destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)).
-  simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4).
-  assert (Hg'0 : g' <> 0) by (intro; now subst g').
-
-  elim (rel_prime_cross_prod aa bb cc dd).
-  - congruence.
-  - (*rel_prime*)
-    constructor.
-    * exists aa; auto using Z.mul_1_r.
-    * exists bb; auto using Z.mul_1_r.
-    * intros x Ha Hb.
-      destruct Hg1 as (Hg11,Hg12,Hg13).
-      destruct (Hg13 (g*x)) as (x',Hx).
-      { rewrite Hg3.
-        destruct Ha as (xa,Hxa); exists xa; rewrite Hxa; ring. }
-      { rewrite Hg4.
-        destruct Hb as (xb,Hxb); exists xb; rewrite Hxb; ring. }
-      exists x'.
-      apply Z.mul_reg_l with g; auto. rewrite Hx at 1; ring.
-  - (* rel_prime *)
-    constructor.
-    * exists cc; auto using Z.mul_1_r.
-    * exists dd; auto using Z.mul_1_r.
-    * intros x Hc Hd.
-      inversion Hg'1 as (Hg'11,Hg'12,Hg'13).
-      destruct (Hg'13 (g'*x)) as (x',Hx).
-      { rewrite Hg'3.
-        destruct Hc as (xc,Hxc); exists xc; rewrite Hxc; ring. }
-      { rewrite Hg'4.
-        destruct Hd as (xd,Hxd); exists xd; rewrite Hxd; ring. }
-      exists x'.
-      apply Z.mul_reg_l with g'; auto. rewrite Hx at 1; ring.
-  - apply Z.lt_gt.
-    rewrite <- (Z.mul_pos_cancel_l g); [ now rewrite <- Hg4 |  apply Z.le_neq; intuition ].
-  - apply Z.lt_gt.
-    rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | apply Z.le_neq; intuition ].
-  - apply Z.mul_reg_l with (g*g').
-    * rewrite Z.mul_eq_0. now destruct 1.
-    * rewrite Z.mul_shuffle1, <- Hg3, <- Hg'4.
-      now rewrite Z.mul_shuffle1, <- Hg'3, <- Hg4, H, Z.mul_comm.
-  Close Scope Z_scope.
+  setoid_rewrite <-Qeq_Qred_iff.
+  intros a b; specialize (gcd_Qred a); specialize (gcd_Qred b).
+  destruct (Qred a) as [p q]; destruct (Qred b) as [p' q'].
+  cbv [Qred Qeq Qnum Qden]; intros H H' Hcross.
+
+  pose proof Z.gauss q' p' q ltac:(exists p; ring [Hcross]) ltac:(rewrite Z.gcd_comm; trivial).
+  pose proof Z.gauss q p q' ltac:(exists p'; ring [Hcross]) ltac:(rewrite Z.gcd_comm; trivial).
+  pose proof Pos2Z.is_nonneg.
+  pose proof Z.divide_antisym_nonneg q q' ltac:(trivial) ltac:(trivial) ltac:(trivial) ltac:(trivial) as q'q.
+  injection q'q as <-; f_equal. eapply Z.mul_cancel_r with (p:=q); trivial. inversion 1.
 Qed.
 
 Lemma Qred_eq_iff q q' : Qred q = Qred q' <-> q == q'.

theories/QArith/Qround.v

@@ -9,7 +9,7 @@
 (************************************************************************)
 
 From Stdlib Require Import QArith_base.
-From Stdlib Require Import Zhints Zdiv.
+From Stdlib Require Import Zdiv.
 
 (************)
 
@@ -78,7 +78,7 @@ replace (n / Zpos d * Zpos d + Zpos d)%Z with
   ((Zpos d * (n / Zpos d) + n mod Zpos  d) + Zpos  d - n mod Zpos d)%Z by ring.
 rewrite <- Z_div_mod_eq_full.
 rewrite <- Z.lt_add_lt_sub_r.
-destruct (Z_mod_lt n (Zpos d)); auto with *.
+apply Z.add_lt_mono_l, Z.mod_pos_bound, eq_refl.
 Qed.
 
 #[global]
@@ -92,7 +92,7 @@ replace (- Qfloor (- x) - 1)%Z with (-(Qfloor (-x) + 1))%Z by ring.
 change ((- (Qfloor (- x) + 1))%Z:Q) with (-(Qfloor (- x) + 1)%Z).
 apply Qlt_le_trans with (- - x); auto with *.
 rewrite Qopp_involutive.
-auto with *.
+apply Qle_refl.
 Qed.
 
 #[global]
@@ -106,7 +106,7 @@ simpl in *.
 rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *.
 rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *.
 rewrite (Z.mul_comm (Zpos yd) (Zpos xd)).
-apply Z_div_le; auto with *.
+apply Z.div_le_mono, Hxy; apply eq_refl.
 Qed.
 
 #[global]

theories/Reals/Nsatz.v

@@ -22,7 +22,6 @@ From Stdlib Require Import List.
 From Stdlib Require Import Setoid.
 From Stdlib Require Import BinPos.
 From Stdlib Require Import BinList.
-From Stdlib Require Import Znumtheory.
 From Stdlib Require Export Morphisms Setoid Bool.
 From Stdlib Require Export Algebra_syntax.
 From Stdlib Require Export Ncring.

theories/ZArith/ZArith.v

@@ -47,8 +47,12 @@ From Stdlib Require Export ZArith_hints.
 From Stdlib Require Export Zcomplements.
 From Stdlib Require Export Zpower.
 From Stdlib Require Export Zdiv.
+From Stdlib Require Export Zdivisibility.
 From Stdlib Require Export Zdiv_facts.
 From Stdlib Require Export Zbitwise.
 From Stdlib Require Export ZModOffset.
 
 Export ZArithRing.
+
+(* This compat Require is deprecated since 9.1 *)
+From Stdlib Require Znumtheory.