Library Stdlib.ZArith.Znumtheory


From Stdlib Require Import ZArith_base.
From Stdlib Require Import ZArithRing.
From Stdlib Require Import Zcomplements.
From Stdlib Require Import Zdiv.
From Stdlib Require Import Zdivisibility.
From Stdlib Require Import Wf_nat.
From Stdlib Require Import Lia Cring Ncring_tac.

For compatibility reasons, this Open Scope isn't local as it should

Open Scope Z_scope.

Local Ltac Tauto.intuition_solver ::= auto with zarith.

This file contains some notions of number theory upon Z numbers:
The former specialized inductive predicate Z.divide is now a generic existential predicate.
Its former constructor is now a pseudo-constructor.

#[deprecated(use=ex_intro, since="9.1")]
Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H.

Results concerning divisibility

#[deprecated(use=Z.divide_1_l, since="9.1")]
Notation Zone_divide := Z.divide_1_l (only parsing).
#[deprecated(use=Z.divide_0_r, since="9.1")]
Notation Zdivide_0 := Z.divide_0_r (only parsing).
#[deprecated(use=Z.mul_divide_mono_l, since="9.1")]
Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing).
#[deprecated(use=Z.mul_divide_mono_r, since="9.1")]
Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (only parsing).
#[deprecated(use=Z.divide_add_r, since="9.1")]
Notation Zdivide_plus_r := Z.divide_add_r (only parsing).
#[deprecated(use=Z.divide_sub_r, since="9.1")]
Notation Zdivide_minus_l := Z.divide_sub_r (only parsing).
#[deprecated(use=Z.divide_mul_l, since="9.1")]
Notation Zdivide_mult_l := Z.divide_mul_l (only parsing).
#[deprecated(use=Z.divide_mul_r, since="9.1")]
Notation Zdivide_mult_r := Z.divide_mul_r (only parsing).
#[deprecated(use=Z.divide_factor_l, since="9.1")]
Notation Zdivide_factor_r := Z.divide_factor_l (only parsing).
#[deprecated(use=Z.divide_factor_r, since="9.1")]
Notation Zdivide_factor_l := Z.divide_factor_r (only parsing).

#[deprecated(use=Z.divide_opp_r, since="9.1")]
Lemma Zdivide_opp_r a b : (a | b) -> (a | - b).

#[deprecated(use=Z.divide_opp_r, since="9.1")]
Lemma Zdivide_opp_r_rev a b : (a | - b) -> (a | b).

#[deprecated(use=Z.divide_opp_l, since="9.1")]
Lemma Zdivide_opp_l a b : (a | b) -> (- a | b).

#[deprecated(use=Z.divide_opp_l, since="9.1")]
Lemma Zdivide_opp_l_rev a b : (- a | b) -> (a | b).

#[deprecated(use=Z.divide_abs_l, since="9.1")]
Theorem Zdivide_Zabs_l a b : (Z.abs a | b) -> (a | b).

#[deprecated(use=Z.divide_abs_l, since="9.1")]
Theorem Zdivide_Zabs_inv_l a b : (a | b) -> (Z.abs a | b).

#[global]
Hint Resolve Z.divide_refl Z.divide_1_l Z.divide_0_r: zarith.
#[global]
Hint Resolve Z.mul_divide_mono_l Z.mul_divide_mono_r: zarith.
#[global]
Hint Resolve Z.divide_add_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l
  Zdivide_opp_l_rev Z.divide_sub_r Z.divide_mul_l Z.divide_mul_r
  Z.divide_factor_l Z.divide_factor_r: zarith.

Auxiliary result.

#[deprecated(use=Z.eq_mul_1_nonneg, since="9.1")]
Lemma Zmult_one x y : x >= 0 -> x * y = 1 -> x = 1.

Only 1 and -1 divide 1.

#[deprecated(use=Z.divide_1_r, since="9.1")]
Notation Zdivide_1 := Z.divide_1_r (only parsing).

If a divides b and b<>0 then |a| <= |b|.

#[deprecated(use=Z.absle_divide, since="9.1")]
Notation Zdivide_bounds := Z.absle_divide (only parsing).

Z.divide can be expressed using Z.modulo.

#[deprecated(use=Z.mod0_divide, since="9.1")]
Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a).

#[deprecated(use=Z.mod0_divide, since="9.1")]
Lemma Zdivide_mod : forall a b, (b | a) -> a mod b = 0.

