The greatest common divisor of integers

module elementary-number-theory.greatest-common-divisor-integers where
Imports
open import elementary-number-theory.absolute-value-integers
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.divisibility-integers
open import elementary-number-theory.equality-integers
open import elementary-number-theory.greatest-common-divisor-natural-numbers
open import elementary-number-theory.integers
open import elementary-number-theory.natural-numbers

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

Definition

The predicate is-gcd-ℤ

is-common-divisor-ℤ :       UU lzero
is-common-divisor-ℤ x y d = (div-ℤ d x) × (div-ℤ d y)

is-gcd-ℤ :       UU lzero
is-gcd-ℤ x y d =
  is-nonnegative-ℤ d × ((k : )  is-common-divisor-ℤ x y k  div-ℤ k d)

The greatest common divisor of two integers

nat-gcd-ℤ :     
nat-gcd-ℤ x y = gcd-ℕ (abs-ℤ x) (abs-ℤ y)

gcd-ℤ :     
gcd-ℤ x y = int-ℕ (nat-gcd-ℤ x y)

Properties

A natural number d is a common divisor of two natural numbers x and y if and only if int-ℕ d is a common divisor of int-ℕ x and ind-ℕ y

is-common-divisor-int-is-common-divisor-ℕ :
  {x y d : } 
  is-common-divisor-ℕ x y d  is-common-divisor-ℤ (int-ℕ x) (int-ℕ y) (int-ℕ d)
is-common-divisor-int-is-common-divisor-ℕ =
  map-prod div-int-div-ℕ div-int-div-ℕ

is-common-divisor-is-common-divisor-int-ℕ :
  {x y d : } 
  is-common-divisor-ℤ (int-ℕ x) (int-ℕ y) (int-ℕ d)  is-common-divisor-ℕ x y d
is-common-divisor-is-common-divisor-int-ℕ {x} {y} {d} =
  map-prod div-div-int-ℕ div-div-int-ℕ

If ux = x' and vy = y' for two units u and v, then d is a common divisor of x and y if and only if d is a common divisor of x' and y'

