Andrew Sneap - 27th April 2021
Updated July 2022

In this file I define common divisors, and HCF's, along with a proof
that the Euclidean Algorithm produces HCF's.
\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan renaming (_+_ to _∔_)

open import Naturals.Addition
open import Naturals.Division
open import Naturals.Multiplication
open import Naturals.Order
open import Naturals.Properties
open import Notation.Order
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

module Naturals.HCF where

\end{code}

A common divisor d of x and y is a Natural Number which divides x and y,
and clearly is a proposition.

\begin{code}

is-common-divisor : (d x y : ℕ) → 𝓤₀ ̇
is-common-divisor d x y = (d ∣ x) × (d ∣ y)

is-common-divisor-is-prop : (d x y : ℕ)
                          → is-prop (is-common-divisor (succ d) x y)
is-common-divisor-is-prop d x y = ×-is-prop (_∣_-is-prop d x) (_∣_-is-prop d y)

\end{code}

The highest common divisor of x and y is the common divisor of x and y
which is greater than all other common divisors. One way to formulate
the type of the hcf h of x and y is to say that any other common
factor is a divisor of the highest common factor.

\begin{code}

is-hcf : (h x y : ℕ) → 𝓤₀ ̇
is-hcf h x y = (is-common-divisor h x y)
             × ((d : ℕ) → is-common-divisor d x y → d ∣ h)

\end{code}

Of course, any we can retrieve from the cartesian product that the hcf
is a common divisor.

\begin{code}

is-hcf-gives-is-common-divisor : (h x y : ℕ)
                               → is-hcf h x y
                               → is-common-divisor h x y
is-hcf-gives-is-common-divisor h x y (a , p) = a

\end{code}

The statement "succ h is the highest common factor of x and y" is a
proposition.  In order to prove this, function extensionality is
required, because the second projection of the cartesian product is a
function. With function extensionality, proof that this statement is a
proposition follows from the proof that (is-common-divisor d x y) is a
proposition.

\begin{code}

is-hcf-is-prop : Fun-Ext → (h x y : ℕ) → is-prop (is-hcf (succ h) x y)
is-hcf-is-prop fe h x y p q = ×-is-prop (is-common-divisor-is-prop h x y) II p q
  where
    I : (d : ℕ) → is-common-divisor d x y → is-prop (d ∣ succ h)
    I 0        i x = 𝟘-elim (zero-does-not-divide-positive h x)
    I (succ d) i   = d ∣ (succ h) -is-prop

    II : is-prop ((d : ℕ) → is-common-divisor d x y → d ∣ succ h)
    II p' q' = Π₂-is-prop fe I p' q'

\end{code}

Of course, hcf is commutative, which is easily proved by re-ordering
projections, and other properties of hcf are simple corollaries of the
definition.

\begin{code}

hcf-comm : (x y h : ℕ) → is-hcf h x y → is-hcf h y x
hcf-comm x y h ((h∣x , h∣y) , f) = (h∣y , h∣x) , γ
 where
  γ : (d : ℕ) → is-common-divisor d y x → d ∣ h
  γ d (d∣y , d∣x) = f d (d∣x , d∣y)

hcf-comm' : (x y : ℕ) → Σ h ꞉ ℕ , is-hcf h x y → Σ h ꞉ ℕ , is-hcf h y x
hcf-comm' x y (h , is-hcf) = h , (hcf-comm x y h is-hcf)

hcf-one-left : {x : ℕ} → is-hcf 1 1 x
hcf-one-left {x} = (∣-refl , 1-divides-all x) , γ
 where
  γ : (d : ℕ) → is-common-divisor d 1 x → d ∣ 1
  γ d (d-divides-1 , _) = d-divides-1

hcf-one-right : {x : ℕ} → is-hcf 1 x 1
hcf-one-right {x} = hcf-comm 1 x 1 hcf-one-left

