module Data.Nat.Divisible where

DivisibilityπŸ”—

In the natural numbers, divisibility1 is the property expressing that a given number can be expressed as a multiple of another, and we write a∣ba | b2 when there exists some kk such that b=kab = ka.

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 N\mathbb{N}-many proofs that 0∣00 | 0, since for any nn, we have 0=n00 = n0. 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 5 _∣_

In this way, we break the pathological case of 0∣00 | 0 by decreeing it to be the (contractible) type 0=00 = 0. Every other natural number is already handled, because the function β€œ(1+x)βˆ—(1 + x) *” 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 _ _)

The type x∣yx | y is, in fact, the propositional truncation of (βˆ—x)βˆ’1(y)(* 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  = 0 , 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 N\mathbb{N} with yet another partial order, i.e., the relation x∣yx | 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 1 (*-onel _)

∣-trans : βˆ€ {x y z} β†’ x ∣ y β†’ y ∣ z β†’ x ∣ z
∣-trans {zero} {zero} p q = q
∣-trans {zero} {suc y} p q = absurd (zeroβ‰ suc (sym p))
∣-trans {suc x} {zero} p q = 0 , 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 ∣ 0
∣-zero = divides 0 refl

∣-one : βˆ€ {x} β†’ 1 ∣ x
∣-one {x} = divides x (*-oner x)

A more important lemma is that if xx divides a non-zero number yy, then x≀yx \le y: the divisors of any positive yy 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

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 (zeroβ‰ suc (sym 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)

  1. Not to be confused with a proper division algorithm.β†©οΈŽ

  2. read β€œa divides bβ€β†©οΈŽ