is-common-divisor-sim-unit-ℤ :
  {x x' y y' d d' : }  sim-unit-ℤ x x'  sim-unit-ℤ y y'  sim-unit-ℤ d d' 
  is-common-divisor-ℤ x y d  is-common-divisor-ℤ x' y' d'
is-common-divisor-sim-unit-ℤ H K L =
  map-prod (div-sim-unit-ℤ L H) (div-sim-unit-ℤ L K)

If ux = x' and vy = y' for two units u and v, then d is a greatest common divisor of x and y if and only if c is a greatest common divisor of x' and y'

is-gcd-sim-unit-ℤ :
  {x x' y y' d : }  sim-unit-ℤ x x'  sim-unit-ℤ y y' 
  is-gcd-ℤ x y d  is-gcd-ℤ x' y' d
pr1 (is-gcd-sim-unit-ℤ H K (pair x _)) = x
pr1 (pr2 (is-gcd-sim-unit-ℤ H K (pair _ G)) k) =
  ( pr1 (G k)) 
  ( is-common-divisor-sim-unit-ℤ
    ( symm-sim-unit-ℤ H)
    ( symm-sim-unit-ℤ K)
    ( refl-sim-unit-ℤ k))
pr2 (pr2 (is-gcd-sim-unit-ℤ H K (pair _ G)) k) =
  ( is-common-divisor-sim-unit-ℤ H K (refl-sim-unit-ℤ k)) 
  ( pr2 (G k))

An integer d is a common divisor of x and y if and only if |d| is a common divisor of x and y

is-common-divisor-int-abs-is-common-divisor-ℤ :
  {x y d : } 
  is-common-divisor-ℤ x y d  is-common-divisor-ℤ x y (int-abs-ℤ d)
is-common-divisor-int-abs-is-common-divisor-ℤ =
  map-prod div-int-abs-div-ℤ div-int-abs-div-ℤ

is-common-divisor-is-common-divisor-int-abs-ℤ :
  {x y d : } 
  is-common-divisor-ℤ x y (int-abs-ℤ d)  is-common-divisor-ℤ x y d
is-common-divisor-is-common-divisor-int-abs-ℤ =
  map-prod div-div-int-abs-ℤ div-div-int-abs-ℤ

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 (pr2 H d) (refl-div-ℤ d)

A natural number d is a greatest common divisor of two natural numbers x and y if and only if int-ℕ d is a greatest common divisor of int-ℕ x and int-ℕ y

is-gcd-int-is-gcd-ℕ :
  {x y d : }  is-gcd-ℕ x y d  is-gcd-ℤ (int-ℕ x) (int-ℕ y) (int-ℕ d)
pr1 (is-gcd-int-is-gcd-ℕ {x} {y} {d} H) = is-nonnegative-int-ℕ d
pr1 (pr2 (is-gcd-int-is-gcd-ℕ {x} {y} {d} H) k) =
  ( ( ( ( div-div-int-abs-ℤ) 
        ( div-int-div-ℕ)) 
      ( pr1 (H (abs-ℤ k)))) 
    ( is-common-divisor-is-common-divisor-int-ℕ)) 
  ( is-common-divisor-int-abs-is-common-divisor-ℤ)
pr2 (pr2 (is-gcd-int-is-gcd-ℕ {x} {y} {d} H) k) =
  ( ( ( ( is-common-divisor-is-common-divisor-int-abs-ℤ) 
        ( is-common-divisor-int-is-common-divisor-ℕ)) 
      ( pr2 (H (abs-ℤ k)))) 
    ( div-div-int-ℕ)) 
  ( div-int-abs-div-ℤ)

is-gcd-is-gcd-int-ℕ :
  {x y d : }  is-gcd-ℤ (int-ℕ x) (int-ℕ y) (int-ℕ d)  is-gcd-ℕ x y d
pr1 (is-gcd-is-gcd-int-ℕ {x} {y} {d} H k) =
  ( ( div-div-int-ℕ) 
    ( pr1 (pr2 H (int-ℕ k)))) 
  ( is-common-divisor-int-is-common-divisor-ℕ)
pr2 (is-gcd-is-gcd-int-ℕ {x} {y} {d} H k) =
  ( ( is-common-divisor-is-common-divisor-int-ℕ) 
    ( pr2 (pr2 H (int-ℕ k)))) 
  ( div-int-div-ℕ)

gcd-ℤ x y is a greatest common divisor of x and y

is-nonnegative-gcd-ℤ : (x y : )  is-nonnegative-ℤ (gcd-ℤ x y)
is-nonnegative-gcd-ℤ x y = is-nonnegative-int-ℕ (nat-gcd-ℤ x y)

gcd-nonnegative-ℤ :     nonnegative-ℤ
pr1 (gcd-nonnegative-ℤ x y) = gcd-ℤ x y
pr2 (gcd-nonnegative-ℤ x y) = is-nonnegative-gcd-ℤ x y

is-gcd-gcd-ℤ : (x y : )  is-gcd-ℤ x y (gcd-ℤ x y)
pr1 (is-gcd-gcd-ℤ x y) = is-nonnegative-gcd-ℤ x y
pr1 (pr2 (is-gcd-gcd-ℤ x y) k) =
  ( ( ( ( ( div-sim-unit-ℤ
            ( sim-unit-abs-ℤ k)
            ( refl-sim-unit-ℤ (gcd-ℤ x y))) 
          ( div-int-div-ℕ)) 
        ( pr1 (is-gcd-gcd-ℕ (abs-ℤ x) (abs-ℤ y) (abs-ℤ k)))) 
      ( is-common-divisor-is-common-divisor-int-ℕ)) 
    ( is-common-divisor-int-abs-is-common-divisor-ℤ)) 
  ( is-common-divisor-sim-unit-ℤ
    ( symm-sim-unit-ℤ (sim-unit-abs-ℤ x))
    ( symm-sim-unit-ℤ (sim-unit-abs-ℤ y))
    ( refl-sim-unit-ℤ k))
pr2 (pr2 (is-gcd-gcd-ℤ x y) k) =
  ( ( ( ( ( is-common-divisor-sim-unit-ℤ
            ( sim-unit-abs-ℤ x)
            ( sim-unit-abs-ℤ y)
            ( refl-sim-unit-ℤ k)) 
          ( is-common-divisor-is-common-divisor-int-abs-ℤ)) 
        ( is-common-divisor-int-is-common-divisor-ℕ)) 
      ( pr2 (is-gcd-gcd-ℕ (abs-ℤ x) (abs-ℤ y) (abs-ℤ k)))) 
    ( div-div-int-ℕ)) 
  ( div-sim-unit-ℤ
    ( symm-sim-unit-ℤ (sim-unit-abs-ℤ k))
    ( refl-sim-unit-ℤ (gcd-ℤ x y)))

The gcd in of x and y is equal to the gcd in of int-ℕ x and int-ℕ y

eq-gcd-gcd-int-ℕ :
  (x y : )  gcd-ℤ (int-ℕ x) (int-ℕ y)  int-ℕ (gcd-ℕ x y)
eq-gcd-gcd-int-ℕ x y =
  ( ( ap
      ( λ x  int-ℕ (gcd-ℕ x (abs-ℤ (int-ℕ y))))
      ( abs-int-ℕ x)) 
    ( ap
      ( λ y  int-ℕ (gcd-ℕ x y))
      ( abs-int-ℕ y)))

The gcd of x and y divides both x and y

is-common-divisor-gcd-ℤ :
  (x y : )  is-common-divisor-ℤ x y (gcd-ℤ x y)
is-common-divisor-gcd-ℤ x y =
  pr2 (pr2 (is-gcd-gcd-ℤ x y) (gcd-ℤ x y)) (refl-div-ℤ (gcd-ℤ x y))

div-left-gcd-ℤ : (x y : )  div-ℤ (gcd-ℤ x y) x
div-left-gcd-ℤ x y = pr1 (is-common-divisor-gcd-ℤ x y)

div-right-gcd-ℤ : (x y : )  div-ℤ (gcd-ℤ x y) y
div-right-gcd-ℤ x y = pr2 (is-common-divisor-gcd-ℤ x y)

Any common divisor of x and y divides the greatest common divisor

div-gcd-is-common-divisor-ℤ :
  (x y k : )  is-common-divisor-ℤ x y k  div-ℤ k (gcd-ℤ x y)
div-gcd-is-common-divisor-ℤ x y k H =
  pr1 (pr2 (is-gcd-gcd-ℤ x y) k) H

If either x or y is a positive integer, then gcd-ℤ x y is positive

is-positive-gcd-is-positive-left-ℤ :
  (x y : )  is-positive-ℤ x  is-positive-ℤ (gcd-ℤ x y)
is-positive-gcd-is-positive-left-ℤ x y H =
  is-positive-int-ℕ
    ( gcd-ℕ (abs-ℤ x) (abs-ℤ y))
    ( is-nonzero-gcd-ℕ
      ( abs-ℤ x)
      ( abs-ℤ y)
      ( λ p  is-nonzero-abs-ℤ x H (f p)))
  where
  f : is-zero-ℕ ((abs-ℤ x) +ℕ (abs-ℤ y))  is-zero-ℕ (abs-ℤ x)
  f = is-zero-left-is-zero-add-ℕ (abs-ℤ x) (abs-ℤ y)

is-positive-gcd-is-positive-right-ℤ :
  (x y : )  is-positive-ℤ y  is-positive-ℤ (gcd-ℤ x y)
is-positive-gcd-is-positive-right-ℤ x y H =
  is-positive-int-ℕ
    ( gcd-ℕ (abs-ℤ x) (abs-ℤ y))
    ( is-nonzero-gcd-ℕ
      ( abs-ℤ x)
      ( abs-ℤ y)
      ( λ p  is-nonzero-abs-ℤ y H (f p)))
  where
  f : is-zero-ℕ ((abs-ℤ x) +ℕ (abs-ℤ y))  is-zero-ℕ (abs-ℤ y)
  f = is-zero-right-is-zero-add-ℕ (abs-ℤ x) (abs-ℤ y)

is-positive-gcd-ℤ :
  (x y : )  (is-positive-ℤ x) + (is-positive-ℤ y) 
  is-positive-ℤ (gcd-ℤ x y)
is-positive-gcd-ℤ x y (inl H) = is-positive-gcd-is-positive-left-ℤ x y H
is-positive-gcd-ℤ x y (inr H) = is-positive-gcd-is-positive-right-ℤ x y H

gcd-ℤ a b is zero if and only if both a and b are zero

is-zero-gcd-ℤ :
  (a b : )  is-zero-ℤ a  is-zero-ℤ b  is-zero-ℤ (gcd-ℤ a b)
is-zero-gcd-ℤ zero-ℤ zero-ℤ refl refl =
  ap int-ℕ is-zero-gcd-zero-zero-ℕ

is-zero-left-is-zero-gcd-ℤ :
  (a b : )  is-zero-ℤ (gcd-ℤ a b)  is-zero-ℤ a
is-zero-left-is-zero-gcd-ℤ a b =
  is-zero-is-zero-div-ℤ a (gcd-ℤ a b) (div-left-gcd-ℤ a b)

is-zero-right-is-zero-gcd-ℤ :
  (a b : )  is-zero-ℤ (gcd-ℤ a b)  is-zero-ℤ b
is-zero-right-is-zero-gcd-ℤ a b =
  is-zero-is-zero-div-ℤ b (gcd-ℤ a b) (div-right-gcd-ℤ a b)

gcd-ℤ is commutative

is-commutative-gcd-ℤ : (x y : )  gcd-ℤ x y  gcd-ℤ y x
is-commutative-gcd-ℤ x y =
  ap int-ℕ (is-commutative-gcd-ℕ (abs-ℤ x) (abs-ℤ y))

gcd-ℕ 1 b = 1

is-one-is-gcd-one-ℤ : {b x : }  is-gcd-ℤ one-ℤ b x  is-one-ℤ x
is-one-is-gcd-one-ℤ {b} {x} H with
  ( is-one-or-neg-one-is-unit-ℤ x
    ( pr1 (is-common-divisor-is-gcd-ℤ one-ℤ b x H)))
... | inl p = p
... | inr p = ex-falso (tr is-nonnegative-ℤ p (pr1 H))

is-one-gcd-one-ℤ : (b : )  is-one-ℤ (gcd-ℤ one-ℤ b)
is-one-gcd-one-ℤ b = is-one-is-gcd-one-ℤ (is-gcd-gcd-ℤ one-ℤ b)

gcd-ℤ a 1 = 1

is-one-is-gcd-one-ℤ' : {a x : }  is-gcd-ℤ a one-ℤ x  is-one-ℤ x
is-one-is-gcd-one-ℤ' {a} {x} H with
  ( is-one-or-neg-one-is-unit-ℤ x
    ( pr2 (is-common-divisor-is-gcd-ℤ a one-ℤ x H)))
... | inl p = p
... | inr p = ex-falso (tr is-nonnegative-ℤ p (pr1 H))

is-one-gcd-one-ℤ' : (a : )  is-one-ℤ (gcd-ℤ a one-ℤ)
is-one-gcd-one-ℤ' a = is-one-is-gcd-one-ℤ' (is-gcd-gcd-ℤ a one-ℤ)

gcd-ℤ 0 b = abs-ℤ b

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

is-id-is-gcd-zero-ℤ : {b x : }  gcd-ℤ zero-ℤ b  x  x  int-ℕ (abs-ℤ b)
is-id-is-gcd-zero-ℤ {inl b} {x} H
  with (is-plus-or-minus-sim-unit-ℤ (is-sim-id-is-gcd-zero-ℤ {inl b} {x} H))
... | inl p =
  ex-falso
    ( Eq-eq-ℤ
      ( inv (pr2 (lem (gcd-ℤ zero-ℤ (inl b)) gcd-is-nonneg))  (H  p)))
  where
  gcd-is-nonneg : is-nonnegative-ℤ (gcd-ℤ zero-ℤ (inl b))
  gcd-is-nonneg = is-nonnegative-int-ℕ (gcd-ℕ 0 (succ-ℕ b))
  lem : (y : )  is-nonnegative-ℤ y  Σ (unit + )  z  y  inr z)
  lem (inr z) H = pair z refl
