The greatest common divisor of natural numbers

module elementary-number-theory.greatest-common-divisor-natural-numbers where
Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.decidable-types
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.divisibility-natural-numbers
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.euclidean-division-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.lower-bounds-natural-numbers
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers
open import elementary-number-theory.well-ordering-principle-natural-numbers

open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.functoriality-cartesian-product-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.universe-levels

Idea

The greatest common divisor of two natural numbers x and y is a number gcd x y such that any natural number d : ℕ is a common divisor of x and y if and only if it is a divisor of gcd x y.

Definition

Common divisors

is-common-divisor-ℕ : (a b x : )  UU lzero
is-common-divisor-ℕ a b x = (div-ℕ x a) × (div-ℕ x b)

Greatest common divisors

is-gcd-ℕ : (a b d : )  UU lzero
is-gcd-ℕ a b d = (x : )  (is-common-divisor-ℕ a b x)  (div-ℕ x d)

The predicate of being a multiple of the greatest common divisor

is-multiple-of-gcd-ℕ : (a b n : )  UU lzero
is-multiple-of-gcd-ℕ a b n =
  is-nonzero-ℕ (a +ℕ b) 
  (is-nonzero-ℕ n) × ((x : )  is-common-divisor-ℕ a b x  div-ℕ x n)

Properties

Reflexivity for common divisors

refl-is-common-divisor-ℕ :
  (x : )  is-common-divisor-ℕ x x x
pr1 (refl-is-common-divisor-ℕ x) = refl-div-ℕ x
pr2 (refl-is-common-divisor-ℕ x) = refl-div-ℕ x

Being a common divisor is decidable

is-decidable-is-common-divisor-ℕ :
  (a b : )  is-decidable-fam (is-common-divisor-ℕ a b)
is-decidable-is-common-divisor-ℕ a b x =
  is-decidable-prod
    ( is-decidable-div-ℕ x a)
    ( is-decidable-div-ℕ x b)

Any greatest common divisor is a common divisor

is-common-divisor-is-gcd-ℕ :
  (a b d : )  is-gcd-ℕ a b d  is-common-divisor-ℕ a b d
is-common-divisor-is-gcd-ℕ a b d H = pr2 (H d) (refl-div-ℕ d)

Uniqueness of greatest common divisors

