module Data.Nat.Divisible.GCD where

Greatest common divisorsπŸ”—

The greatest common divisor of a pair of natural numbers is the largest number which divides them both. The definition we use is slightly unorthodox, since it requires only that the GCD be the greatest in the divisibility ordering, but the divisibility ordering is finer than the usual ordering, so this will turn out to imply they are greatest in magnitude, as well.

We start by defining what it means for a number to be a GCD β€” that is, we start by defining the graph of the function Only after will we show that such a function exists.

record is-gcd (x y : Nat) (gcd : Nat) : Type where
    gcd-∣l : gcd ∣ x
    gcd-∣r : gcd ∣ y
    greatest : βˆ€ {g'} β†’ g' ∣ x β†’ g' ∣ y β†’ g' ∣ gcd

open is-gcd

is-gcd-is-prop : βˆ€ {x y z} β†’ is-prop (is-gcd x y z)
is-gcd-is-prop p q i .gcd-∣l = ∣-is-prop _ _ (p .gcd-∣l) (q .gcd-∣l) i
is-gcd-is-prop p q i .gcd-∣r = ∣-is-prop _ _ (p .gcd-∣r) (q .gcd-∣r) i
is-gcd-is-prop p q i .greatest a b = ∣-is-prop _ _ (p .greatest a b) (q .greatest a b) i

  H-Level-is-gcd : βˆ€ {x y z n} β†’ H-Level (is-gcd x y z) (suc n)
  H-Level-is-gcd = prop-instance is-gcd-is-prop

GCD : Nat β†’ Nat β†’ Type
GCD a b = Ξ£ _ (is-gcd a b)

GCD-is-prop : βˆ€ {a b} β†’ is-prop (GCD a b)
GCD-is-prop (_ , p) (_ , q) = Ξ£-prop-path! $
  ∣-antisym (q .greatest (p .gcd-∣l) (p .gcd-∣r)) (p .greatest (gcd-∣l q) (gcd-∣r q))

  : βˆ€ {x y g : Nat}
  β†’ is-gcd x y (suc g)
  β†’ βˆ€ {g'} β†’ g' ∣ x β†’ g' ∣ y
  β†’ g' ≀ suc g
GCD-magnitude gcd Ξ± Ξ² = m∣snβ†’m≀sn (gcd .greatest Ξ± Ξ²)

The following observations may seem trivial, but it will come in super handy later: If then the GCD of and is Similarly, the GCD function is β€œsymmetric”, meaning

dividesβ†’GCD : βˆ€ {x y} β†’ x ∣ y β†’ GCD x y
divides→GCD {x} {y} w = x , gcd where
  gcd : is-gcd x y x
  gcd .gcd-∣l = ∣-refl
  gcd .gcd-∣r = w
  gcd .greatest g'∣x g'∣y = g'∣x

GCD-sym : βˆ€ {x y} β†’ GCD x y β†’ GCD y x
GCD-sym w .fst = w .fst
GCD-sym w .snd .gcd-∣l = w .snd .gcd-∣r
GCD-sym w .snd .gcd-∣r = w .snd .gcd-∣l
GCD-sym w .snd .greatest g'∣y g'∣x = w .snd .greatest g'∣x g'∣y

Euclid’s algorithmπŸ”—

To compute greatest common divisors, we use the familiar (recursive) Euclidean algorithm: and otherwise. The difficulty comes in when we want not only to compute the numbers (in which case the definition above is perfectly cromulent), but also to show that they are greatest common divisors.

module Euclid where
  private variable
    n m k d d' : Nat

The base case can be established using our existing functions:

  is-gcd-0 : is-gcd n 0 n
  is-gcd-0 .gcd-∣l = ∣-refl
  is-gcd-0 .gcd-∣r = ∣-zero
  is-gcd-0 .greatest g'∣n g∣n = g'∣n

The inductive step is a bit more complicated. We first have to establish (using the most tedious of arithmetic properties) the following properties of the divisibility relation:

  • If is nonzero, and then
  • If is nonzero, and then

These two facts, incarnated in the following helper lemmas lem₁ and lemβ‚‚, will allow us to compute the inductive step for GCD.

    lem₁ : fibre (_* d) (suc n) β†’ fibre (_* d) (m % suc n) β†’ fibre (_* d) m
    lem₁ {d = d} {n} {m} (c₁ , p) (cβ‚‚ , q) = dm.q * c₁ + cβ‚‚ , r where
      module dm = DivMod (divide-pos m (suc n)) renaming (quot to q ; rem to r)
      r =
        (dm.q * c₁ + cβ‚‚) * d   β‰‘βŸ¨ *-distrib-+r (dm.q * c₁) _ _ βŸ©β‰‘
        dm.q * c₁ * d + ⌜ cβ‚‚ * d ⌝ β‰‘βŸ¨ ap! q βŸ©β‰‘
        ⌜ dm.q * c₁ * d ⌝ + dm.r   β‰‘βŸ¨ ap! (*-associative dm.q c₁ d) βŸ©β‰‘
        dm.q * ⌜ c₁ * d ⌝ + dm.r   β‰‘βŸ¨ ap! p βŸ©β‰‘
        dm.q * suc n + dm.r        β‰‘Λ˜βŸ¨ is-divmod m (suc n) βŸ©β‰‘Λ˜
        m                          ∎

    lemβ‚‚ : fibre (_* d) (suc n) β†’ fibre (_* d) m β†’ fibre (_* d) (m % suc n)
    lemβ‚‚ {d = d} {n} {m} (c₁ , p) (cβ‚‚ , q) = cβ‚‚ - dm.q * c₁ , r where
      module dm = DivMod (divide-pos m (suc n)) renaming (quot to q ; rem to r)
      r = (cβ‚‚ - dm.q * c₁) * d                   β‰‘βŸ¨ monus-distribr cβ‚‚ (dm.q * c₁) d βŸ©β‰‘
          cβ‚‚ * d - ⌜ dm.q * c₁ * d ⌝             β‰‘βŸ¨ ap! (*-associative dm.q c₁ d βˆ™ ap (dm.q *_) p) βŸ©β‰‘
          ⌜ cβ‚‚ * d ⌝ - dm.q * suc n              β‰‘βŸ¨ ap! (q βˆ™ is-divmod m (suc n)) βŸ©β‰‘
          ⌜ dm.q * suc n + dm.r ⌝ - dm.q * suc n β‰‘βŸ¨ ap! (+-commutative (dm.q * suc n) dm.r) βŸ©β‰‘
          (dm.r + dm.q * suc n) - dm.q * suc n   β‰‘βŸ¨ monus-cancelr dm.r 0 (dm.q * suc n) βŸ©β‰‘
          dm.r                                   ∎

That step is put together here: It says that, if ( is nonzero and) then too β€” so that it will suffice to compute the former if we want the latter.

  is-gcd-step : is-gcd (suc n) (m % suc n) d β†’ is-gcd m (suc n) d
  is-gcd-step x .gcd-∣l = fibreβ†’βˆ£ (lem₁ (βˆ£β†’fibre (x .gcd-∣l)) (βˆ£β†’fibre (x .gcd-∣r)))
  is-gcd-step x .gcd-∣r = x .gcd-∣l
  is-gcd-step x .greatest g'∣m g'∣sucn =
    x .greatest g'∣sucn (fibreβ†’βˆ£ (lemβ‚‚ (βˆ£β†’fibre g'∣sucn) (βˆ£β†’fibre g'∣m)))

Actually putting this together is a bit indirect, since we are not performing structural induction: Agda can’t see that the argument is less than We can, however, turn this into well-founded recursion, which demands only that the recursive call be less (in the sense of than the original input.

  euclid-< : βˆ€ y x β†’ x < y β†’ GCD y x
  euclid-< = Wf-induction _ <-wf _ Ξ» where
     x rec zero p    β†’ x , is-gcd-0
     x rec (suc y) p β†’
      let (d , step) = rec (suc y) p (x % suc y) (x%y<y x (suc y))
       in d , is-gcd-step step

With a handy wrapper to put the arguments in the order our induction worker euclid-< expects, we can create the euclid function, together with its numerical component gcd, and a proof that the graph of gcd is indeed is-gcd.

  euclid : βˆ€ x y β†’ GCD x y
  euclid x y with ≀-split y x
  ... | inl y<x       = euclid-< x y y<x
  ... | inr (inl x<y) = GCD-sym (euclid-< y x x<y)
  ... | inr (inr y=x) = dividesβ†’GCD (subst (x ∣_) (sym y=x) ∣-refl)

gcd : Nat β†’ Nat β†’ Nat
gcd x y = Euclid.euclid x y .fst

is-gcd-graphs-gcd : βˆ€ {m n d} β†’ is-gcd m n d ≃ (gcd m n ≑ d)
is-gcd-graphs-gcd {m = m} {n} {d} = prop-ext!
  (Ξ» x β†’ ap fst $ GCD-is-prop (gcd m n , Euclid.euclid m n .snd) (d , x))
  (Ξ» p β†’ subst (is-gcd m n) p (Euclid.euclid m n .snd))