hcf-refl : {x : ℕ} → is-hcf x x x
hcf-refl {x} = (∣-refl , ∣-refl) , γ
 where
  γ : (d : ℕ) → is-common-divisor d x x → d ∣ x
  γ d (d-divides-x , _) = d-divides-x

hcf-zero-left : {x : ℕ} → is-hcf x 0 x
hcf-zero-left {x} = (everything-divides-zero , ∣-refl) , γ
 where
  γ : (d : ℕ) → is-common-divisor d 0 x → d ∣ x
  γ d (_ , d-divides-0) = d-divides-0

hcf-zero-right : {x : ℕ} → is-hcf x x 0
hcf-zero-right {x} = hcf-comm 0 x x hcf-zero-left

\end{code}

With an eye towards implement Euclid's algorithm to compute the
highest common factor, we now prove two lemmas; each direction of the
following proof:

If x ＝ q * y + r, then is-hcf h x y ↔ is-hcf y r.

For Euclid's algorithm, we only need the right-to-left implication,
but both are proved for completeness.

The general idea of the right-to-left implication is as follows:

x ＝ q * y + r, h | y and h | r, with h ＝ hcf(y , r).

Now, clearly h | x since h | (q * y + r), and h | y by assumption,
so h is a common factor of x and y.

To show that h is the highest common factor, assume that d | x,
d | y, and further that d * u ＝ x , d * v ＝ y for some u , v.

If we can show that d | y, and d | r, then d | h since is-hcf h y r.
First, d | y by assumption.

Now, d * u ＝ q * (d * v) + r, so by the factor-of-sum-consequence,
d | r, and we are done.

\begin{code}

euclids-algorithm-lemma : (x y q r h : ℕ)
                        → x ＝ q * y + r
                        → is-hcf h x y
                        → is-hcf h y r
euclids-algorithm-lemma x y q r h e (((a , e₀) , b , e₁) , f) = I , II
 where
  I : is-common-divisor h y r
  I = (b , e₁) , factor-of-sum-consequence h a (q * b) r i
   where
    i : h * a ＝ h * (q * b) + r
    i = h * a           ＝⟨ e₀                                            ⟩
        x               ＝⟨ e                                             ⟩
        q * y + r       ＝⟨ ap (λ - → q * - + r) (e₁ ⁻¹)                  ⟩
        q * (h * b) + r ＝⟨ ap (_+ r) (mult-associativity q h b ⁻¹)       ⟩
        q * h * b + r   ＝⟨ ap (λ - → - * b + r) (mult-commutativity q h) ⟩
        h * q * b + r   ＝⟨ ap (_+ r) (mult-associativity h q b)          ⟩
        h * (q * b) + r ∎

  II : (d : ℕ) → is-common-divisor d y r → d ∣ h
  II d ((u , e₁) , v , e₂) = f d ((q * u + v , i) , u , e₁)
   where
    i : d * (q * u + v) ＝ x
    i = d * (q * u + v)     ＝⟨ distributivity-mult-over-addition d (q * u) v ⟩
        d * (q * u) + d * v ＝⟨ ap (d * (q * u) +_) e₂                        ⟩
        d * (q * u) + r     ＝⟨ ap (_+ r) (mult-associativity d q u ⁻¹)       ⟩
        d * q * u + r       ＝⟨ ap (λ - → - * u + r) (mult-commutativity d q) ⟩
        q * d * u + r       ＝⟨ ap (_+ r) (mult-associativity q d u)          ⟩
        q * (d * u) + r     ＝⟨ ap (λ - → q * - + r) e₁                       ⟩
        q * y + r           ＝⟨ e ⁻¹                                          ⟩
        x                   ∎

euclids-algorithm-lemma' : (x y q r h : ℕ)
                         → x ＝ q * y + r
                         → is-hcf h y r
                         → is-hcf h x y
