Naturals.Division

Andrew Sneap - October - November 2021
Updated May - July 2022

This file defines division of natural numbers as a Σ type. Many common
proofs of properties of division are also provided.


{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan renaming (_+_ to _∔_)

open import Naturals.Addition
open import Naturals.Multiplication
open import Naturals.Properties
open import Naturals.Order
open import Notation.Order
open import UF.DiscreteAndSeparated
open import UF.Subsingletons

module Naturals.Division where


First, we have the definition of division. Division can also be
defined inductively, but as with most definitions I have instead
chosen to express division as a Σ type.


_∣_ : ℕ → ℕ → 𝓤₀ ̇
x ∣ y = Σ a ꞉ ℕ , (x * a ＝ y)


Notice that we cannot prove that (x y : ℕ) → is-prop (x ∣ y).
When x ＝ 0, and y ＝ 0, we can choose any factor a and the identity type holds.

On the other hand, for values x > 0, it is a proposition that x | y.
This is proved using the cancellative property of multiplication of
factors greater than 0.


_∣_-is-prop : (x y : ℕ) → is-prop (succ x ∣ y)
_∣_-is-prop x y (a , p) (b , p') = to-subtype-＝ (λ _ → ℕ-is-set) II
 where
  I : succ x * a ＝ succ x * b
  I = p ∙ p' ⁻¹

  II : a ＝ b
  II = mult-left-cancellable a b x I


Clearly, 1 divides anything, which is easily proved since 1 is the
multiplicative identity of naturals.

0 does not divide any value greater than 0. If this was the case, then
we would have that 0 * a ＝ 0 ＝ succ x, which is a contradiction.

Also, any number divides itself, and divides zero.


1-divides-all : (x : ℕ) → 1 ∣ x
1-divides-all x = x , mult-left-id x

zero-does-not-divide-positive : (x : ℕ) → ¬(0 ∣ succ x)
zero-does-not-divide-positive x (a , p) = positive-not-zero x γ
 where
  γ : succ x ＝ 0
  γ = succ x ＝⟨ p ⁻¹             ⟩
      0 * a  ＝⟨ zero-left-base a ⟩
      0      ∎

∣-refl : {x : ℕ} → x ∣ x
∣-refl = 1 , refl

everything-divides-zero : {x : ℕ} → x ∣ 0
everything-divides-zero = 0 , refl


For natural numbers, division has the property that if x | y and
y | x, then x ＝ y.  This property is used to prove that if the
numerator a of a rational is 0, then the rational is 0.  In order to
prove this, we first need two lemmas.

The first is that if x < y, and x < z, then x < y * z.
This follows as a corollary of <-+.


∣-anti-lemma : (x y z : ℕ) → x < y → x < z → x < y * z
∣-anti-lemma x 0        z        l₁ l₂ = 𝟘-elim (zero-least' z l₁)
∣-anti-lemma x (succ y) 0        l₁ l₂ = 𝟘-elim (zero-least' y l₂)
∣-anti-lemma x (succ y) (succ z) l₁ l₂ = <-+ x (succ y) (succ y * z) l₁


The second is that if the product of two naturals is 1, then the left
argument is 1. Of course, both arguments are 1 by commutativity of
multiplication.

The proof is by case analysis. When x ＝ 1, we are done.
If x ＝ 0, then x * y ＝ 0 ＝ 1, which is a contradiction.
If x > 1, the consider y. In each case, we find a contradiction.


left-factor-one : (x y : ℕ) → x * y ＝ 1 → x ＝ 1
left-factor-one 0 y e = 𝟘-elim (zero-not-positive 0 γ)
 where
  γ : 0 ＝ 1
  γ = zero-left-base y ⁻¹ ∙ e
left-factor-one 1 y e = refl
left-factor-one (succ (succ x)) 0 e = 𝟘-elim (zero-not-positive 0 e)
left-factor-one (succ (succ x)) 1 e = 𝟘-elim (zero-not-positive x γ)
 where
  γ : 0 ＝ succ x
  γ = succ-lc (e ⁻¹)
left-factor-one (succ (succ x)) (succ (succ y)) e = 𝟘-elim γ
 where
  l₁ : 0 < succ x
  l₁ = zero-least (succ x)

  l₂ : 0 < succ y
  l₂ = zero-least (succ y)

  l₃ : 1 < succ (succ x) * succ (succ y)
  l₃ = ∣-anti-lemma 1 (succ (succ x)) (succ (succ y)) l₁ l₂

  γ : 𝟘
  γ = less-than-not-equal _ _ l₃ (e ⁻¹)

division-refl-right-unit : (x y : ℕ) → succ x * y ∣ succ x → y ＝ 1
division-refl-right-unit x y (k , e) = left-factor-one y k II
 where
  I : succ x * (y * k) ＝ succ x * 1
  I = mult-associativity (succ x) y k ⁻¹ ∙ e

  II : y * k ＝ 1
  II = mult-left-cancellable (y * k) 1 x I

division-refl-right-factor : (x y : ℕ) → succ x * y ∣ succ x → y ∣ 1
division-refl-right-factor x y (k , e) = γ
 where
  I : y ＝ 1
  I = division-refl-right-unit x y (k , e)

  II : 1 ∣ 1
  II = 1-divides-all 1

  γ : y ∣ 1
  γ = transport (_∣ 1) (I ⁻¹) II


And we can finally prove that division is anti-symmetric property,
using the two lemmas, and case analysis on y. In the case y ＝ 0, we
have 0 * b ＝ x, and hence x ＝ y ＝ 0.

In the case y > 0, we can use the fact that multiplication is
cancellable, and the hypothesis x * a ＝ succ y, succ y * b ＝ x to
prove that b ＝ 1, and conclude that division is anti-symmetric.



∣-anti : (x y : ℕ) → x ∣ y → y ∣ x → x ＝ y
∣-anti x 0        (a , e₁) (b , e₂) = e₂ ⁻¹ ∙ zero-left-base b
∣-anti x (succ y) (a , e₁) (b , e₂) = e₂ ⁻¹ ∙ ap (succ y *_) b-is-1
 where
  I : succ y * (b * a) ＝ succ y * 1
  I = succ y * (b * a) ＝⟨ mult-associativity (succ y) b a ⁻¹ ⟩
      succ y * b * a   ＝⟨ ap (_* a) e₂ ∙ e₁                  ⟩
      succ y ∎

  b*a-is-1 : b * a ＝ 1
  b*a-is-1 = mult-left-cancellable (b * a) 1 y I

  b-is-1 : b ＝ 1
  b-is-1 = left-factor-one b a b*a-is-1


Division distributes over addition, over multiples, and is
transitive. The proofs are simple and corollaries of the properties of
multiplication.


∣-respects-addition : (x y z : ℕ) → x ∣ y → x ∣ z → x ∣ (y + z)
∣-respects-addition x y z (a , p) (b , q) = (a + b , I)
 where
  I : x * (a + b) ＝ y + z
  I = x * (a + b)   ＝⟨ distributivity-mult-over-addition x a b ⟩
      x * a + x * b ＝⟨ ap (_+ x * b) p                         ⟩
      y + x * b     ＝⟨ ap (y +_) q                             ⟩
      y + z         ∎

∣-divisor-divides-multiple : (a b k : ℕ) → a ∣ b → a ∣ k * b
∣-divisor-divides-multiple a b k (x , p) = (x * k) , I
 where
  I : a * (x * k) ＝ k * b
  I = a * (x * k) ＝⟨ mult-associativity a x k ⁻¹ ⟩
      a * x * k   ＝⟨ ap (_* k) p                 ⟩
      b * k       ＝⟨ mult-commutativity b k      ⟩
      k * b       ∎

∣-respects-multiples : (a b c k l : ℕ) → a ∣ b → a ∣ c → a ∣ (k * b + l * c)
∣-respects-multiples a b c k l p₁ p₂ = ∣-respects-addition a (k * b) (l * c) I II
 where
  I : a ∣ (k * b)
  I = ∣-divisor-divides-multiple a b k p₁
  II : a ∣ (l * c)
  II = ∣-divisor-divides-multiple a c l p₂

∣-trans : (a b c : ℕ) → a ∣ b → b ∣ c → a ∣ c
∣-trans a b c (x , p) (y , q) = (x * y) , I
 where
  I : a * (x * y) ＝ c
  I = a * (x * y)  ＝⟨ mult-associativity a x y ⁻¹ ⟩
      (a * x) * y  ＝⟨ ap ( _* y) p                ⟩
      b * y        ＝⟨ q                           ⟩
      c            ∎


Now we state the division theorem for natural numbers. This states
that for a natural number a and d, there exists a quotient q and
remainder r with a ＝ q * (d + 1) + r, with the remainder r less than
succ d.


division-theorem : (a d : ℕ) → 𝓤₀ ̇
division-theorem a d = Σ q ꞉ ℕ , Σ r ꞉ ℕ , (a ＝ q * succ d + r) × (r < succ d)


There are many ways to compute division on natural numbers. The chosen
method here (mainly to satisfy the termination checker) is to use
natural induction.

To compute (succ d) | a, we do induction on a.

Base: If a ＝ 0, then the quotient and remainder are both 0.

Inductive step: Suppose that (succ d) | k, then there exists q , r
such that k = q * succ d + r, and r < succ d.

We want to show that (succ d) | (succ k).
Since r < succ d, we have that either r < d or r ＝ d.

If r < d, then the quotient remains the same and the remainder
increases by 1. Since r < d, (succ r) < (succ d), and we are done.

If r ＝ d, then the quotient increases by 1 and the remainder is 0.
Clearly, 0 < succ d.  Proving that succ k ＝ succ q + succ q * d
follows from the inductive hypothesis and r ＝ d.


division : (a d : ℕ) → division-theorem a d
division a d = ℕ-induction base step a
 where
  base : Σ q ꞉ ℕ , Σ r ꞉ ℕ , (0 ＝ q * succ d + r) × (r < succ d)
  base = 0 , (0 , (I , II))
   where
    I : 0 ＝ 0 * succ d + 0
    I = 0         ＝⟨ refl                               ⟩
        0 + 0     ＝⟨ ap (0 +_) (zero-left-base d ⁻¹) ⟩
        0 + 0 * d ∎

    II : 0 < succ d
    II = zero-least d

  step : (k : ℕ)
       → Σ q ꞉ ℕ , Σ r ꞉ ℕ , (k ＝ q * succ d + r) × (r < succ d)
       → Σ q ꞉ ℕ , Σ r ꞉ ℕ , (succ k ＝ q * succ d + r) × (r < succ d)
  step k (q , r , e , l) = γ (<-split r d l)
   where
    γ : (r < d) ∔ (r ＝ d)
      →  Σ q ꞉ ℕ , Σ r ꞉ ℕ , (succ k ＝ q * succ d + r) × (r < succ d)
    γ (inl l) = q , succ r , ap succ e , l
    γ (inr e') = succ q , 0 , I , unique-to-𝟙 (0 < succ d)
     where
      I : succ k ＝ succ q + succ q * d
      I = succ k                        ＝⟨ i   ⟩
          succ (q + q * d + r)          ＝⟨ ii  ⟩
          succ (q + q * d + d)          ＝⟨ iii ⟩
          succ (q + (q * d + d))        ＝⟨ iv  ⟩
          succ q + (q * d + d)          ＝⟨ v   ⟩
          succ q + (d * q + d)          ＝⟨ vi  ⟩
          succ q + (d + d * q)          ＝⟨ vii ⟩
          succ q + succ q * d           ∎
       where
        i   = ap succ e
        ii  = ap succ (ap (q + q * d +_) e')
        iii = ap succ (addition-associativity q (q * d) d)
        iv  = succ-left q (q * d + d) ⁻¹
        v   = ap (succ q +_) (ap (_+ d) (mult-commutativity q d))
        vi  = ap (succ q +_) (addition-commutativity (d * q) d)
        vii = ap (succ q +_) (mult-commutativity d (succ q))


The division theorem is clearly a proposition.

First, we fix the quotient, and prove that the remainder is unique.

That is, if we have that a ＝ q * succ d + r, and
                         a ＝ q * succ d + r', then r ＝ r'.
This is easy to prove using cancellation of addition.


division-is-prop' : (a d q : ℕ)
                  → is-prop (Σ r ꞉ ℕ , (a ＝ q * succ d + r) × r < succ d)
division-is-prop' a d q (r₀ , e₀ , l₀) (r₁ , e₁ , l₁) = γ
  where
   γ₁ : (r : ℕ) → is-prop ((a ＝ q * succ d + r) × r < succ d)
   γ₁ r = ×-is-prop ℕ-is-set (<-is-prop-valued r (succ d))

   I : q * succ d + r₀ ＝ q * succ d + r₁
   I = q * succ d + r₀ ＝⟨ e₀ ⁻¹ ⟩
       a               ＝⟨ e₁    ⟩
       q * succ d + r₁ ∎

   γ₂ : r₀ ＝ r₁
   γ₂ = addition-left-cancellable r₀ r₁ (q * succ d) I

   γ : r₀ , e₀ , l₀ ＝ r₁ , e₁ , l₁
   γ = to-subtype-＝ γ₁ γ₂


To conclude that the division theorem is a proposition, we use
trichotomy on the two quotient values q₀ and q₁.

When q₀ ＝ q₁, we are done.

In either of two cases, we can generalise a contradiction proof, which
is done in division-is-prop-lemma.

The idea of the proof is as follows:

We have that:
r₀ ≤ d,
r₁ ≤ d,
q₀ < q₁

a ＝ q₀ * succ d + r₀,
a ＝ q₁ * succ d + r₁,

Hence we have that

q₀ + k ＝ q₁, with k > 0
q₀ * succ d + r₀ ＝ q₁ * succ d + r₁
                 ＝ (q₀ + k) * succ d + r₁
                 ＝ (q₀ * d) + k * succ d + r₁
Now, r₀ ＝ k * succ d + r₁
   ⇒ k * succ d + r₁ ≤ d    (since r₀ ≤ d)
   ⇒ k * succ d ≤ d
   ⇒ succ d ≤ d, and hence we have a contradiction.


division-is-prop-lemma : (a d q₀ q₁ r₀ r₁ : ℕ)
                       → r₀ ≤ d
                       → a ＝ q₀ * succ d + r₀
                       → a ＝ q₁ * succ d + r₁
                       → ¬ (q₀ < q₁)
division-is-prop-lemma a d q₀ q₁ r₀ r₁ l₁ e₁ e₂ l₂ = not-less-than-itself d γ
 where
  t : Σ k ꞉ ℕ , k + succ q₀ ＝ q₁
  t = subtraction (succ q₀) q₁ l₂

  k = pr₁ t
  e₃ = pr₂ t

  I : q₀ * succ d + r₀ ＝ q₀ * succ d + (succ k * succ d + r₁)
  I = q₀ * succ d + r₀                     ＝⟨ e₁ ⁻¹ ⟩
      a                                    ＝⟨ e₂    ⟩
      q₁ + q₁ * d + r₁                     ＝⟨refl⟩
      q₁ * succ d + r₁                     ＝⟨ i     ⟩
      succ (k + q₀) * succ d + r₁          ＝⟨ ii    ⟩
      (q₀ + succ k) * succ d + r₁          ＝⟨ iii   ⟩
      q₀ * succ d + succ k * succ d + r₁   ＝⟨ iv    ⟩
      q₀ * succ d + (succ k * succ d + r₁) ∎
   where
    i   = ap (λ - → - * succ d + r₁) (e₃ ⁻¹)
    ii  = ap (λ - → succ - * succ d + r₁) (addition-commutativity k q₀)
    iii = ap (_+ r₁) (distributivity-mult-over-addition' q₀ (succ k) (succ d))
    iv  = addition-associativity (q₀ * succ d) (succ k * succ d) r₁

  II : r₀ ＝ succ k * succ d + r₁
  II = addition-left-cancellable r₀ (succ k * succ d + r₁) (q₀ * succ d)  I

  III : succ k * succ d + r₁ ≤ d
  III = transport (_≤ d) II l₁

  IV : succ k * succ d ≤ succ k * succ d + r₁
  IV = ≤-+ (succ k * succ d) r₁

  V : succ k * succ d ≤ d
  V = ≤-trans (succ k * succ d) (succ k * succ d + r₁) d IV III

  VI : succ d * succ k ≤ d
  VI = transport (_≤ d) (mult-commutativity (succ k) (succ d)) V

  γ : succ d ≤ d
  γ = product-order-cancellable (succ d) k d VI

division-is-prop : (a d : ℕ) → is-prop (division-theorem a d)
division-is-prop a d (q₀ , r₀ , e₀ , l₀) (q₁ , r₁ , e₁ , l₁) = γ I
 where
  I : (q₀ < q₁) ∔ (q₀ ＝ q₁) ∔ (q₁ < q₀)
  I = <-trichotomous q₀ q₁

  γ : (q₀ < q₁) ∔ (q₀ ＝ q₁) ∔ (q₁ < q₀)
    → q₀ , r₀ , e₀ , l₀ ＝ q₁ , r₁ , e₁ , l₁
  γ (inl l)       = 𝟘-elim (division-is-prop-lemma a d q₀ q₁ r₀ r₁ l₀ e₀ e₁ l)
  γ (inr (inl e)) = to-subtype-＝ (division-is-prop' a d) e
  γ (inr (inr l)) = 𝟘-elim (division-is-prop-lemma a d q₁ q₀ r₁ r₀ l₁ e₁ e₀ l)


A property of division which is sometimes useful is the following.
If a * b ＝ a * c + d. If we were considering integers, this would be
easy to prove by simply by rewriting the equation as a * (b - c) ＝
d. With natural numbers, instead use induction on b and c.

If c ＝ 0, we are done, since a * b ∣ d.
If b ＝ 0, then 0 ＝ a * c + d, and hence d ＝ 0, and a * 0 ＝ 0, and we are done.
If b , c > 0, then we use induction.
The inductive hypothesis is: a * b       ＝ a * c       + d → a ∣ d,
                 and we have a * (b + 1) ＝ a * (c + 1) + d.

Since addition is left cancellable, we can find that a * b ＝ a * c + d and we
are done.


factor-of-sum-consequence : (a b c d : ℕ) → a * b ＝ a * c + d → a ∣ d
factor-of-sum-consequence a b 0 d e = b , γ
 where
  γ : a * b ＝ d
  γ = a * b     ＝⟨ e                   ⟩
      a * 0 + d ＝⟨ zero-left-neutral d ⟩
      d         ∎
factor-of-sum-consequence a 0 (succ c) d e = 0 , γ
 where
  γ : 0 ＝ d
  γ = sum-to-zero-gives-zero (a * succ c) d (e ⁻¹) ⁻¹
factor-of-sum-consequence a (succ b) (succ c) d e = γ
  where
   I : a * succ b ＝ a + (a * c + d)
   I = a * succ b      ＝⟨ e                                  ⟩
       a * succ c + d  ＝⟨ addition-associativity a (a * c) d ⟩
       a + (a * c + d) ∎

   II : a * b ＝ a * c + d
   II = addition-left-cancellable (a * b) (a * c + d) a I

   γ : a ∣ d
   γ = factor-of-sum-consequence a b c d II