{-# OPTIONS --cubical #-}
module BrouwerTree.Arithmetic.Properties where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Data.Nat
using (ℕ; zero; suc; ·-comm)
renaming (_+_ to _N+_; _·_ to _N·_; +-assoc to N+-assoc)
import Cubical.Data.Nat.Order as N
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary using (Dec; yes; no)
open import PropTrunc
open import BrouwerTree.Base
open import BrouwerTree.Properties
open import BrouwerTree.Code
open import BrouwerTree.Code.Results
open import BrouwerTree.Arithmetic
N≤-k· : ∀ {m n k} → m N.≤ n → k N· m N.≤ k N· n
N≤-k· {m} {n} {k} m≤n = subst (λ z → fst z N.≤ snd z)
(λ i → ·-comm m k i , ·-comm n k i)
(N.≤-·k m≤n)
ι-+-commutes : ∀ n m → ι (m N+ n) ≡ ι n + ι m
ι-+-commutes n zero = refl
ι-+-commutes n (suc m) = cong succ (ι-+-commutes n m)
ι-·-commutes : ∀ n m → ι (m N· n) ≡ ι n · ι m
ι-·-commutes n zero = refl
ι-·-commutes n (suc m) = ι-+-commutes (m N· n) n ∙ cong (_+ ι n) (ι-·-commutes n m)
increasing→monotone : ∀ {f : ℕ → Brw} → increasing f → ∀ {n m} → n N.≤ m → f n ≤ f m
increasing→monotone {f} f↑ {n} {m} (k , k+n≡m) = helper {n} {m} k k+n≡m where
helper : ∀ {n} {m} → (k : ℕ) → k N+ n ≡ m → f n ≤ f m
helper zero n≡m = ≤-refl-≡ (cong f n≡m)
helper {n} {m} (suc k) sk+n≡m = subst (λ z → f n ≤ f z) sk+n≡m
(≤-trans (helper k refl) (<-in-≤ (f↑ (k N+ n))))
increasing→zero<fsuc : ∀ {f : ℕ → Brw} {k} → increasing f → zero < f (suc k)
increasing→zero<fsuc {f} {zero} f↑ = ≤∘<-in-< ≤-zero (f↑ 0)
increasing→zero<fsuc {f} {suc k} f↑ = <-trans _ _ _ (increasing→zero<fsuc {f} {k} f↑) (f↑ (suc k))
succ-from : Brw → ℕ → Brw
succ-from x zero = x
succ-from x (suc n) = succ (succ-from x n)
succ-from-increasing : {x : Brw} → increasing (succ-from x)
succ-from-increasing zero = ≤-refl
succ-from-increasing (suc k) = ≤-succ-mono (succ-from-increasing k)
+-assoc : ∀ {a b} c → a + (b + c) ≡ (a + b) + c
+-assoc {a} {b} =
Brw-ind (λ c → a + (b + c) ≡ (a + b) + c)
(λ c → Brw-is-set _ _)
refl
(λ {x} ih → cong succ ih)
(λ {f} {f↑} ih → limit-pointwise-equal _ _ ih)
·-+-distributivity : ∀ {a b} c → a · b + a · c ≡ a · (b + c)
·-+-distributivity {a} {b} =
Brw-ind (λ c → a · b + a · c ≡ a · (b + c))
(λ c → Brw-is-set _ _)
refl
(λ {x} ih → +-assoc {a · b} {a · x} a ∙ cong (_+ a) ih)
limitCase
where
limitCase : ∀ {f} {f↑} → (∀ k → a · b + a · f k ≡ a · (b + f k)) →
a · b + a · limit f {f↑} ≡ a · (b + limit f {f↑})
limitCase {f} {f↑} ih with decZero a
... | yes a≡zero = cong (_· b) a≡zero ∙ zero·y≡zero b
... | no a≡zero = limit-pointwise-equal _ _ ih
·-assoc : ∀ {a b} c → a · (b · c) ≡ (a · b) · c
·-assoc {a} {b} =
Brw-ind (λ c → a · (b · c) ≡ (a · b) · c)
(λ c → Brw-is-set _ _)
refl
(λ {a'} ih → sym (·-+-distributivity {a} {b · a'} b) ∙ cong (λ z → z + a · b) ih)
limitCase
where
limitCase : ∀ {f} {f↑} → (∀ k → a · b · f k ≡ (a · b) · f k) →
a · b · limit f ≡ (a · b) · limit f {f↑}
limitCase {f} {f↑} ih with decZero b | decZero (a · b)
limitCase {f} {f↑} ih | yes b≡zero | yes ab≡zero = refl
limitCase {f} {f↑} ih | yes b≡zero | no ab≢zero =
⊥.rec (ab≢zero (subst (λ z → a · z ≡ zero) (sym b≡zero) refl))
limitCase {f} {f↑} ih | no b≢zero | yes ab≡zero with decZero a
limitCase {f} {f↑} ih | no b≢zero | yes ab≡zero | yes a≡zero = refl
limitCase {f} {f↑} ih | no b≢zero | yes ab≡zero | no a≢zero =
⊥.rec (·-no-zero-divisors a≢zero b≢zero ab≡zero)
limitCase {f} {f↑} ih | no b≢zero | no ab≢zero with decZero a
limitCase {f} {f↑} ih | no b≢zero | no ab≢zero | yes a≡zero =
⊥.rec (ab≢zero (subst (λ z → z · b ≡ zero) (sym a≡zero) (zero·y≡zero b)))
limitCase {f} {f↑} ih | no b≢zero | no ab≢zero | no a≢zero =
bisim (λ n → a · b · f n) (λ n → (a · b) · f n)
((λ k → ∣ k , ≤-refl-≡ (ih k) ∣) , λ k → ∣ k , ≤-refl-≡ (sym (ih k)) ∣)
exp-homomorphism : ∀ {a b c} → a ^ (b + c) ≡ a ^ b · a ^ c
exp-homomorphism {a} {b} {c} =
Brw-ind (λ c → a ^ (b + c) ≡ a ^ b · a ^ c)
(λ c → Brw-is-set _ _)
(sym (zero+y≡y (a ^ b)))
(λ {a'} ih → cong (_· a) ih ∙ sym (·-assoc {a ^ b} {a ^ a'} a))
limitCase
c
where
limitCase : ∀ {f} {f↑} → (∀ k → a ^ (b + f k) ≡ a ^ b · a ^ f k) →
a ^ (b + limit f {f↑}) ≡ a ^ b · a ^ limit f {f↑}
limitCase {f} {f↑} ih with decZeroOneMany a
limitCase {f} {f↑} ih | inl a≡zero = refl
limitCase {f} {f↑} ih | inr (inl a≡one) = sym (zero+y≡y (a ^ b) ∙ cong (_^ b) a≡one ∙ one^y≡one b)
limitCase {f} {f↑} ih | inr (inr one<a) with decZero (a ^ b)
limitCase {f} {f↑} ih | inr (inr one<a) | yes a^b≡zero =
⊥.rec (zero≢a^ b (one<x→x≢zero one<a) (sym a^b≡zero))
limitCase {f} {f↑} ih | inr (inr one<a) | no a^b≢zero =
bisim (λ n → a ^ (b + f n)) (λ n → a ^ b · a ^ f n)
((λ k → ∣ k , ≤-refl-≡ (ih k) ∣) , λ k → ∣ k , ≤-refl-≡ (sym (ih k)) ∣)
y·one≡y : (y : Brw) → y · one ≡ y
y·one≡y y = zero+y≡y y
one·y≡y : (y : Brw) → one · y ≡ y
one·y≡y =
Brw-ind (λ y → one · y ≡ y)
(λ y → Brw-is-set _ _)
refl
(cong succ)
(λ {f} {f↑} ih → bisim (λ n → one · f n) f
((λ k → ∣ k , ≤-refl-≡ (ih k) ∣) ,
(λ k → ∣ k , ≤-refl-≡ (sym (ih k)) ∣)))
x·2=x+x : (x : Brw) → x · ι 2 ≡ x + x
x·2=x+x x = sym (+-assoc {zero} {x} x) ∙ zero+y≡y (x + x)
x·n=1=x+xn : {n : ℕ} → (x : Brw) → x · ι n + x ≡ x + x · ι n
x·n=1=x+xn {zero} x = zero+y≡y x
x·n=1=x+xn {suc n} x = cong (_+ x) (x·n=1=x+xn {n} x) ∙ sym (+-assoc x)
ω=ω^1 : ω ≡ ω^ one
ω=ω^1 = bisim ι (λ n → one · ι n)
((λ k → ∣ k , ≤-refl-≡ (sym (one·y≡y (ι k))) ∣) ,
(λ k → ∣ k , ≤-refl-≡ (one·y≡y (ι k)) ∣))
ω-absorbs-finite : ∀ n → ι (suc n) · ω ≡ ω
ω-absorbs-finite zero =
bisim (λ n → succ zero · ι n) ι
((λ k → ∣ k , ≤-refl-≡ (one·y≡y (ι k)) ∣) ,
(λ k → ∣ k , ≤-refl-≡ (sym (one·y≡y (ι k))) ∣))
ω-absorbs-finite (suc n) =
bisim (λ k → succ (succ (ι n)) · ι k) (λ k → succ (ι n) · ι k)
((λ k → ∣ k N+ k , subst (λ z → fst z ≤ snd z)
(λ i → (cong ι (·-comm (suc (suc n)) k) ∙
ι-·-commutes (suc (suc n)) k) i ,
(cong ι (·-comm (suc n) (k N+ k)) ∙
ι-·-commutes (suc n) (k N+ k)) i)
(increasing→monotone ι-increasing (n+2·k≤⟨n+1⟩·2k n k)) ∣) ,
(λ k → ∣ k , ·x-mono (ι k) ≤-succ-incr-simple ∣))
∙ ω-absorbs-finite n
where
n+2·k≤⟨n+1⟩·2k : ∀ n k → (suc (suc n)) N· k N.≤ (suc n) N· (k N+ k)
n+2·k≤⟨n+1⟩·2k n k = subst (λ z → z N.≤ (suc n) N· (k N+ k))
(sym (N+-assoc k k (n N· k)))
(N.≤-k+ {k = k N+ k} (N≤-k· {k = n} (N.≤-+k {k = k} N.zero-≤)))
ω^x-absorbs-finite : ∀ {x n} → zero < x → ι (suc n) · ω^ x ≡ ω^ x
ω^x-absorbs-finite {x} {n} =
Brw-ind (λ x → zero < x → ι (suc n) · ω^ x ≡ ω^ x)
(λ x → isProp→ (Brw-is-set _ _))
(λ zero<zero → ⊥.rec (<-irreflexive _ zero<zero))
sucCase
(λ {f} {f↑} ih _ →
limit-skip-first (λ k → succ (ι n) · ω ^ f k)
∙ bisim (λ k → succ (ι n) · ω ^ f (suc k)) (λ k → ω ^ f k)
((λ k → ∣ suc k , ≤-refl-≡ (ih (suc k) (increasing→zero<fsuc f↑)) ∣) ,
(λ k → ∣ k , ≤-trans (ω^-mono (<-in-≤ (f↑ k)))
(≤-refl-≡ (sym (ih (suc k)(increasing→zero<fsuc f↑)))) ∣)))
x
where
sucCase : ∀ {x'} → (zero < x' → ι (suc n) · ω^ x' ≡ ω^ x') →
zero < succ x' → ι (suc n) · ω^ (succ x') ≡ ω^ (succ x')
sucCase {x'} ih zero<sx' with decZero x'
... | yes x'≡zero = subst (λ z → ι (suc n) · z ≡ z)
(ω=ω^1 ∙ cong (λ z → ω^ (succ z)) (sym x'≡zero))
(ω-absorbs-finite n)
... | no x'≢zero = ·-assoc {ι (suc n)} {ω^ x'} ω
∙ cong (_· ω) (ih (zero≠x→zero<x _ (λ zero≡x → x'≢zero (sym zero≡x))))
ω^-mono-< : {x y : Brw} → x < y → ω^ x < ω^ y
ω^-mono-< {x} {y} x<y with decZero (ω^ x)
... | yes ω^x≡zero = ⊥.rec (zero≢a^ x (λ ω≡zero → zero≠lim (sym ω≡zero)) (sym ω^x≡zero) )
... | no ω^x≢zero = ≤-trans (ω^-preserves-increasing {succ-from x} succ-from-increasing zero)
(ω^-mono x<y)
zero<ω^c : (c : Brw) → zero < ω^ c
zero<ω^c c = zero≠x→zero<x _ (zero≢a^ c λ ω≡zero → zero≠lim (sym ω≡zero))
a<omega^a : {a : Brw} → a ≤ ω^ a
a<omega^a {a} =
Brw-ind (λ a → a ≤ ω^ a)
(λ a → ≤-trunc)
≤-zero
(λ {a} ih → ≤-trans (≤-succ-mono ih) (ω^-mono-< (<-succ-incr-simple {a})))
(λ {f} {f↑} ih → weakly-bisimilar→lim≤lim f _ λ k → ∣ k , ih k ∣)
a
ω^one≡ω : ω^ one ≡ ω
ω^one≡ω = bisim _ _ ((λ k → ∣ k , ≤-refl-≡ (one·y≡y _) ∣) ,
(λ k → ∣ k , ≤-refl-≡ (sym (one·y≡y _)) ∣))
zero<ω : zero < ω
zero<ω = <∘≤-in-< (zero<ω^c one) (≤-refl-≡ ω^one≡ω)
ω<ω+ω : ω < ω + ω
ω<ω+ω = x+-mono-< {ω} {zero} {ω} zero<ω
is-additive-principal : Brw → Type
is-additive-principal x = (a : Brw) → a < x → a + x ≡ x
is-additive-principal-≤ : ∀ {x} → (∀ a → a < x → a + x ≤ x) → is-additive-principal x
is-additive-principal-≤ {x} p a a<x =
≤-antisym (p a a<x) (subst (λ z → z ≤ a + x) (zero+y≡y x) (+x-mono x ≤-zero))
additive-principal-ω^ : ∀ (c : Brw) → is-additive-principal (ω^ c)
additive-principal-ω^ =
Brw-ind (λ c → is-additive-principal (ω^ c))
(λ c → isPropΠ (λ a → isProp→ (Brw-is-set _ _)))
(λ a sa≤one → cong succ (x≤zero→x≡zero (≤-succ-mono⁻¹ sa≤one)))
(λ {c} _ → additive-principal-ω^succ c)
(λ {f} {f↑} ih → additive-principal-ω^lim f f↑ ih)
where
additive-principal-ω^succ : ∀ c → is-additive-principal (ω^ (succ c))
additive-principal-ω^succ c with decZero (ω^ c)
... | yes x = λ a a<zero → ⊥.rec (succ≰zero a<zero)
... | no qq =
is-additive-principal-≤ (λ a a<ω^c·ω →
weakly-bisimilar→lim≤lim _ _
(λ k → ∥-∥rec isPropPropTrunc
(λ (l , a<ω^c·l ) →
∣ k N+ l , ≤-trans (+x-mono (ω^ c · ι k) (<-in-≤ a<ω^c·l))
(≤-refl-≡ (·-+-distributivity {ω^ c} {ι l} (ι k)
∙ cong (ω^ c ·_) (sym (ι-+-commutes l k)))) ∣)
(below-limit-lemma _ _ a<ω^c·ω)))
additive-principal-ω^lim : ∀ f f↑ → ((k : ℕ) → is-additive-principal (ω^ (f k))) →
is-additive-principal (ω^ (limit f {f↑}))
additive-principal-ω^lim f f↑ ih =
is-additive-principal-≤ (λ a a<ω^fn →
weakly-bisimilar→lim≤lim _ _
(λ k → ∥-∥rec isPropPropTrunc (λ (l , a<ω^fl) → helper k l a<ω^fl)
(below-limit-lemma _ _ a<ω^fn)))
where
helper : ∀ {a} k l (a<ω^fn : a < ω^ (f l)) → ∥ Σ[ n ∈ ℕ ] (a + ω ^ f k) ≤ (ω ^ f n) ∥
helper {a} k l a<ω^fl with k N.≟ l
... | N.lt k<l =
∣ l , ≤-trans (x+-mono {a} {ω^ (f k)} {ω^ (f l)}
(ω^-mono (increasing→monotone f↑ (N.<-weaken k<l))))
(≤-refl-≡ (ih l a a<ω^fl)) ∣
... | N.eq k≡l = ∣ l , ≤-refl-≡ (cong (λ z → a + ω^ (f z)) k≡l ∙ ih l a a<ω^fl) ∣
... | N.gt l<k =
∣ k , ≤-refl-≡ (ih k a (≤-trans a<ω^fl (ω^-mono (increasing→monotone f↑ (N.<-weaken l<k))))) ∣
additive-principal-ω^-closure : ∀ c {a b} → a < ω^ c → b < ω^ c → a + b < ω^ c
additive-principal-ω^-closure c a<ω^c b<ω^c =
<∘≤-in-< (x+-mono-< b<ω^c) (≤-refl-≡ (additive-principal-ω^ c _ a<ω^c))
ω↑↑ : ℕ → Brw
ω↑↑ 0 = one
ω↑↑ (suc i) = ω^ (ω↑↑ i)
ω↑↑-↑ : increasing ω↑↑
ω↑↑-↑ 0 = subst (λ z → one < z) (sym ω^one≡ω) (<-cocone-simple ι {k = 1})
ω↑↑-↑ (suc i) = ω^-mono-< (ω↑↑-↑ i)
ε₀ : Brw
ε₀ = limit ω↑↑ {ω↑↑-↑}
ε₀≡ω^ε₀ : ε₀ ≡ ω^ ε₀
ε₀≡ω^ε₀ = ≤-antisym (weakly-bisimilar→lim≤lim ω↑↑ (λ n → limit ι ^ ω↑↑ n)
(λ k → ∣ k , a<omega^a ∣))
(weakly-bisimilar→lim≤lim (λ n → limit ι ^ ω↑↑ n) ω↑↑
(λ k → ∣ suc k , ≤-refl ∣))