euclids-algorithm-lemma' x y q r h e (((a , e₀) , b , e₁) , f) = I , II
 where
  I : is-common-divisor h x y
  I = (q * a + b , i) , (a , e₀)
   where
    i : h * (q * a + b) ＝ x
    i = h * (q * a + b)     ＝⟨ distributivity-mult-over-addition h (q * a) b ⟩
        h * (q * a) + h * b ＝⟨ ap (h * (q * a) +_) e₁                        ⟩
        h * (q * a) + r     ＝⟨ ap (_+ r) (mult-associativity h q a ⁻¹)       ⟩
        h * q * a + r       ＝⟨ ap (λ - → - * a + r) (mult-commutativity h q) ⟩
        q * h * a + r       ＝⟨ ap (_+ r) (mult-associativity q h a)          ⟩
        q * (h * a) + r     ＝⟨ ap (λ - → q * - + r) e₀                       ⟩
        q * y + r           ＝⟨ e ⁻¹                                          ⟩
        x                   ∎
  II : (d : ℕ) → is-common-divisor d x y → d ∣ h
  II d ((u , e₂) , v , e₃)  = f d ((v , e₃) , ii)
   where
    i : d * u ＝ d * (q * v) + r
    i = d * u           ＝⟨ e₂                                            ⟩
        x               ＝⟨ e                                             ⟩
        q * y + r       ＝⟨ ap (λ - → q * - + r) (e₃ ⁻¹)                  ⟩
        q * (d * v) + r ＝⟨ ap (_+ r) (mult-associativity q d v ⁻¹)       ⟩
        q * d * v + r   ＝⟨ ap (λ - → - * v + r) (mult-commutativity q d) ⟩
        d * q * v + r   ＝⟨ ap (_+ r) (mult-associativity d q v)          ⟩
        d * (q * v) + r ∎

    ii : d ∣ r
    ii = factor-of-sum-consequence d u (q * v) r i


\end{code}

Now we have the function which computes the highest common factor for any two
natural numbers x and y.  This function uses course-of-values induction in order
to satisfy the Agda termination checker.

The step function includes an induction, which says the following:

If for any number x, we can find a number r with r < x, and for any number k
there exists a highest common factor of r and k, then for any y there exists a
highest common factor of x and y.

\begin{code}

HCF : (x y : ℕ) → Σ h ꞉ ℕ , is-hcf h x y
HCF = course-of-values-induction (λ x → (y : ℕ) → Σ h ꞉ ℕ , is-hcf h x y) step
 where
  step : (x : ℕ)
       → ((r : ℕ) → r < x → (y : ℕ) → Σ h ꞉ ℕ , is-hcf h r y)
       → (y : ℕ)
       → Σ h ꞉ ℕ , is-hcf h x y
  step 0        IH y = y , (everything-divides-zero , ∣-refl) , γ
   where
    γ : (d : ℕ) → is-common-divisor d 0 y → d ∣ y
    γ d (a , b) = b
  step (succ x) IH y = I (division y x)
   where
    I : Σ q ꞉ ℕ , Σ r ꞉ ℕ , (y ＝ q * succ x + r) × (r < succ x)
      → Σ h ꞉ ℕ , is-hcf h (succ x) y
    I (q , r , e₀ , l) = II (IH r l (succ x))
     where
      II : Σ h ꞉ ℕ , is-hcf h r (succ x) → Σ h ꞉ ℕ , is-hcf h (succ x) y
      II (h , h-is-hcf) = h , hcf-comm y (succ x) h ii
       where
        i : is-hcf h (succ x) r
        i = hcf-comm r (succ x) h h-is-hcf

        ii : is-hcf h y (succ x)
        ii = euclids-algorithm-lemma' y (succ x) q r h e₀ i

hcf : (x y : ℕ) → ℕ
hcf x y = pr₁ (HCF x y)

hcf-is-HCF : (x y : ℕ) → is-hcf (hcf x y) x y
hcf-is-HCF x y = pr₂ (HCF x y)

\end{code}

Two numbers being coprime is also a proposition, as a simple
consequence of hcf being a proposition for all values of h.

Two numbers are coprime in the special case that the hcf is 1.

\begin{code}