Z.divide is hence decidable
#[deprecated(use=Z.BoolSpec_divide, since="9.1")]
Lemma Zdivide_dec a b : {(a | b)} + {~ (a | b)}.

#[deprecated(use=Z.lt_neq, since="9.1")]
Lemma Z_lt_neq {x y: Z} : x < y -> y <> x.

Theorem Zdivide_Zdiv_eq a b : 0 < a -> (a | b) -> b = a * (b / a).

Theorem Zdivide_Zdiv_eq_2 a b c :
 0 < a -> (a | b) -> (c * b) / a = c * (b / a).

#[deprecated(use=Z.divide_pos_le, since="9.1")]
Theorem Zdivide_le: forall a b : Z,
 0 <= a -> 0 < b -> (a | b) -> a <= b.

Theorem Zdivide_Zdiv_lt_pos a b :
 1 < a -> 0 < b -> (a | b) -> 0 < b / a < b .

#[deprecated(use=Z.mod_mod_divide, since="9.1")]
Lemma Zmod_div_mod n m a:
 0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n.

Lemma Zmod_divide_minus a b c:
 0 < b -> a mod b = c -> (b | a - c).

Lemma Zdivide_mod_minus a b c:
 0 <= c < b -> (b | a - c) -> a mod b = c.

Greatest common divisor (gcd).

There is no unicity of the gcd; hence we define the predicate Zis_gcd a b g expressing that g is a gcd of a and b. (We show later that the gcd is actually unique if we discard its sign.)

Inductive Zis_gcd (a b g:Z) : Prop :=
 Zis_gcd_intro :
  (g | a) ->
  (g | b) ->
  (forall x, (x | a) -> (x | b) -> (x | g)) ->
  Zis_gcd a b g.

#[deprecated(use=Z.gcd, since="9.1")]
Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b).

Trivial properties of gcd

Lemma Zis_gcd_sym : forall a b d, Zis_gcd a b d -> Zis_gcd b a d.

Lemma Zis_gcd_0 : forall a, Zis_gcd a 0 a.

#[deprecated(use=Z.gcd_1_r, since="9.1")]
Lemma Zis_gcd_1 : forall a, Zis_gcd a 1 1.

#[deprecated(use=Z.gcd_diag, since="9.1")]
Lemma Zis_gcd_refl : forall a, Zis_gcd a a a.

Lemma Zis_gcd_minus : forall a b d, Zis_gcd a (- b) d -> Zis_gcd b a d.

#[deprecated(note="Z.cd is always non-negative", since="9.1")]
Lemma Zis_gcd_opp : forall a b d, Zis_gcd a b d -> Zis_gcd b a (- d).

Lemma Zis_gcd_0_abs a : Zis_gcd 0 a (Z.abs a).

#[global]
Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.

#[deprecated(use=f_equal, note="Use Z.gcd", since="9.1")]
Theorem Zis_gcd_unique: forall a b c d : Z,
 Zis_gcd a b c -> Zis_gcd a b d -> c = d \/ c = (- d).

Extended Euclid algorithm.


Lemma deprecated_Zis_gcd_for_euclid :
  forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d.
#[deprecated(since="8.17")]
Notation Zis_gcd_for_euclid := deprecated_Zis_gcd_for_euclid (only parsing).

#[deprecated(since="9.1")]
Lemma Zis_gcd_for_euclid2 :
  forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d.

#[deprecated(use=Z.extgcd, since="9.1")]
Notation extgcd := Z.extgcd (only parsing).

#[deprecated(use=Z.extgcd_correct, since="9.1")]
Notation extgcd_correct := Z.extgcd_correct (only parsing).

