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π

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
zero  β£ y = y β‘ zero
suc x β£ y = fibre (_* 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:

β£-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 is, in fact, the propositional truncation of β 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 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:

β£-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 (sucβ zero 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 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!

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 (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)


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.

is-even : Nat β Type
is-even n = 2 β£ 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 1 _ _ (ap suc q β sym p) β sym (monus-distribr x y 2)
where
1β 2*n : β n β Β¬ (1 β‘ n * 2)
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.

1. Not to be confused with a proper division algorithm.β©οΈ