coprime' : ℕ → ℕ → 𝓤₀ ̇
coprime' x y = hcf x y ＝ 1

coprime'-is-prop : (x y : ℕ) → is-prop (coprime' x y)
coprime'-is-prop _ _ = ℕ-is-set

coprime : (a b : ℕ) → 𝓤₀ ̇
coprime a b = is-hcf 1 a b

coprime-is-prop : Fun-Ext → (a b : ℕ) → is-prop (coprime a b)
coprime-is-prop fe a b = is-hcf-is-prop fe 0 a b

coprime'-to-coprime : (x y : ℕ) → coprime' x y → coprime x y
coprime'-to-coprime x y p = transport (λ - → is-hcf - x y) p (hcf-is-HCF x y)

coprime-0-1 : coprime 0 1
coprime-0-1 = (1-divides-all 0 , 1-divides-all 1) , γ
 where
  γ : (d : ℕ) → is-common-divisor d 0 1 → d ∣ 1
  γ d (_ , d-divides-one) = d-divides-one

divbyhcf' : (a b : ℕ)
          → Σ h ꞉ ℕ , Σ x ꞉ ℕ , Σ y ꞉ ℕ , ((h * x ＝ a) × (h * y ＝ b))
                                        × coprime x y
divbyhcf' 0 b = b , 0 , 1 , (refl , refl) , coprime-0-1
divbyhcf' (succ a) b = γ' (HCF (succ a) b)
 where
  γ' : Σ h ꞉ ℕ , is-hcf h (succ a) b
     → Σ h ꞉ ℕ , Σ x ꞉ ℕ , Σ y ꞉ ℕ , ((h * x ＝ succ a) × (h * y ＝ b))
                                   × coprime x y
  γ' (0 , (p , _) , τ) = 𝟘-elim (zero-does-not-divide-positive a p)
  γ' (succ h , ((x , α) , (y , β)) , τ) = succ h , x , y , (α , β) , γ
   where
    γ₁ : is-common-divisor 1 x y
    γ₁ = 1-divides-all x , 1-divides-all y

    γ₂ : (d : ℕ) → is-common-divisor d x y → d ∣ 1
    γ₂ d ((k , δ) , (l , ψ)) = division-refl-right-factor h d II
     where
      I : (k x a : ℕ)
        → d * k ＝ x
        → succ h * x ＝ a
        → succ h * d ∣ a
      I k x a e₁ e₂ = k , (succ h * d * k  ＝⟨ mult-associativity (succ h) d k ⟩
                          succ h * (d * k) ＝⟨ ap (succ h *_) e₁               ⟩
                          succ h * x       ＝⟨ e₂                              ⟩
                          a ∎)

      II : (succ h * d) ∣ succ h
      II = τ (succ h * d) (I k x (succ a) δ α , I l y b ψ β)

    γ : coprime x y
    γ = γ₁ , γ₂

divbyhcf : (a b : ℕ)
         → Σ h ꞉ ℕ , Σ x ꞉ ℕ , Σ y ꞉ ℕ , ((h * x ＝ a)
                                       × (h * y ＝ b))
                                       × coprime x y
divbyhcf 0 b = b , 0 , 1 , I , II , III
  where
  I : (b * 0 ＝ zero) × (b * 1 ＝ b)
  I = refl , refl
  II : (1 ∣ 0) × (1 ∣ 1)
  II = everything-divides-zero , 1-divides-all 1
  III : (d : ℕ) → is-common-divisor d 0 1 → d ∣ 1
  III d (_ , d-divides-one) = d-divides-one
