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