Andrew Sneap, April 2023
Note that this file is incomplete.
\begin{code}
{-# OPTIONS --without-K --safe #-}
open import Integers.Addition renaming (_+_ to _+ℤ_ ; _-_ to _ℤ-_)
open import Integers.Multiplication renaming (_*_ to _ℤ*_)
open import Integers.Negation renaming (-_ to ℤ-_)
open import Integers.Order
open import Integers.Type
open import MLTT.Spartan
open import Naturals.Addition renaming (_+_ to _+ℕ_)
open import Naturals.Multiplication renaming (_*_ to _ℕ*_)
open import Naturals.Properties hiding (double)
open import Notation.Order
open import UF.Base
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.DiscreteAndSeparated
open import TWA.Thesis.Chapter5.Integers
module TWA.Thesis.AndrewSneap.DyadicRationals where
\end{code}
This file defines dyadic rationals as a record, along with many widely
accepted operations, relations and results on dyadic rationals. They
are denoted ℤ[1/2].
\begin{code}
ℤ[1/2] : 𝓤₀ ̇
ℤ[1/2] = Σ (z , n) ꞉ ℤ × ℕ , (n ＝ 0) + ((n ≠ 0) × odd z)
ℤ[1/2]-cond-is-prop : FunExt → (z : ℤ) (n : ℕ)
→ is-prop ((n ＝ 0) + ((n ≠ 0) × odd z))
ℤ[1/2]-cond-is-prop fe z n
= +-is-prop ℕ-is-set
(×-is-prop (Π-is-prop (fe 𝓤₀ 𝓤₀) (λ _ → 𝟘-is-prop))
(odd-is-prop z))
(λ e (ne , _) → ne e)
0ℤ[1/2] : ℤ[1/2]
0ℤ[1/2] = (pos 0 , 0) , inl refl
1ℤ[1/2] : ℤ[1/2]
1ℤ[1/2] = (pos 1 , 0) , inl refl
1/2ℤ[1/2] : ℤ[1/2]
1/2ℤ[1/2] = (pos 1 , 1) , inr (positive-not-zero 0 , ⋆)
normalise-pos normalise-neg : ℤ → ℕ → ℤ[1/2]
normalise-pos-oe : (z : ℤ) → ℕ → even z + odd z → ℤ[1/2]
normalise-pos-oe z 0 _ = (z , 0) , inl refl
normalise-pos-oe z (succ n) (inl e) = normalise-pos (z /2') n
normalise-pos-oe z (succ n) (inr o) = (z , succ n)
, inr (positive-not-zero n , o)
normalise-pos z n = normalise-pos-oe z n (even-or-odd? z)
normalise-neg z 0 = (z +ℤ z , 0) , inl refl
normalise-neg z (succ n) = normalise-neg (z +ℤ z) n
normalise-pos' : (z : ℤ) (n : ℕ)
→ (oe : even z + odd z)
→ let ((k , δ) , p) = normalise-pos-oe z n oe in
Σ m ꞉ ℕ , ((pos (2^ m) ℤ* k , δ +ℕ m) ＝ z , n)
normalise-pos' z 0 oe
= 0 , to-×-＝ (ℤ-mult-left-id z) refl
normalise-pos' z (succ n) (inl e)
= succ m , to-×-＝ γ (ap succ e₂)
where
kδ = normalise-pos-oe (z /2') n (even-or-odd? (z /2'))
k : ℤ
k = pr₁ (pr₁ kδ)
δ : ℕ
δ = pr₂ (pr₁ kδ)
IH = normalise-pos' (z /2') n (even-or-odd? (z /2'))
m : ℕ
m = pr₁ IH
q : pos (2^ m) ℤ* k , δ +ℕ m ＝ (z /2') , n
q = pr₂ IH
e₁ : pos (2^ m) ℤ* k ＝ (z /2')
e₁ = pr₁ (from-×-＝' q)
e₂ : δ +ℕ m ＝ n
e₂ = pr₂ (from-×-＝' q)
γ : pos (2^ (succ m)) ℤ* k ＝ z
γ = pos (2^ (succ m)) ℤ* k
＝⟨ refl ⟩
pos (2 ℕ* 2^ m) ℤ* k
＝⟨ ap (_ℤ* k) (pos-multiplication-equiv-to-ℕ 2 (2^ m) ⁻¹) ⟩
pos 2 ℤ* pos (2^ m) ℤ* k
＝⟨ ℤ*-assoc (pos 2) (pos (2^ m)) k ⟩
pos 2 ℤ* (pos (2^ m) ℤ* k)
＝⟨ ap (pos 2 ℤ*_) e₁ ⟩
pos 2 ℤ* (z /2')
＝⟨ ℤ*-comm (pos 2) (z /2') ⟩
(z /2') ℤ* pos 2
＝⟨ even-lemma z e ⟩
z ∎
normalise-pos' z (succ n) (inr o) = 0 , to-×-＝ (ℤ-mult-left-id z) refl
normalise : ℤ × ℤ → ℤ[1/2]
normalise (k , pos n) = normalise-pos k n
normalise (k , negsucc n) = normalise-neg k n
normalise-neg' : (z : ℤ) (n : ℕ)
→ let ((k , δ) , p) = normalise-neg z n in
(k , δ) ＝ pos (2^ (succ n)) ℤ* z , 0
normalise-neg' z 0 = to-×-＝ (ℤ*-comm z (pos 2)) refl
normalise-neg' z (succ n) = to-×-＝ I e₂
where
kδ = normalise-neg (z +ℤ z) n
k : ℤ
k = pr₁ (pr₁ kδ)
δ : ℕ
δ = pr₂ (pr₁ kδ)
e₁ : k ＝ pos (2^ (succ n)) ℤ* (z +ℤ z)
e₁ = pr₁ (from-×-＝' (normalise-neg' (z +ℤ z) n))
e₂ : δ ＝ 0
e₂ = pr₂ (from-×-＝' (normalise-neg' (z +ℤ z) n))
I : k ＝ pos (2^ (succ (succ n))) ℤ* z
I = k
＝⟨ e₁ ⟩
pos (2^ (succ n)) ℤ* (z ℤ* pos 2)
＝⟨ ap (pos (2^ (succ n)) ℤ*_) (ℤ*-comm z (pos 2)) ⟩
pos (2^ (succ n)) ℤ* (pos 2 ℤ* z)
＝⟨ ℤ*-assoc (pos (2^ (succ n))) (pos 2) z ⁻¹ ⟩
pos (2^ (succ n)) ℤ* pos 2 ℤ* z
＝⟨ ap (_ℤ* z) (pos-multiplication-equiv-to-ℕ (2^ (succ n)) 2) ⟩
pos (2^ (succ n) ℕ* 2) ℤ* z
＝⟨ ap (λ n → pos n ℤ* z) (mult-commutativity (2^ (succ n)) 2) ⟩
pos (2^ (succ (succ n))) ℤ* z ∎
lowest-terms-normalised : FunExt → (((k , δ) , p) : ℤ[1/2])
→ normalise-pos k δ ＝ ((k , δ) , p)
lowest-terms-normalised fe ((k , .0) , inl refl) = refl
lowest-terms-normalised fe ((k , zero) , inr (δnz , o)) = 𝟘-elim (δnz refl)
lowest-terms-normalised fe ((k , succ δ) , inr (δnz , o))
= γ (even-or-odd? k)
where
γ : (oe : even k + odd k)
→ normalise-pos-oe k (succ δ) oe ＝ (k , succ δ) , inr (δnz , o)
γ (inl e) = 𝟘-elim (e o)
γ (inr o)
= to-subtype-＝ (λ (z , n) → ℤ[1/2]-cond-is-prop fe z n) refl
normalise-pos-lemma₁ : FunExt → (k : ℤ) (δ : ℕ)
→ (p : (δ ＝ 0) + ((δ ≠ 0) × odd k))
→ normalise-pos ((k +ℤ k) /2') δ ＝ (k , δ) , p
normalise-pos-lemma₁ fe k 0 (inl refl)
= to-subtype-＝ (λ (z , n) → ℤ[1/2]-cond-is-prop fe z n)
(to-×-＝ (div-by-two k) refl)
normalise-pos-lemma₁ fe k 0 (inr (δnz , k-odd)) = 𝟘-elim (δnz refl)
normalise-pos-lemma₁ fe k (succ δ) (inr p) with even-or-odd? ((k +ℤ k) /2')
normalise-pos-lemma₁ fe k (succ δ) (inr (δnz , k-odd)) | inl k-even
= 𝟘-elim (k-even (transport odd (div-by-two k ⁻¹) k-odd))
... | inr _ = to-subtype-＝ (λ (z , n) → ℤ[1/2]-cond-is-prop fe z n)
(to-×-＝ (div-by-two k) refl)
normalise-pos-lemma₂ : (k : ℤ) (δ : ℕ)
→ normalise-pos k δ ＝ normalise-pos (k +ℤ k) (succ δ)
normalise-pos-lemma₂ k δ with even-or-odd? (k +ℤ k)
... | inl _ = ap (λ s → normalise-pos s δ) (div-by-two k ⁻¹)
... | inr o = 𝟘-elim (times-two-even' k o)
double : ℤ → ℤ
double a = a +ℤ a
normalise-lemma : FunExt → (k : ℤ) (δ : ℕ) (n : ℕ)
→ (p : (δ ＝ 0) + ((δ ≠ 0) × odd k))
→ normalise
(rec k double n +ℤ rec k double n , (pos (succ δ) +ℤ pos n))
＝ (k , δ) , p
normalise-lemma fe k δ 0 p with even-or-odd? (k +ℤ k)
... | inl even = normalise-pos-lemma₁ fe k δ p
... | inr odd = 𝟘-elim (times-two-even' k odd)
normalise-lemma fe k δ (succ n) p with even-or-odd? (k +ℤ k)
... | inl even
= let y = rec k double n
z = (y +ℤ y) in
normalise (z +ℤ z , (succℤ (pos (succ δ) +ℤ pos n)))
＝⟨ ap (λ - → normalise (z +ℤ z , succℤ -))
(distributivity-pos-addition (succ δ) n) ⟩
normalise (z +ℤ z , succℤ (pos (succ δ +ℕ n)))
＝⟨ refl ⟩
normalise-pos (z +ℤ z) (succ (succ δ +ℕ n))
＝⟨ normalise-pos-lemma₂ z (succ δ +ℕ n) ⁻¹ ⟩
normalise-pos z (succ δ +ℕ n)
＝⟨ refl ⟩
normalise (z , pos (succ δ +ℕ n))
＝⟨ ap (λ - → normalise (z , -))
(distributivity-pos-addition (succ δ) n ⁻¹) ⟩
normalise (z , pos (succ δ) +ℤ pos n)
＝⟨ normalise-lemma fe k δ n p ⟩
(k , δ) , p ∎
... | inr odd = 𝟘-elim (times-two-even' k odd)
_<ℤ[1/2]_ _≤ℤ[1/2]_ : ℤ[1/2] → ℤ[1/2] → 𝓤₀ ̇
((x , n) , _) <ℤ[1/2] ((y , m) , _) = x ℤ* pos (2^ m) < y ℤ* pos (2^ n)
((x , n) , _) ≤ℤ[1/2] ((y , m) , _) = x ℤ* pos (2^ m) ≤ y ℤ* pos (2^ n)
<ℤ[1/2]-is-prop : (x y : ℤ[1/2]) → is-prop (x <ℤ[1/2] y)
<ℤ[1/2]-is-prop ((x , a) , _) ((y , b) , _)
= ℤ<-is-prop (x ℤ* pos (2^ b)) (y ℤ* pos (2^ a))
≤ℤ[1/2]-is-prop : (x y : ℤ[1/2]) → is-prop (x ≤ℤ[1/2] y)
≤ℤ[1/2]-is-prop ((x , a) , _) ((y , b) , _)
= ℤ≤-is-prop (x ℤ* pos (2^ b)) (y ℤ* pos (2^ a))
ℤ[1/2]⁺ : 𝓤₀ ̇
ℤ[1/2]⁺ = Σ x ꞉ ℤ[1/2] , 0ℤ[1/2] <ℤ[1/2] x
_<ℤ[1/2]⁺_ _≤ℤ[1/2]⁺_ : ℤ[1/2]⁺ → ℤ[1/2]⁺ → 𝓤₀ ̇
(x , l) <ℤ[1/2]⁺ (y , l') = x <ℤ[1/2] y
(x , l) ≤ℤ[1/2]⁺ (y , l') = x ≤ℤ[1/2] y
is-positive : ℤ[1/2] -> 𝓤₀ ̇
is-positive x = 0ℤ[1/2] <ℤ[1/2] x
instance
Order-ℤ[1/2]-ℤ[1/2] : Order ℤ[1/2] ℤ[1/2]
_≤_ {{Order-ℤ[1/2]-ℤ[1/2]}} = _≤ℤ[1/2]_
Strict-Order-ℤ[1/2]-ℤ[1/2] : Strict-Order ℤ[1/2] ℤ[1/2]
_<_ {{Strict-Order-ℤ[1/2]-ℤ[1/2]}} = _<ℤ[1/2]_
instance
Order-ℤ[1/2]⁺-ℤ[1/2]⁺ : Order ℤ[1/2]⁺ ℤ[1/2]⁺
_≤_ {{Order-ℤ[1/2]⁺-ℤ[1/2]⁺}} = _≤ℤ[1/2]⁺_
Strict-Order-ℤ[1/2]⁺-ℤ[1/2]⁺ : Strict-Order ℤ[1/2]⁺ ℤ[1/2]⁺
_<_ {{Strict-Order-ℤ[1/2]⁺-ℤ[1/2]⁺}} = _<ℤ[1/2]⁺_
record Dyadics : 𝓤₁ ̇ where
field
_ℤ[1/2]+_ : ℤ[1/2] → ℤ[1/2] → ℤ[1/2]
ℤ[1/2]-_ : ℤ[1/2] → ℤ[1/2]
infix 20 ℤ[1/2]-_
infixl 19 _ℤ[1/2]-_
_ℤ[1/2]-_ : (p q : ℤ[1/2]) → ℤ[1/2]
p ℤ[1/2]- q = p ℤ[1/2]+ (ℤ[1/2]- q)
field
_ℤ[1/2]*_ : ℤ[1/2] → ℤ[1/2] → ℤ[1/2]
ℤ[1/2]-abs : ℤ[1/2] → ℤ[1/2]
trans : (x y z : ℤ[1/2]) → x < y → y < z → x < z
trans' : (x y z : ℤ[1/2]) → x ≤ y → y ≤ z → x ≤ z
dense : (x y : ℤ[1/2]) → (x < y) → Σ k ꞉ ℤ[1/2] , (x < k) × (k < y)
≤-refl : (x : ℤ[1/2]) → x ≤ x
<-is-≤ℤ[1/2] : (x y : ℤ[1/2]) → x < y → x ≤ y
diff-positive : (x y : ℤ[1/2]) → x < y → 0ℤ[1/2] < (y ℤ[1/2]- x)
<-swap : (x y : ℤ[1/2]) → x < y → (ℤ[1/2]- y) < (ℤ[1/2]- x)
≤-swap : (x y : ℤ[1/2]) → x ≤ y → (ℤ[1/2]- y) ≤ (ℤ[1/2]- x)
≤-swap' : (x y : ℤ[1/2]) → (ℤ[1/2]- x) ≤ (ℤ[1/2]- y) → y ≤ x
≤-split : (x y : ℤ[1/2]) → x ≤ y → x < y + (x ＝ y)
<-pos-mult'
: (x y : ℤ[1/2]) → 0ℤ[1/2] < x
→ 0ℤ[1/2] < y → 0ℤ[1/2] < (x ℤ[1/2]* y)
ℤ[1/2]<-+ : (x y : ℤ[1/2]) → 0ℤ[1/2] < y → x < (x ℤ[1/2]+ y)
ℤ[1/2]<-neg : (x y : ℤ[1/2]) → 0ℤ[1/2] < y → (x ℤ[1/2]- y) < x
ℤ[1/2]<-rearrange : (x y z : ℤ[1/2]) → (x ℤ[1/2]+ y) < z → y < (z ℤ[1/2]- x)
ℤ[1/2]-1/2-< : (x : ℤ[1/2]) → 0ℤ[1/2] < x → (1/2ℤ[1/2] ℤ[1/2]* x) < x
normalise-≤
: (n : ℕ) → ((k , p) : ℤ × ℤ)
→ normalise (k , p) ≤ normalise ((k +pos n) , p)
normalise-denom-≤
: (k : ℕ) (p q : ℤ) → p ≤ q → normalise (pos k , q) ≤ normalise (pos k , p)
ℤ[1/2]-ordering-property
: (a b c d : ℤ[1/2]) → (a ℤ[1/2]- b) < (c ℤ[1/2]- d) → (a < c) + (d < b)
normalise-succ' : (z n : ℤ) → normalise (z , n)
＝ normalise (z +ℤ z , succℤ n)
normalise-pred' : (z n : ℤ) → normalise (z , predℤ n)
＝ normalise (z +ℤ z , n)
ℤ[1/2]<-positive-mult
: (a b : ℤ[1/2]) → is-positive a → is-positive b → is-positive (a ℤ[1/2]* b)
ℤ[1/2]-find-lower : (ε : ℤ[1/2]) → is-positive ε
→ Σ n ꞉ ℤ , normalise (pos 2 , n) < ε
normalise-negation
: (a b c : ℤ)
→ normalise (a , c) ℤ[1/2]- normalise (b , c) ＝ normalise (a ℤ- b , c)
normalise-negation' : (a b : ℤ)
→ ℤ[1/2]- normalise (a , b) ＝ normalise (ℤ- a , b)
from-normalise-≤-same-denom
: (a b c : ℤ) → normalise (a , c) ≤ normalise (b , c) → a ≤ b
ℤ[1/2]<-≤ : (x y z : ℤ[1/2]) → x < y → y ≤ z → x < z
ℤ[1/2]<-≤ x y z x<y y≤z with ≤-split y z y≤z
... | inl y<z = trans x y z x<y y<z
... | inr y=z = transport (x <_) y=z x<y
ℤ[1/2]≤-< : (x y z : ℤ[1/2]) → x ≤ y → y < z → x < z
ℤ[1/2]≤-< x y z x≤y y<z with ≤-split x y x≤y
... | inl x<y = trans x y z x<y y<z
... | inr x＝y = transport (_< z) (x＝y ⁻¹) y<z
0<1/2ℤ[1/2] : 0ℤ[1/2] < 1/2ℤ[1/2]
0<1/2ℤ[1/2] = 0 , refl
0<1ℤ[1/2] : 0ℤ[1/2] < 1ℤ[1/2]
0<1ℤ[1/2] = 0 , refl
normalise-≤2 : (l r p : ℤ) → l ≤ r → normalise (l , p) ≤ normalise (r , p)
normalise-≤2 l r p (j , refl) = normalise-≤ j (l , p)
\end{code}