Section extended_euclid_algorithm.

  Variables a b : Z.

  Inductive deprecated_Euclid : Set :=
    deprecated_Euclid_intro :
    forall u v d:Z, u * a + v * b = d -> Zis_gcd a b d -> deprecated_Euclid.

  Lemma deprecated_euclid : deprecated_Euclid.

  Lemma deprecated_euclid_rec :
    forall v3:Z,
      0 <= v3 ->
      forall u1 u2 u3 v1 v2:Z,
       u1 * a + u2 * b = u3 ->
       v1 * a + v2 * b = v3 ->
       (forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> deprecated_Euclid.

End extended_euclid_algorithm.

#[deprecated(since="8.17", note="Use Coq.ZArith.Znumtheory.extgcd")]
Notation Euclid := deprecated_Euclid (only parsing).
#[deprecated(since="8.17", note="Use Coq.ZArith.Znumtheory.extgcd")]
Notation Euclid_intro := deprecated_Euclid_intro (only parsing).
#[deprecated(since="8.17", note="Use Coq.ZArith.Znumtheory.extgcd")]
Notation euclid := deprecated_euclid (only parsing).
#[deprecated(since="8.17", note="Use Coq.ZArith.Znumtheory.extgcd")]
Notation euclid_rec := deprecated_euclid_rec (only parsing).

#[deprecated(use=Z.gcd_unique, since="9.1")]
Theorem Zis_gcd_uniqueness_apart_sign :
  forall a b d d':Z, Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'.

Bezout's coefficients


Inductive Bezout_deprecated (a b d:Z) : Prop :=
  Bezout_deprecated_intro : forall u v:Z, u * a + v * b = d -> Bezout_deprecated a b d.

#[deprecated(use=Z.Bezout, since="9.1")]
Notation Bezout := Bezout_deprecated (only parsing).
#[deprecated(use=ex_intro, since="9.1")]
Notation Bezout_intro := Bezout_deprecated_intro (only parsing).

Existence of Bezout's coefficients for the gcd of a and b
#[deprecated(use=Z.Bezout_coprime_iff, since="9.1")]
Lemma Zis_gcd_bezout : forall a b d:Z, Zis_gcd a b d -> Bezout a b d.

gcd of ca and cb is c gcd(a,b).

#[deprecated(use=Z.gcd_mul_mono_l, since="9.1")]
Lemma Zis_gcd_mult :
  forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d).

Relative primality


Definition rel_prime (a b:Z) : Prop := Zis_gcd a b 1.

Lemma rel_prime_iff_coprime a b : rel_prime a b <-> Z.coprime a b.

Bezout's theorem: a and b are relatively prime if and only if there exist u and v such that ua+vb = 1.

#[deprecated(use=Z.Bezout_coprime, since="9.1")]
Lemma rel_prime_bezout : forall a b:Z, rel_prime a b -> Bezout a b 1.

#[deprecated(use=Z.coprime_Bezout, since="9.1")]
Lemma bezout_rel_prime : forall a b:Z, Bezout a b 1 -> rel_prime a b.

Gauss's theorem: if a divides bc and if a and b are relatively prime, then a divides c.

#[deprecated(use=Z.gauss, since="9.1")]
Theorem Gauss : forall a b c:Z, (a | b * c) -> rel_prime a b -> (a | c).

If a is relatively prime to b and c, then it is to bc

#[deprecated(use=Z.coprime_mul_r, since="9.1")]
Lemma rel_prime_mult :
  forall a b c:Z, rel_prime a b -> rel_prime a c -> rel_prime a (b * c).

#[deprecated(note="Consider Z.gcd instead", since="9.1")]
Lemma rel_prime_cross_prod :
  forall a b c d:Z,
    rel_prime a b ->
    rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d.

After factorization by a gcd, the original numbers are relatively prime.

#[deprecated(use=Z.gcd_div_gcd, since="9.1")]
Lemma Zis_gcd_rel_prime :
  forall a b g:Z,
    b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g).

#[deprecated(use=Z.Symmetric_coprime, since="9.1")]
Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a.

Theorem rel_prime_div: forall p q r,
 rel_prime p q -> (r | p) -> rel_prime r q.

#[deprecated(use=Z.coprime_1_l, since="9.1")]
Theorem rel_prime_1: forall n, rel_prime 1 n.

#[deprecated(use=Z.coprime_0_l_iff, since="9.1")]
Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n.

#[deprecated(use=Z.coprime_mod_l_iff, since="9.1")]
Theorem rel_prime_mod: forall p q, 0 < q ->
 rel_prime p q -> rel_prime (p mod q) q.

#[deprecated(use=Z.coprime_mod_l_iff, since="9.1")]
Theorem rel_prime_mod_rev: forall p q, 0 < q ->
 rel_prime (p mod q) q -> rel_prime p q.

#[deprecated(note="unfold Z.coprime", since="9.1")]
Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0.

Primality

Note: prefer Z.prime
Inductive prime (p:Z) : Prop :=
  prime_intro :
    1 < p -> (forall n:Z, 1 <= n < p -> rel_prime n p) -> prime p.

#[deprecated(note="Use lia", since="9.1")]
Lemma Z_0_1_more x : 0<=x -> x=0 \/ x=1 \/ 1<x.

Theorem prime_alt p : Z.prime p <-> prime p.

The sole divisors of a prime number p are -1, 1, p and -p.

