open import 1Lab.Prelude

open import Data.Nat.Properties
open import Data.Nat.Order
open import Data.Dec.Base
open import Data.Nat.Base
open import Data.Sum.Base

module Data.Nat.Divisible where

Divisibility of natural numbers🔗

In the natural numbers, divisibility¹ is the property expressing that a given number can be expressed as a multiple of another, and we write $a|b$² when there exists some $k$ such that $b=ka\text{.}$

Note the use of an existential quantifier, which is a bit annoying: For divisibility to truly be a property, we must work under a truncation, since otherwise there would be $\mathbb{N}\text{-many}$ proofs that $0|0\text{,}$ since for any $n\text{,}$ we have $0=n0\text{.}$ To avoid this sticky situation, we define divisibility with a single step of indirection:

_∣_ : Nat → Nat → Type
zero  ∣ y = y ≡ zero
suc x ∣ y = fibre (_* suc x) y

infix  _∣_

In this way, we break the pathological case of $0|0$ by decreeing it to be the (contractible) type $0=0\text{.}$ Every other natural number is already handled, because the function “$(1+x)\ast$” is injective. With this indirection, we can prove that divisibility is a mere property:

∣-is-prop : ∀ x y → is-prop (x ∣ y)
∣-is-prop zero y n k = prop!
∣-is-prop (suc x) y (n , p) (n' , q) = Σ-prop-path! (*-suc-inj x n n' (p ∙ sym q))

