DyadicRationals
Andrew Sneap, April 2023 Note that this file is incomplete.{-# 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 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 whereThis file defines dyadic rationals as a record, along with many widely accepted operations, relations and results on dyadic rationals. They are denoted ℤ[1/2].ℤ[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)