... | inr p = inv (neg-neg-ℤ x)  ap neg-ℤ p
is-id-is-gcd-zero-ℤ {inr (inl star)} {x} H =
  inv H  is-zero-gcd-ℤ zero-ℤ zero-ℤ refl refl
is-id-is-gcd-zero-ℤ {inr (inr b)} {x} H
  with
  is-plus-or-minus-sim-unit-ℤ (is-sim-id-is-gcd-zero-ℤ {inr (inr b)} {x} H)
... | inl p = p
... | inr p =
  ex-falso
    ( Eq-eq-ℤ
      ( ( inv (pr2 (lem (gcd-ℤ zero-ℤ (inl b)) gcd-is-nonneg))) 
        ( H  (inv (neg-neg-ℤ x)  ap neg-ℤ p))))
  where
  gcd-is-nonneg : is-nonnegative-ℤ (gcd-ℤ zero-ℤ (inl b))
  gcd-is-nonneg = is-nonnegative-int-ℕ (gcd-ℕ 0 (succ-ℕ b))
  lem : (y : )  is-nonnegative-ℤ y  Σ (unit + )  z  y  inr z)
  lem (inr z) H = pair z refl

gcd-ℤ a 0 = abs-ℤ a

is-sim-id-is-gcd-zero-ℤ' : {a x : }  gcd-ℤ a zero-ℤ  x  sim-unit-ℤ x a
is-sim-id-is-gcd-zero-ℤ' {a} {x} H = is-sim-id-is-gcd-zero-ℤ {a} {x}
  ((is-commutative-gcd-ℤ zero-ℤ a)  H)

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