Andrew Sneap, 27 April 2021
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import MLTT.Spartan renaming (_+_ to _∔_)
open import Naturals.Addition renaming (_+_ to _ℕ+_)
open import Naturals.Properties
open import Naturals.Order
open import Notation.Order
open import UF.Base
open import UF.Subsingletons
open import Integers.Addition
open import Integers.Type
open import Integers.Negation
open import Integers.Order
open import Integers.Multiplication renaming (_*_ to _ℤ*_)
open import Naturals.Division renaming (_∣_ to _ℕ∣_)
open import Naturals.Multiplication renaming (_*_ to _ℕ*_)
module Integers.Division where
_∣_ : ℤ → ℤ → 𝓤₀ ̇
a ∣ b = Σ x ꞉ ℤ , a ℤ* x ＝ b
_ℤ∣_-is-prop : (a b : ℤ) → not-zero a → is-prop (a ∣ b)
_ℤ∣_-is-prop a b nz (x , p) (x' , p') = to-subtype-＝ (λ _ → ℤ-is-set) II
where
I : x ℤ* a ＝ x' ℤ* a
I = x ℤ* a ＝⟨ ℤ*-comm x a ⟩
a ℤ* x ＝⟨ p ⟩
b ＝⟨ p' ⁻¹ ⟩
a ℤ* x' ＝⟨ ℤ*-comm a x' ⟩
x' ℤ* a ∎
II : x ＝ x'
II = ℤ-mult-right-cancellable x x' a nz I
div-equiv-to-pos-div : (a b : ℕ) → a ℕ∣ b → pos a ∣ pos b
div-equiv-to-pos-div a b (x , p) = pos x , goal
where
goal : pos a ℤ* pos x ＝ pos b
goal = pos a ℤ* pos x ＝⟨ pos-multiplication-equiv-to-ℕ a x ⟩
pos (a ℕ* x) ＝⟨ ap pos p ⟩
pos b ∎
sign-split : (x : ℤ) → positive x ∔ negative x
sign-split (pos x) = inl ⋆
sign-split (negsucc x) = inr ⋆
pos-div-to-nat-div : (a b : ℕ) → pos a ∣ pos b → a ℕ∣ b
pos-div-to-nat-div a b (pos x , p) = x , pos-lc I
where
I : pos (a ℕ* x) ＝ pos b
I = pos (a ℕ* x) ＝⟨ pos-multiplication-equiv-to-ℕ a x ⁻¹ ⟩
pos a ℤ* pos x ＝⟨ p ⟩
pos b ∎
pos-div-to-nat-div a 0 (negsucc x , p) = 0 , refl
pos-div-to-nat-div 0 (succ b) (negsucc x , p) = 𝟘-elim γ
where
I : pos (succ b) ＝ pos 0
I = pos (succ b) ＝⟨ p ⁻¹ ⟩
pos 0 ℤ* negsucc x ＝⟨ ℤ-zero-left-base (negsucc x) ⟩
pos 0 ∎
γ : 𝟘
γ = positive-not-zero b (pos-lc I)
pos-div-to-nat-div (succ a) (succ b) (negsucc x , p) = 𝟘-elim γ
where
γ : 𝟘
γ = product-positive-negative-not-positive (succ a) x b p
\end{code}
TODO : Break apart ℤ-division into 4 subproofs
\begin{code}
ℤ-division : (a : ℤ) → (d : ℕ)
→ Σ q ꞉ ℤ , Σ r ꞉ ℕ , (a ＝ q ℤ* pos (succ d) + pos r) × r < succ d
ℤ-division (pos a) d = f (division a d)
where
f : Σ q ꞉ ℕ , Σ r ꞉ ℕ , (a ＝ q ℕ* succ d ℕ+ r) × r < succ d
→ Σ q ꞉ ℤ , Σ r ꞉ ℕ , (pos a ＝ q ℤ* pos (succ d) + pos r) × r < succ d
f (q , r , e , l) = (pos q) , r , I , l
where
I : pos a ＝ pos q ℤ* pos (succ d) + pos r
I = pos a ＝⟨ ap pos e ⟩
pos (q ℕ* succ d ℕ+ r) ＝⟨ i ⟩
pos (q ℕ* succ d) + pos r ＝⟨ ii ⟩
pos q ℤ* pos (succ d) + pos r ∎
where
i = distributivity-pos-addition (q ℕ* (succ d)) r ⁻¹
ii = ap (_+ pos r) (pos-multiplication-equiv-to-ℕ q (succ d) ⁻¹)
ℤ-division (negsucc a) d = f (division (succ a) d)
where
a' = negsucc a
d' = succ d
f : Σ q ꞉ ℕ , Σ r ꞉ ℕ , (succ a ＝ q ℕ* d' ℕ+ r) × r < d'
→ Σ q ꞉ ℤ , Σ r ꞉ ℕ , (a' ＝ q ℤ* pos d' + pos r) × r < d'
f (0 , 0 , e , l) = 𝟘-elim (positive-not-zero a I)
where
I : succ a ＝ 0
I = succ a ＝⟨ e ⟩
0 ℕ* d' ℕ+ 0 ＝⟨ zero-left-base d' ⟩
0 ∎
f (succ q , 0 , e , l) = negsucc q , 0 , I , l
where
I : a' ＝ negsucc q ℤ* pos d'
I = a' ＝⟨ refl ⟩
- pos (succ a) ＝⟨ i ⟩
- pos (succ q ℕ* d') ＝⟨ ii ⟩
- pos (succ q) ℤ* pos d' ＝⟨ iii ⟩
(- pos (succ q)) ℤ* pos d' ＝⟨ refl ⟩
negsucc q ℤ* pos d' ∎
where
i = ap -_ (ap pos e)
ii = ap -_ (pos-multiplication-equiv-to-ℕ (succ q) d' ⁻¹)
iii = negation-dist-over-mult' (pos (succ q)) (pos d') ⁻¹
f (0 , succ r , e₁ , l₁) = negsucc 0 , I (subtraction' (succ r) (succ d) l₁)
where
n1 : ℤ
n1 = negsucc 0
I : Σ k ꞉ ℕ , k ℕ+ succ r ＝ succ d
→ Σ r ꞉ ℕ , (a' ＝ n1 ℤ* pos (succ d) + pos r) × r < succ d
I (k , e₂) = k , III (cosubtraction k d (r , succ-lc II))
where
k' = pos k
II : succ (r ℕ+ k) ＝ succ d
II = succ (r ℕ+ k) ＝⟨ ap succ (addition-commutativity r k) ⟩
succ (k ℕ+ r) ＝⟨ e₂ ⟩
succ d ∎
III : k < succ d
→ (a' ＝ n1 ℤ* pos (succ d) + k')
× k < succ d
III l₂ = V , l₂
where
IV : succ a ＝ succ r
IV = succ a ＝⟨ e₁ ⟩
0 ℕ* succ d ℕ+ succ r ＝⟨ i ⟩
succ (0 ℕ+ r) ＝⟨ ii ⟩
succ r ∎
where
i = ap succ (ap (_ℕ+ r) (zero-left-base (succ d)))
ii = ap succ (zero-left-neutral r)
V : a' ＝ n1 ℤ* pos (succ d) + k'
V = a' ＝⟨ i ⟩
negsucc r ＝⟨ ii ⟩
pos 0 + negsucc r ＝⟨ iii ⟩
k' + (- k') + negsucc r ＝⟨ iv ⟩
k' + ((- k') + negsucc r) ＝⟨ v ⟩
(- k') + negsucc r + k' ＝⟨ vi ⟩
n1 ℤ* k' + (- pos (succ r)) + k' ＝⟨ vii ⟩
n1 ℤ* k' + n1 ℤ* pos (succ r) + k' ＝⟨ viii ⟩
n1 ℤ* (k' + pos (succ r)) + k' ＝⟨ ix ⟩
n1 ℤ* pos (k ℕ+ succ r) + k' ＝⟨ x ⟩
n1 ℤ* pos (succ d) + k' ∎
where
i = ap negsucc (succ-lc IV)
ii = ℤ-zero-left-neutral (negsucc r) ⁻¹
iii = ap (_+ (negsucc r)) (ℤ-sum-of-inverse-is-zero k' ⁻¹)
iv = ℤ+-assoc k' (- k') (negsucc r)
v = ℤ+-comm k' ((- k') + negsucc r)
vi = ap (λ z → (z + negsucc r) + k') (mult-negation k')
vii = ap (λ z → (n1 ℤ* k' + z) + k') (mult-negation (pos (succ r)))
viii = ap (_+ k') (distributivity-mult-over-ℤ' k' (pos (succ r)) n1 ⁻¹)
ix = ap (λ z → n1 ℤ* z + k') (distributivity-pos-addition k (succ r))
x = ap (λ z → n1 ℤ* pos z + k') e₂
f (succ q , succ r , e₁ , l₁) = negsucc (succ q) , γ
where
I : Σ k ꞉ ℕ , k ℕ+ succ r ＝ d'
→ Σ r ꞉ ℕ , (a' ＝ negsucc (succ q) ℤ* pos d' + pos r) × r < d'
I (k , e₂) = k , III (cosubtraction k d (r , succ-lc II))
where
k' = pos k
q' = pos (succ q)
II : succ (r ℕ+ k) ＝ d'
II = succ (r ℕ+ k) ＝⟨ ap succ (addition-commutativity r k) ⟩
succ (k ℕ+ r) ＝⟨ e₂ ⟩
d' ∎
III : k < d' → (a' ＝ negsucc (succ q) ℤ* pos d' + k') × k < d'
III l₂ = V , l₂
where
IV : - pos (succ r) ＝ k' - pos d'
IV = - pos (succ r) ＝⟨ refl ⟩
negsucc r ＝⟨ i ⟩
pos 0 + negsucc r ＝⟨ ii ⟩
k' + (- k') + negsucc r ＝⟨ iii ⟩
k' + ((- k') - pos (succ r)) ＝⟨ iv ⟩
k' - (k' + pos (succ r)) ＝⟨ v ⟩
k' - pos (k ℕ+ succ r) ＝⟨ vi ⟩
k' - pos d' ∎
where
i = ℤ-zero-left-neutral (negsucc r) ⁻¹
ii = ap (_+ negsucc r) (ℤ-sum-of-inverse-is-zero k' ⁻¹)
iii = ℤ+-assoc k' (- k') (negsucc r)
iv = ap (k' +_) (negation-dist k' (pos (succ r)))
v = ap (λ z → k' - z) (distributivity-pos-addition k (succ r))
vi = ap (λ z → k' - pos z) e₂
V : a' ＝ negsucc (succ q) ℤ* pos d' + k'
V = a' ＝⟨ refl ⟩
- pos (succ a) ＝⟨ ap -_ (ap pos e₁) ⟩
- pos (succ q ℕ* d' ℕ+ succ r) ＝⟨ i ⟩
- (pos (succ q ℕ* d') + pos (succ r)) ＝⟨ ii ⟩
(- pos (succ q ℕ* d')) - pos (succ r) ＝⟨ iii ⟩
(- q' ℤ* pos d') - pos (succ r) ＝⟨ iv ⟩
(- q' ℤ* pos d') + (k' - pos d') ＝⟨ v ⟩
(- q' ℤ* pos d') - pos d' + k' ＝⟨ vi ⟩
(- pos d' ℤ* q') - pos d' + k' ＝⟨ vii ⟩
(- pos d') ℤ* q' - pos d' + k' ＝⟨ viii ⟩
(- pos d') ℤ* q' - pos d' ℤ* pos 1 + k' ＝⟨ ix ⟩
(- pos d') ℤ* (q' + pos 1) + k' ＝⟨ refl ⟩
(- pos d') ℤ* pos (succ (succ q)) + k' ＝⟨ x ⟩
(- pos d' ℤ* pos (succ (succ q))) + k' ＝⟨ xi ⟩
(- pos (succ (succ q)) ℤ* pos d') + k' ＝⟨ xii ⟩
negsucc (succ q) ℤ* pos d' + k' ∎
where
iₐₚ = distributivity-pos-addition (succ q ℕ* d') (succ r) ⁻¹
iiiₐₚ = pos-multiplication-equiv-to-ℕ (succ q) d' ⁻¹
viiₐₚ = negation-dist-over-mult' (pos d') q' ⁻¹
viiiₐₚ = ℤ-mult-right-id (- pos d')
ixₐₚ = distributivity-mult-over-ℤ' q' (pos 1) (- pos d') ⁻¹
xₐₚ = negation-dist-over-mult' (pos d') (pos (succ (succ q)))
xiₐₚ = ℤ*-comm (pos d') (pos (succ (succ q)))
xiiₐₚ = negation-dist-over-mult' (pos (succ (succ q))) (pos d') ⁻¹
i = ap -_ iₐₚ
ii = negation-dist (pos (succ q ℕ* d')) (pos (succ r)) ⁻¹
iii = ap (λ z → (- z) - pos (succ r)) iiiₐₚ
iv = ap ((- q' ℤ* pos d') +_) IV
v = ℤ+-rearrangement (- (q' ℤ* pos d')) k' (- pos d') ⁻¹
vi = ap (λ z → ((- z) + (- pos d')) + k') (ℤ*-comm q' (pos d'))
vii = ap (λ z → (z + (- pos d')) + k') viiₐₚ
viii = ap (λ z → ((- pos d') ℤ* q' + z) + k') viiiₐₚ ⁻¹
ix = ap (_+ k') ixₐₚ
x = ap (_+ k') xₐₚ
xi = ap (λ z → (- z) + k') xiₐₚ
xii = ap (_+ k') xiiₐₚ
γ : Σ r ꞉ ℕ , (a' ＝ negsucc (succ q) ℤ* pos d' + pos r) × r < d'
γ = I (subtraction' (succ r) (succ d) l₁)
ℤ-∣-respects-addition : (x y z : ℤ) → x ∣ y → x ∣ z → x ∣ y + z
ℤ-∣-respects-addition x y z (α , αₚ) (β , βₚ) = α + β , I
where
I : x ℤ* (α + β) ＝ y + z
I = x ℤ* (α + β) ＝⟨ distributivity-mult-over-ℤ' α β x ⟩
x ℤ* α + x ℤ* β ＝⟨ ap₂ _+_ αₚ βₚ ⟩
y + z ∎
ℤ-∣-respects-addition-of-multiples : (x y z k l : ℤ)
→ x ∣ y
→ x ∣ z
→ x ∣ (y ℤ* k + z ℤ* l)
ℤ-∣-respects-addition-of-multiples x y z k l (α , αₚ) (β , βₚ) = γ
where
I : x ℤ* (α ℤ* k + β ℤ* l) ＝ y ℤ* k + z ℤ* l
I = x ℤ* (α ℤ* k + β ℤ* l) ＝⟨ i ⟩
x ℤ* (α ℤ* k) + x ℤ* (β ℤ* l) ＝⟨ ii ⟩
x ℤ* α ℤ* k + x ℤ* β ℤ* l ＝⟨ iii ⟩
y ℤ* k + z ℤ* l ∎
where
i = distributivity-mult-over-ℤ' (α ℤ* k) (β ℤ* l) x
ii = ap₂ _+_ (ℤ*-assoc x α k ⁻¹) (ℤ*-assoc x β l ⁻¹)
iii = ap₂ _+_ (ap (_ℤ* k) αₚ) (ap (_ℤ* l) βₚ)
γ : Σ v ꞉ ℤ , x ℤ* v ＝ y ℤ* k + z ℤ* l
γ = α ℤ* k + β ℤ* l , I
\end{code}