#[deprecated(use=Z.divide_prime_r, since="9.1")]
Lemma prime_divisors :
  forall p:Z,
    prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.

A prime number is relatively prime with any number it does not divide

#[deprecated(use=Z.coprime_prime_l, since="9.1")]
Lemma prime_rel_prime :
  forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a.

#[global]
Hint Resolve prime_rel_prime: zarith.

As a consequence, a prime number is relatively prime with smaller numbers

#[deprecated(use=Z.coprime_prime_small, since="9.1")]
Theorem rel_prime_le_prime:
 forall a p, prime p -> 1 <= a < p -> rel_prime a p.

If a prime p divides ab then it divides either a or b

#[deprecated(use=Z.divide_prime_mul, since="9.1")]
Lemma prime_mult :
  forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b).

#[deprecated(use=Z.not_prime_0, since="9.1")]
Lemma not_prime_0: ~ prime 0.

#[deprecated(use=Z.not_prime_1, since="9.1")]
Lemma not_prime_1: ~ prime 1.

#[deprecated(use=Z.prime_2, since="9.1")]
Lemma prime_2: prime 2.

#[deprecated(use=Z.prime_3, since="9.1")]
Theorem prime_3: prime 3.

#[deprecated(use=Z.prime_ge_2, since="9.1")]
Theorem prime_ge_2 p : prime p -> 2 <= p.

#[deprecated(use=Z.prime, since="9.1")]
Notation prime' := Z.prime (only parsing).

#[deprecated(use=Z.not_prime_square, since="9.1")]
Theorem square_not_prime: forall a, ~ prime (a * a).

#[deprecated(use=Z.divide_prime_prime, since="9.1")]
Theorem prime_div_prime: forall p q,
 prime p -> prime q -> (p | q) -> p = q.

#[deprecated(use=Z.gcd_nonneg , since="9.1")]
Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing).

#[deprecated(since="9.1")]
Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.

#[deprecated(use=Z.gcd_greatest, since="9.1")]
Theorem Zdivide_Zgcd: forall p q r : Z,
 (p | q) -> (p | r) -> (p | Z.gcd q r).

#[deprecated(use=Z.gcd, since="9.1")]
Theorem Zis_gcd_gcd: forall a b c : Z,
 0 <= c -> Zis_gcd a b c -> Z.gcd a b = c.

#[deprecated(use=Z.gcd_eq_0_l , since="9.1")]
Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (only parsing).
#[deprecated(use=Z.gcd_eq_0_r , since="9.1")]
Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing).

#[deprecated(use=Z.gcd_div_swap, since="9.1")]
Theorem Zgcd_div_swap0 : forall a b : Z,
 0 < Z.gcd a b ->
 0 < b ->
 (a / Z.gcd a b) * b = a * (b/Z.gcd a b).

#[deprecated(use=Z.gcd_div_swap, since="9.1")]
Theorem Zgcd_div_swap : forall a b c : Z,
 0 < Z.gcd a b ->
 0 < b ->
 (c * a) / Z.gcd a b * b = c * a * (b/Z.gcd a b).

#[deprecated(use=Z.gcd_assoc, since="9.1")]
Lemma Zgcd_ass a b c : Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c).

#[deprecated(use=Z.gcd_abs_l, since="9.1")]
Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing).
#[deprecated(use=Z.gcd_0_r, since="9.1")]
Notation Zgcd_0 := Z.gcd_0_r (only parsing).
#[deprecated(use=Z.gcd_1_r, since="9.1")]
Notation Zgcd_1 := Z.gcd_1_r (only parsing).

#[global]
Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith.

#[deprecated(note="Use Z.gcd_greatest, Z.gcd_divide_l, or Z.gcd_divide_r", since="9.1")]
Theorem Zgcd_1_rel_prime : forall a b,
 Z.gcd a b = 1 <-> rel_prime a b.

#[deprecated(use=Z.BoolSpec_coprime, since="9.1")]
Definition rel_prime_dec: forall a b,
 { rel_prime a b }+{ ~ rel_prime a b }.

#[deprecated(since="9.1")]
Definition prime_dec_aux:
 forall p m,
  { forall n, 1 < n < m -> rel_prime n p } +
  { exists n, 1 < n < m /\ ~ rel_prime n p }.

Definition prime_dec: forall p, { prime p }+{ ~ prime p }.

Theorem not_prime_divide:
 forall p, 1 < p -> ~ prime p -> exists n, 1 < n < p /\ (n | p).