uniqueness-is-gcd-ℕ :
  (a b d d' : )  is-gcd-ℕ a b d  is-gcd-ℕ a b d'  d  d'
uniqueness-is-gcd-ℕ a b d d' H H' =
  antisymmetric-div-ℕ d d'
    ( pr1 (H' d) (is-common-divisor-is-gcd-ℕ a b d H))
    ( pr1 (H d') (is-common-divisor-is-gcd-ℕ a b d' H'))

If d is a common divisor of a and b, and a + b ≠ 0, then d ≤ a + b

leq-sum-is-common-divisor-ℕ' :
  (a b d : ) 
  is-successor-ℕ (a +ℕ b)  is-common-divisor-ℕ a b d  leq-ℕ d (a +ℕ b)
leq-sum-is-common-divisor-ℕ' a zero-ℕ d (pair k p) H =
  concatenate-leq-eq-ℕ d
    ( leq-div-succ-ℕ d k (concatenate-div-eq-ℕ (pr1 H) p))
    ( inv p)
leq-sum-is-common-divisor-ℕ' a (succ-ℕ b) d (pair k p) H =
  leq-div-succ-ℕ d (a +ℕ b) (div-add-ℕ d a (succ-ℕ b) (pr1 H) (pr2 H))

leq-sum-is-common-divisor-ℕ :
  (a b d : ) 
  is-nonzero-ℕ (a +ℕ b)  is-common-divisor-ℕ a b d  leq-ℕ d (a +ℕ b)
leq-sum-is-common-divisor-ℕ a b d H =
  leq-sum-is-common-divisor-ℕ' a b d (is-successor-is-nonzero-ℕ H)

Being a multiple of the greatest common divisor is decidable

is-decidable-is-multiple-of-gcd-ℕ :
  (a b : )  is-decidable-fam (is-multiple-of-gcd-ℕ a b)
is-decidable-is-multiple-of-gcd-ℕ a b n =
  is-decidable-function-type'
    ( is-decidable-neg (is-decidable-is-zero-ℕ (a +ℕ b)))
    ( λ np 
      is-decidable-prod
        ( is-decidable-neg (is-decidable-is-zero-ℕ n))
        ( is-decidable-bounded-Π-ℕ
          ( is-common-divisor-ℕ a b)
          ( λ x  div-ℕ x n)
          ( is-decidable-is-common-divisor-ℕ a b)
          ( λ x  is-decidable-div-ℕ x n)
          ( a +ℕ b)
          ( λ x  leq-sum-is-common-divisor-ℕ a b x np)))

The sum of a and b is a multiple of the greatest common divisor of a and b

sum-is-multiple-of-gcd-ℕ : (a b : )  is-multiple-of-gcd-ℕ a b (a +ℕ b)
pr1 (sum-is-multiple-of-gcd-ℕ a b np) = np
pr2 (sum-is-multiple-of-gcd-ℕ a b np) x H = div-add-ℕ x a b (pr1 H) (pr2 H)

The greatest common divisor exists

abstract
  GCD-ℕ : (a b : )  minimal-element-ℕ (is-multiple-of-gcd-ℕ a b)
  GCD-ℕ a b =
    well-ordering-principle-ℕ
      ( is-multiple-of-gcd-ℕ a b)
      ( is-decidable-is-multiple-of-gcd-ℕ a b)
      ( pair (a +ℕ b) (sum-is-multiple-of-gcd-ℕ a b))

gcd-ℕ :     
gcd-ℕ a b = pr1 (GCD-ℕ a b)

is-multiple-of-gcd-gcd-ℕ : (a b : )  is-multiple-of-gcd-ℕ a b (gcd-ℕ a b)
is-multiple-of-gcd-gcd-ℕ a b = pr1 (pr2 (GCD-ℕ a b))

is-lower-bound-gcd-ℕ :
  (a b : )  is-lower-bound-ℕ (is-multiple-of-gcd-ℕ a b) (gcd-ℕ a b)
is-lower-bound-gcd-ℕ a b = pr2 (pr2 (GCD-ℕ a b))

a + b = 0 if and only if gcd a b = 0

is-zero-gcd-ℕ :
  (a b : )  is-zero-ℕ (a +ℕ b)  is-zero-ℕ (gcd-ℕ a b)
is-zero-gcd-ℕ a b p =
  is-zero-leq-zero-ℕ
    ( gcd-ℕ a b)
    ( concatenate-leq-eq-ℕ
      ( gcd-ℕ a b)
      ( is-lower-bound-gcd-ℕ a b
        ( a +ℕ b)
        ( sum-is-multiple-of-gcd-ℕ a b))
      ( p))

is-zero-gcd-zero-zero-ℕ : is-zero-ℕ (gcd-ℕ zero-ℕ zero-ℕ)
is-zero-gcd-zero-zero-ℕ = is-zero-gcd-ℕ zero-ℕ zero-ℕ refl

is-zero-add-is-zero-gcd-ℕ :
  (a b : )  is-zero-ℕ (gcd-ℕ a b)  is-zero-ℕ (a +ℕ b)
is-zero-add-is-zero-gcd-ℕ a b H =
  double-negation-elim-is-decidable
    ( is-decidable-is-zero-ℕ (a +ℕ b))
    ( λ f  pr1 (is-multiple-of-gcd-gcd-ℕ a b f) H)

If at least one of a and b is nonzero, then their gcd is nonzero

is-nonzero-gcd-ℕ :
  (a b : )  is-nonzero-ℕ (a +ℕ b)  is-nonzero-ℕ (gcd-ℕ a b)
is-nonzero-gcd-ℕ a b ne = pr1 (is-multiple-of-gcd-gcd-ℕ a b ne)

is-successor-gcd-ℕ :
  (a b : )  is-nonzero-ℕ (a +ℕ b)  is-successor-ℕ (gcd-ℕ a b)
is-successor-gcd-ℕ a b ne =
  is-successor-is-nonzero-ℕ (is-nonzero-gcd-ℕ a b ne)

Any common divisor is also a divisor of the greatest common divisor

div-gcd-is-common-divisor-ℕ :
  (a b x : )  is-common-divisor-ℕ a b x  div-ℕ x (gcd-ℕ a b)
div-gcd-is-common-divisor-ℕ a b x H with
  is-decidable-is-zero-ℕ (a +ℕ b)
... | inl p = concatenate-div-eq-ℕ (div-zero-ℕ x) (inv (is-zero-gcd-ℕ a b p))
... | inr np = pr2 (is-multiple-of-gcd-gcd-ℕ a b np) x H

If every common divisor divides a number r < gcd a b, then r = 0.

is-zero-is-common-divisor-le-gcd-ℕ :
  (a b r : )  le-ℕ r (gcd-ℕ a b) 
  ((x : )  is-common-divisor-ℕ a b x  div-ℕ x r)  is-zero-ℕ r
is-zero-is-common-divisor-le-gcd-ℕ a b r l d with is-decidable-is-zero-ℕ r
... | inl H = H
... | inr x =
  ex-falso
    ( contradiction-le-ℕ r (gcd-ℕ a b) l
      ( is-lower-bound-gcd-ℕ a b r  np  pair x d)))

Any divisor of gcd a b is a common divisor of a and b

div-left-factor-div-gcd-ℕ :
  (a b x : )  div-ℕ x (gcd-ℕ a b)  div-ℕ x a
div-left-factor-div-gcd-ℕ a b x d with
  is-decidable-is-zero-ℕ (a +ℕ b)
... | inl p =
  concatenate-div-eq-ℕ (div-zero-ℕ x) (inv (is-zero-left-is-zero-add-ℕ a b p))
... | inr np =
  transitive-div-ℕ x (gcd-ℕ a b) a d
    ( pair q
      ( ( ( α) 
          ( ap ( dist-ℕ a)
               ( is-zero-is-common-divisor-le-gcd-ℕ a b r B
                 ( λ x H 
                   div-right-summand-ℕ x (q *ℕ (gcd-ℕ a b)) r
                     ( div-mul-ℕ q x (gcd-ℕ a b)
                       ( div-gcd-is-common-divisor-ℕ a b x H))
                     ( concatenate-div-eq-ℕ (pr1 H) (inv β)))))) 
        ( right-unit-law-dist-ℕ a)))
  where
  r = remainder-euclidean-division-ℕ (gcd-ℕ a b) a
  q = quotient-euclidean-division-ℕ (gcd-ℕ a b) a
  α = eq-quotient-euclidean-division-ℕ (gcd-ℕ a b) a
  B = strict-upper-bound-remainder-euclidean-division-ℕ (gcd-ℕ a b) a
       ( is-nonzero-gcd-ℕ a b np)
  β = eq-euclidean-division-ℕ (gcd-ℕ a b) a

div-right-factor-div-gcd-ℕ :
  (a b x : )  div-ℕ x (gcd-ℕ a b)  div-ℕ x b
div-right-factor-div-gcd-ℕ a b x d with
  is-decidable-is-zero-ℕ (a +ℕ b)
... | inl p =
  concatenate-div-eq-ℕ (div-zero-ℕ x) (inv (is-zero-right-is-zero-add-ℕ a b p))
... | inr np =
  transitive-div-ℕ x (gcd-ℕ a b) b d
    ( pair q
      ( ( α  ( ap ( dist-ℕ b)
               ( is-zero-is-common-divisor-le-gcd-ℕ a b r B
                 ( λ x H 
                   div-right-summand-ℕ x (q *ℕ (gcd-ℕ a b)) r
                     ( div-mul-ℕ q x (gcd-ℕ a b)
                       ( div-gcd-is-common-divisor-ℕ a b x H))
                     ( concatenate-div-eq-ℕ (pr2 H) (inv β)))))) 
        ( right-unit-law-dist-ℕ b)))
  where
  r = remainder-euclidean-division-ℕ (gcd-ℕ a b) b
  q = quotient-euclidean-division-ℕ (gcd-ℕ a b) b
  α = eq-quotient-euclidean-division-ℕ (gcd-ℕ a b) b
  B = strict-upper-bound-remainder-euclidean-division-ℕ (gcd-ℕ a b) b
       ( is-nonzero-gcd-ℕ a b np)
  β = eq-euclidean-division-ℕ (gcd-ℕ a b) b

is-common-divisor-div-gcd-ℕ :
  (a b x : )  div-ℕ x (gcd-ℕ a b)  is-common-divisor-ℕ a b x
pr1 (is-common-divisor-div-gcd-ℕ a b x d) =
  div-left-factor-div-gcd-ℕ a b x d
pr2 (is-common-divisor-div-gcd-ℕ a b x d) =
  div-right-factor-div-gcd-ℕ a b x d

The gcd of a and b is a common divisor

div-left-factor-gcd-ℕ : (a b : )  div-ℕ (gcd-ℕ a b) a
div-left-factor-gcd-ℕ a b =
  div-left-factor-div-gcd-ℕ a b (gcd-ℕ a b) (refl-div-ℕ (gcd-ℕ a b))

div-right-factor-gcd-ℕ : (a b : )  div-ℕ (gcd-ℕ a b) b
div-right-factor-gcd-ℕ a b =
  div-right-factor-div-gcd-ℕ a b (gcd-ℕ a b) (refl-div-ℕ (gcd-ℕ a b))

is-common-divisor-gcd-ℕ : (a b : )  is-common-divisor-ℕ a b (gcd-ℕ a b)
is-common-divisor-gcd-ℕ a b =
  is-common-divisor-div-gcd-ℕ a b (gcd-ℕ a b) (refl-div-ℕ (gcd-ℕ a b))

The gcd of a and b is a greatest common divisor

is-gcd-gcd-ℕ : (a b : )  is-gcd-ℕ a b (gcd-ℕ a b)
pr1 (is-gcd-gcd-ℕ a b x) = div-gcd-is-common-divisor-ℕ a b x
pr2 (is-gcd-gcd-ℕ a b x) = is-common-divisor-div-gcd-ℕ a b x

The gcd is commutative

is-commutative-gcd-ℕ : (a b : )  gcd-ℕ a b  gcd-ℕ b a
is-commutative-gcd-ℕ a b =
  antisymmetric-div-ℕ
    ( gcd-ℕ a b)
    ( gcd-ℕ b a)
    ( pr1 (is-gcd-gcd-ℕ b a (gcd-ℕ a b)) (σ (is-common-divisor-gcd-ℕ a b)))
    ( pr1 (is-gcd-gcd-ℕ a b (gcd-ℕ b a)) (σ (is-common-divisor-gcd-ℕ b a)))
  where
  σ : {A B : UU lzero}  A × B  B × A
  pr1 (σ (pair x y)) = y
  pr2 (σ (pair x y)) = x

If d is a common divisor of a and b, then kd is a common divisor of ka and kb.

preserves-is-common-divisor-mul-ℕ :
  (k a b d : )  is-common-divisor-ℕ a b d 
  is-common-divisor-ℕ (k *ℕ a) (k *ℕ b) (k *ℕ d)
preserves-is-common-divisor-mul-ℕ k a b d =
  map-prod
    ( preserves-div-mul-ℕ k d a)
    ( preserves-div-mul-ℕ k d b)

reflects-is-common-divisor-mul-ℕ :
  (k a b d : )  is-nonzero-ℕ k 
  is-common-divisor-ℕ (k *ℕ a) (k *ℕ b) (k *ℕ d) 
  is-common-divisor-ℕ a b d
reflects-is-common-divisor-mul-ℕ k a b d H =
  map-prod
    ( reflects-div-mul-ℕ k d a H)
    ( reflects-div-mul-ℕ k d b H)

gcd-ℕ 1 b = 1

is-one-is-gcd-one-ℕ : {b x : }  is-gcd-ℕ 1 b x  is-one-ℕ x
is-one-is-gcd-one-ℕ {b} {x} H =
  is-one-div-one-ℕ x (pr1 (is-common-divisor-is-gcd-ℕ 1 b x H))

is-one-gcd-one-ℕ : (b : )  is-one-ℕ (gcd-ℕ 1 b)
is-one-gcd-one-ℕ b = is-one-is-gcd-one-ℕ (is-gcd-gcd-ℕ 1 b)

gcd-ℕ a 1 = 1

is-one-is-gcd-one-ℕ' : {a x : }  is-gcd-ℕ a 1 x  is-one-ℕ x
is-one-is-gcd-one-ℕ' {a} {x} H =
  is-one-div-one-ℕ x (pr2 (is-common-divisor-is-gcd-ℕ a 1 x H))

is-one-gcd-one-ℕ' : (a : )  is-one-ℕ (gcd-ℕ a 1)
is-one-gcd-one-ℕ' a = is-one-is-gcd-one-ℕ' (is-gcd-gcd-ℕ a 1)

gcd-ℕ 0 b = b

is-id-is-gcd-zero-ℕ : {b x : }  gcd-ℕ 0 b  x  x  b
is-id-is-gcd-zero-ℕ {b} {x} H = antisymmetric-div-ℕ x b
  (pr2 (is-common-divisor-is-gcd-ℕ 0 b x
    (tr  t  is-gcd-ℕ 0 b t) H (is-gcd-gcd-ℕ 0 b))))
  (tr  t  div-ℕ b t) H
    (div-gcd-is-common-divisor-ℕ 0 b b
      (pair' (div-zero-ℕ b) (refl-div-ℕ b))))

gcd-ℕ a 0 = a

is-id-is-gcd-zero-ℕ' : {a x : }  gcd-ℕ a 0  x  x  a
is-id-is-gcd-zero-ℕ' {a} {x} H = is-id-is-gcd-zero-ℕ {a} {x}
  ((is-commutative-gcd-ℕ 0 a)  H)

Consider a common divisor d of a and b and let e be a divisor of d. Then any divisor of d/e is a common divisor of a/e and b/e.

is-common-divisor-quotients-div-quotient-ℕ :
  {a b d e n : }  is-nonzero-ℕ e  (H : is-common-divisor-ℕ a b d)
  (K : div-ℕ e d)  div-ℕ n (quotient-div-ℕ e d K) 
  (M : is-common-divisor-ℕ a b e) 
  is-common-divisor-ℕ
    ( quotient-div-ℕ e a (pr1 M))
    ( quotient-div-ℕ e b (pr2 M))
    ( n)
pr1 (is-common-divisor-quotients-div-quotient-ℕ nz H K L M) =
  div-quotient-div-div-quotient-div-ℕ nz (pr1 H) K (pr1 M) L
pr2 (is-common-divisor-quotients-div-quotient-ℕ nz H K L M) =
  div-quotient-div-div-quotient-div-ℕ nz (pr2 H) K (pr2 M) L

simplify-is-common-divisor-quotient-div-ℕ :
  {a b d x : }  is-nonzero-ℕ d  (H : is-common-divisor-ℕ a b d) 
  is-common-divisor-ℕ
    ( quotient-div-ℕ d a (pr1 H))
    ( quotient-div-ℕ d b (pr2 H))
    ( x) 
  is-common-divisor-ℕ a b (x *ℕ d)
pr1 (pr1 (simplify-is-common-divisor-quotient-div-ℕ nz H) K) =
  forward-implication (simplify-div-quotient-div-ℕ nz (pr1 H)) (pr1 K)
pr2 (pr1 (simplify-is-common-divisor-quotient-div-ℕ nz H) K) =
  forward-implication (simplify-div-quotient-div-ℕ nz (pr2 H)) (pr2 K)
pr1 (pr2 (simplify-is-common-divisor-quotient-div-ℕ nz H) K) =
  backward-implication (simplify-div-quotient-div-ℕ nz (pr1 H)) (pr1 K)
pr2 (pr2 (simplify-is-common-divisor-quotient-div-ℕ nz H) K) =
  backward-implication (simplify-div-quotient-div-ℕ nz (pr2 H)) (pr2 K)

The greatest common divisor of a/d and b/d is gcd(a,b)/d

is-gcd-quotient-div-gcd-ℕ :
  {a b d : }  is-nonzero-ℕ d  (H : is-common-divisor-ℕ a b d) 
  is-gcd-ℕ
    ( quotient-div-ℕ d a (pr1 H))
    ( quotient-div-ℕ d b (pr2 H))
    ( quotient-div-ℕ d
      ( gcd-ℕ a b)
      ( div-gcd-is-common-divisor-ℕ a b d H))
is-gcd-quotient-div-gcd-ℕ {a} {b} {d} nz H x =
  logical-equivalence-reasoning
    is-common-divisor-ℕ
      ( quotient-div-ℕ d a (pr1 H))
      ( quotient-div-ℕ d b (pr2 H))
      ( x)
     is-common-divisor-ℕ a b (x *ℕ d)
      by simplify-is-common-divisor-quotient-div-ℕ nz H
     div-ℕ (x *ℕ d) (gcd-ℕ a b)
      by is-gcd-gcd-ℕ a b (x *ℕ d)
     div-ℕ x
        ( quotient-div-ℕ d
          ( gcd-ℕ a b)
          ( div-gcd-is-common-divisor-ℕ a b d H))
      by
      inv-iff
        ( simplify-div-quotient-div-ℕ nz
          ( div-gcd-is-common-divisor-ℕ a b d H))