instance
  H-Level-∣ : ∀ {x y} {n} → H-Level (x ∣ y) (suc n)
  H-Level-∣ = prop-instance (∣-is-prop _ _)
  {-# INCOHERENT H-Level-∣ #-}

The type $x|y$ is, in fact, the propositional truncation of $(\ast x{)}^{-1}(y)$ — and it is logically equivalent to that type, too!

∣-is-truncation : ∀ {x y} → (x ∣ y) ≃ ∥ fibre (_* x) y ∥
∣-is-truncation {zero} {y} =
  prop-ext!
    (λ p → inc (y , *-zeror y ∙ sym p))
    (rec! λ x p → sym p ∙ *-zeror x )
∣-is-truncation {suc x} {y} = Equiv.to is-prop≃equiv∥-∥ (∣-is-prop (suc x) y)

∣→fibre : ∀ {x y} → x ∣ y → fibre (_* x) y
∣→fibre {zero} wit  =  , sym wit
∣→fibre {suc x} wit = wit

fibre→∣ : ∀ {x y} → fibre (_* x) y → x ∣ y
fibre→∣ f = Equiv.from ∣-is-truncation (inc f)

divides : ∀ {x y} (q : Nat) → q * x ≡ y → x ∣ y
divides x p = fibre→∣ (x , p)

As an ordering🔗

The notion of divisibility equips the type $\mathbb{N}$ with yet another partial order, i.e., the relation $x|y$ is reflexive, transitive, and antisymmetric. We can establish the former two directly, but antisymmetry will take a bit of working up to:

∣-refl : ∀ {x} → x ∣ x
∣-refl = divides  (*-onel _)

∣-trans : ∀ {x y z} → x ∣ y → y ∣ z → x ∣ z
∣-trans {zero} {zero} p q = q
∣-trans {zero} {suc y} p q = absurd (suc≠zero p)
∣-trans {suc x} {zero} p q =  , sym q
∣-trans {suc x} {suc y} {z} (k , p) (k' , q) = k' * k , (
  k' * k * suc x   ≡⟨ *-associative k' k (suc x) ⟩≡
  k' * (k * suc x) ≡⟨ ap (k' *_) p ⟩≡
  k' * suc y       ≡⟨ q ⟩≡
  z                ∎)

We note in passing that any number divides zero, and one divides every number.

∣-zero : ∀ {x} → x ∣ 
∣-zero = divides  refl

∣-one : ∀ {x} →  ∣ x
∣-one {x} = divides x (*-oner x)

A more important lemma is that if $x$ divides a non-zero number $y\text{,}$ then $x\le y\text{:}$ the divisors of any positive $y$ are smaller than it. Zero is a sticking point here since, again, any number divides zero!

m∣sn→m≤sn : ∀ {x y} → x ∣ suc y → x ≤ suc y
m∣sn→m≤sn {x} {y} p with ∣→fibre p
... | zero  , p = absurd (zero≠suc p)
... | suc k , p = difference→≤ (k * x) p

m∣n→m≤n : ∀ {m n} .⦃ _ : Positive n ⦄ → m ∣ n → m ≤ n
m∣n→m≤n {n = suc _} = m∣sn→m≤sn

proper-divisor-< : ∀ {m n} .⦃ _ : Positive n ⦄ → m ≠ n → m ∣ n → m < n
proper-divisor-< m≠n m∣n with ≤-strengthen (m∣n→m≤n m∣n)
... | inl here  = absurd (m≠n here)
... | inr there = there

This will let us establish the antisymmetry we were looking for:

∣-antisym : ∀ {x y} → x ∣ y → y ∣ x → x ≡ y
∣-antisym {zero}  {y}     p q = sym p
∣-antisym {suc x} {zero}  p q = absurd (suc≠zero q)
∣-antisym {suc x} {suc y} p q = ≤-antisym (m∣sn→m≤sn p) (m∣sn→m≤sn q)

Elementary properties🔗

Since divisibility is the “is-multiple-of” relation, we would certainly expect a number to divide its multiples. Fortunately, this is the case:

∣-*l : ∀ {x y} → x ∣ x * y
∣-*l {y = y} = fibre→∣ (y , *-commutative y _)

∣-*r : ∀ {x y} → x ∣ y * x
∣-*r {y = y} = fibre→∣ (y , refl)

|-*l-pres : ∀ {n a b} → n ∣ b → n ∣ a * b
|-*l-pres {n} {a} {b} p1 with (q , α) ← ∣→fibre p1 = fibre→∣ (a * q , *-associative a q n ∙ ap (a *_) α)

∣-*-cancelr : ∀ {n a b} .⦃ _ : Positive n ⦄ → a * n ∣ b * n → a ∣ b
∣-*-cancelr {n} {a} {b} p1 with (q , α) ← ∣→fibre p1 = fibre→∣ (q , *-injr n (q * a) b (*-associative q a n ∙ α))

If two numbers are multiples of $k\text{,}$ then so is their sum.

∣-+ : ∀ {k n m} → k ∣ n → k ∣ m → k ∣ (n + m)
∣-+ {zero} {n} {m} p q = ap (_+ m) p ∙ q
∣-+ {suc k} (x , p) (y , q) = x + y , *-distrib-+r x y (suc k) ∙ ap₂ _+_ p q

∣-+-cancel : ∀ {n a b} → n ∣ a → n ∣ a + b → n ∣ b
∣-+-cancel {n} {a} {b} p1 p2 with (q , α) ← ∣→fibre p1 | (r , β) ← ∣→fibre p2 = fibre→∣
  (r - q , monus-distribr r q n ∙ ap₂ _-_ β α ∙ ap ((a + b) -_) (sym (+-zeror a)) ∙ monus-cancell a b )

∣-+-cancel' : ∀ {n a b} → n ∣ b → n ∣ a + b → n ∣ a
∣-+-cancel' {n} {a} {b} p1 p2 = ∣-+-cancel {n} {b} {a} p1 (subst (n ∣_) (+-commutative a b) p2)

The only number that divides 1 is 1 itself:

∣-1 : ∀ {n} → n ∣  → n ≡ 
∣-1 {} p = sym p
∣-1 {} p = refl
∣-1 {suc (suc n)} (k , p) = *-is-oner k ( + n) p

Even and odd natural numbers🔗

A number is even if it is divisible by 2, and odd otherwise. Note that a number is odd if and only if its successor is even; we take this as our definition because it’s easier to compute with positive statements.

is-even : Nat → Type
is-even n =  ∣ n

is-odd : Nat → Type
is-odd n = is-even (suc n)

odd→not-even : ∀ n → is-odd n → ¬ is-even n
odd→not-even n (x , p) (y , q) = 1≠2*n (x - y) $
  monus-swapr  _ _ (ap suc q ∙ sym p) ∙ sym (monus-distribr x y )
  where
    1≠2*n : ∀ n → ¬ ( ≡ n * )
    1≠2*n zero = suc≠zero
    1≠2*n (suc n) h = zero≠suc (suc-inj h)

We can easily decide whether a number is even or odd by induction.

even-or-odd : ∀ n → is-even n ⊎ is-odd n
even-or-odd zero = inl ∣-zero
even-or-odd (suc n) with even-or-odd n
... | inl p = inr (∣-+ ∣-refl p)
... | inr p = inl p

even? : ∀ n → Dec (is-even n)
even? n with even-or-odd n
... | inl e = yes e
... | inr o = no (odd→not-even n o)

See Data.Nat.DivMod for a general decision procedure for divisibility.