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 2 when there exists some such that
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 proofs that since for any we have To avoid this sticky situation, we define divisibility with a single step of indirection:
_∣_ : Nat → Nat → Type
= y ≡ zero
zero ∣ y = fibre (_* suc x) y
suc x ∣ y
infix 5 _∣_
In this way, we break the pathological case of by decreeing it to be the (contractible) type Every other natural number is already handled, because the function “” is injective. With this indirection, we can prove that divisibility is a mere property:
: ∀ x y → is-prop (x ∣ y)
∣-is-prop = prop!
∣-is-prop zero y n k (suc x) y (n , p) (n' , q) = Σ-prop-path! (*-suc-inj x n n' (p ∙ sym q))
∣-is-prop
instance
: ∀ {x y} {n} → H-Level (x ∣ y) (suc n)
H-Level-∣ = prop-instance (∣-is-prop _ _)
H-Level-∣ {-# INCOHERENT H-Level-∣ #-}
The type is, in fact, the propositional truncation of — and it is logically equivalent to that type, too!
: ∀ {x y} → (x ∣ y) ≃ ∥ fibre (_* x) y ∥
∣-is-truncation {zero} {y} =
∣-is-truncation
prop-ext!(λ p → inc (y , *-zeror y ∙ sym p))
(rec! λ x p → sym p ∙ *-zeror x )
{suc x} {y} = Equiv.to is-prop≃equiv∥-∥ (∣-is-prop (suc x) y)
∣-is-truncation
: ∀ {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→∣ = Equiv.from ∣-is-truncation (inc f)
fibre→∣ f
: ∀ {x y} (q : Nat) → q * x ≡ y → x ∣ y
divides = fibre→∣ (x , p) divides x p
As an ordering🔗
The notion of divisibility equips the type with yet another partial order, i.e., the relation is reflexive, transitive, and antisymmetric. We can establish the former two directly, but antisymmetry will take a bit of working up to:
: ∀ {x} → x ∣ x
∣-refl = divides 1 (*-onel _)
∣-refl
: ∀ {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 = 0 , sym q
∣-trans {suc x} {suc y} {z} (k , p) (k' , q) = k' * k , (
∣-trans (suc x) ⟩
k' * k * suc x ≡⟨ *-associative k' k (k * suc x) ≡⟨ ap (k' *_) p ⟩
k' *
k' * suc y ≡⟨ q ⟩) z ∎
We note in passing that any number divides zero, and one divides every number.
: ∀ {x} → x ∣ 0
∣-zero = divides 0 refl
∣-zero
: ∀ {x} → 1 ∣ x
∣-one {x} = divides x (*-oner x) ∣-one
A more important lemma is that if divides a non-zero number then the divisors of any positive are smaller than it. Zero is a sticking point here since, again, any number divides zero!
: ∀ {x y} → x ∣ suc y → x ≤ suc y
m∣sn→m≤sn {x} {y} p with ∣→fibre p
m∣sn→m≤sn ... | zero , p = absurd (zero≠suc p)
... | suc k , p = difference→≤ (k * x) p
This will let us establish the antisymmetry we were looking for:
: ∀ {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) ∣-antisym
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:
: ∀ {x y} → x ∣ x * y
∣-*l {y = y} = fibre→∣ (y , *-commutative y _)
∣-*l
: ∀ {x y} → x ∣ y * x
∣-*r {y = y} = fibre→∣ (y , refl) ∣-*r
If two numbers are multiples of 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 ∣-+
Even and odd 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.
: Nat → Type
is-even = 2 ∣ n
is-even n
: Nat → Type
is-odd = is-even (suc n)
is-odd n
: ∀ n → is-odd n → ¬ is-even n
odd→not-even (x , p) (y , q) = 1≠2*n (x - y) $
odd→not-even n 1 _ _ (ap suc q ∙ sym p) ∙ sym (monus-distribr x y 2)
monus-swapr where
: ∀ n → ¬ (1 ≡ n * 2)
1≠2*n = suc≠zero
1≠2*n zero (suc n) h = zero≠suc (suc-inj h) 1≠2*n
We can easily decide whether a number is even or odd by induction.
: ∀ n → is-even n ⊎ is-odd n
even-or-odd = inl ∣-zero
even-or-odd zero (suc n) with even-or-odd n
even-or-odd ... | inl p = inr (∣-+ ∣-refl p)
... | inr p = inl p
: ∀ n → Dec (is-even n)
even? with even-or-odd n
even? n ... | inl e = yes e
... | inr o = no (odd→not-even n o)
See Data.Nat.DivMod
for a general decision procedure for divisibility.