divbyhcf (succ a) b = I (HCF (succ a) b)
 where
  I : Σ c ꞉ ℕ , is-hcf c (succ a) b
    → Σ h ꞉ ℕ , Σ x ꞉ ℕ , Σ y ꞉ ℕ , ((h * x ＝ succ a)
                                  × (h * y ＝ b))
                                  × coprime x y
  I (0 , ((x , xₚ) , y , yₚ) , τ) = 𝟘-elim (positive-not-zero a II)
   where
    II : succ a ＝ 0
    II = succ a  ＝⟨ xₚ ⁻¹                     ⟩
         0 * x   ＝⟨ mult-commutativity zero x ⟩
         0       ∎
  I (succ h , ((x , xₚ) , y , yₚ) , τ) = succ h , x , y , (xₚ , yₚ) , goal
   where
    II : (f' : ℕ) → is-common-divisor f' x y → f' ∣ 1
    II f' ((α , αₚ) , β , βₚ) = III (τ (succ h * f') ((α , αₚ') , β , βₚ'))
     where
      αₚ' : succ h * f' * α ＝ succ a
      αₚ' = succ h * f' * α     ＝⟨ mult-associativity (succ h) f' α ⟩
            succ h * (f' * α)   ＝⟨ ap (succ h *_) αₚ                ⟩
            succ h * x          ＝⟨ xₚ                               ⟩
            succ a              ∎

      βₚ' : succ h * f' * β ＝ b
      βₚ' = succ h * f' * β   ＝⟨ mult-associativity (succ h) f' β ⟩
            succ h * (f' * β) ＝⟨ ap (succ h *_) βₚ                ⟩
            succ h * y        ＝⟨ yₚ                               ⟩
            b                 ∎

      III : (succ h) * f' ∣ (succ h) → f' ∣ 1
      III (δ , δₚ) = 1 , left-factor-one f' δ γ
       where
        e : succ h * (f' * δ) ＝ succ h * 1
        e = succ h * (f' * δ) ＝⟨ mult-associativity (succ h) f' δ ⁻¹ ⟩
            succ h * f' * δ   ＝⟨ δₚ ⟩
            succ h            ∎

        γ : f' * δ ＝ 1
        γ = mult-left-cancellable (f' * δ) 1 h e

    goal : coprime x y
    goal = (1-divides-all x , 1-divides-all y) , II

hcf-unique : (a b : ℕ)
           → ((h , p) : Σ h ꞉ ℕ , is-hcf h a b)
           → ((h' , p') : Σ h' ꞉ ℕ , is-hcf h' a b)
           → h ＝ h'
hcf-unique a b (h , h-icd , f) (h' , h'-icd , f') = ∣-anti h h' I II
 where
  I : h ∣ h'
  I = f' h h-icd

  II : h' ∣ h
  II = f h' h'-icd

coprime-to-coprime' : (x y : ℕ) → coprime x y → coprime' x y
coprime-to-coprime' x y p = γ
 where
  I : is-hcf (hcf x y) x y
  I = hcf-is-HCF x y

  γ : hcf x y ＝ 1
  γ = hcf-unique x y (hcf x y , I) (1 , p)

\end{code}

The statement "x and y have a highest-common-factor" is also a
proposition. Again, function extensionality is required.

To prove that the hcf is unique, we assume there are two different
hcf's. But by the definition of is-hcf, all common factors are factors
of the hcf, and both hcf's are common factors. Two numbers which are
factors of each other are equal by the anti-symmetric property of
division.

\begin{code}

has-hcf : (x y : ℕ) → 𝓤₀ ̇
has-hcf x y = Σ d ꞉ ℕ , is-hcf (succ d) x y

has-hcf-is-prop : Fun-Ext → (x y : ℕ) → is-prop (has-hcf x y)
has-hcf-is-prop fe x y (h₁ , h₁-hcf) (h₂ , h₂-hcf) = to-subtype-＝ γ₁ γ₂
 where
  γ₁ : (d : ℕ) → is-prop (is-hcf (succ d) x y)
  γ₁ d = is-hcf-is-prop fe d x y

  I : succ h₁ ＝ succ h₂
  I = hcf-unique x y (succ h₁ , h₁-hcf) (succ h₂ , h₂-hcf)

  γ₂ : h₁ ＝ h₂
  γ₂ = succ-lc I

\end{code}
