Truncated logarithm over the natural numbers

Cubical/Data/Fin/Properties.agda

@@ -440,39 +440,6 @@ Fin-inj n m p with n ≟ m
 ... | lt n<m = Empty.rec (Fin-inj′ n<m (sym p))
 ... | gt n>m = Empty.rec (Fin-inj′ n>m p)
 
-≤-·sk-cancel : ∀ {m} {k} {n} → m · suc k ≤ n · suc k → m ≤ n
-≤-·sk-cancel {m} {k} {n} (d , p) = o , inj-·sm {m = k} goal where
-  r = d % suc k
-  o = d / suc k
-  resn·k : Residue (suc k) (n · suc k)
-  resn·k = ((r , n%sk<ᵗsk d k) , (o + m)) , reason where
-   reason = expand× ((r , n%sk<ᵗsk d k) , o + m) ≡⟨ expand≡ (suc k) r (o + m) ⟩
-            (o + m) · suc k + r                 ≡[ i ]⟨ +-comm (·-distribʳ o m (suc k) (~ i)) r i ⟩
-            r + (o · suc k + m · suc k)         ≡⟨ +-assoc r (o · suc k) (m · suc k) ⟩
-            (r + o · suc k) + m · suc k         ≡⟨ cong (_+ m · suc k) (+-comm r (o · suc k) ∙ moddiv d (suc k)) ⟩
-            d + m · suc k                       ≡⟨ p ⟩
-            n · suc k ∎
-
-  residuek·n : ∀ k n → (r : Residue (suc k) (n · suc k)) → ((fzero , n) , expand≡ (suc k) 0 n ∙ +-zero _) ≡ r
-  residuek·n _ _ = isContr→isProp isContrResidue _
-
-  r≡0 : r ≡ 0
-  r≡0 = cong (toℕ {suc k} ∘ extract) (sym (residuek·n k n resn·k))
-  d≡o·sk : d ≡ o · suc k
-  d≡o·sk = sym (moddiv d (suc k)) ∙∙ cong (o · suc k +_) r≡0 ∙∙ +-zero _
-  goal : (o + m) · suc k ≡ n · suc k
-  goal = sym (·-distribʳ o m (suc k)) ∙∙ cong (_+ m · suc k) (sym d≡o·sk) ∙∙ p
-
-<-·sk-cancel : ∀ {m} {k} {n} → m · suc k < n · suc k → m < n
-<-·sk-cancel {m} {k} {n} p = goal where
-  ≤-helper : m ≤ n
-  ≤-helper = ≤-·sk-cancel (pred-≤-pred (<≤-trans p (≤-suc ≤-refl)))
-  goal : m < n
-  goal = case <-split (suc-≤-suc ≤-helper) of λ
-    { (inl g) → g
-    ; (inr e) → Empty.rec (¬m<m (subst (λ m → m · suc k < n · suc k) e p))
-    }
-
 factorEquiv : ∀ {n} {m} → Fin n × Fin m ≃ Fin (n · m)
 factorEquiv {zero} {m} = uninhabEquiv (¬Fin0 ∘ fst) ¬Fin0
 factorEquiv {suc n} {m} = intro , isEmbedding×isSurjection→isEquiv (isEmbeddingIntro , isSurjectionIntro) where

Cubical/Data/Nat/Logarithm.agda

@@ -0,0 +1,156 @@
+module Cubical.Data.Nat.Logarithm where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum   as ⊎
+
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Nat.Order.Inductive
+open import Cubical.Data.Nat.Mod renaming (
+  remainder_/_ to _%_ ; quotient_/_ to _/_ ; ≡remainder+quotient to ≡%+·/)
+
+open import Cubical.Reflection.RecordEquiv
+
+open import Cubical.Relation.Binary.Order.Poset.Instances.Nat
+open import Cubical.Relation.Binary.Order.Quoset.Instances.Nat
+open import Cubical.Relation.Binary.Order.QuosetReasoning
+open import Cubical.Relation.Nullary
+
+open <-≤-Reasoning ℕ
+  (snd ℕ≤Poset) (snd ℕ<Quoset) (λ _ → <≤-trans) (λ _ → ≤<-trans) <-weaken
+open ≤-syntax
+open <-syntax
+open ≡-syntax
+
+record Logℕ (b x : ℕ) : Type where
+  no-eta-equality
+  field
+    log     : ℕ
+    ^log≤   : b ^ log ≤ x
+    <^1+log : x < b ^ suc log
+
+unquoteDecl LogℕIsoΣ = declareRecordIsoΣ LogℕIsoΣ (quote Logℕ)
+
+private
+  lemmaIsPropLogℕ : ∀ {m x l₀ l₁} → x < (suc m) ^ suc l₀ → (suc m) ^ l₁ ≤ x → ¬ (l₀ < l₁)
+  lemmaIsPropLogℕ {b-1} {x} {l₀} {l₁} <b^1+l₀ b^l₁≤ l₀<l₁ =
+    let b = suc b-1
+    in  ¬m<m $ begin< x <⟨ <b^1+l₀ ⟩ b ^ suc l₀ ≤⟨ ≤-sk^ l₀<l₁ ⟩ b ^ l₁ ≤⟨ b^l₁≤ ⟩ x ◾
+
+isPropLogℕ : ∀ m n → isProp (Logℕ (suc m) n)
+isPropLogℕ m x = isOfHLevelRetractFromIso 1 LogℕIsoΣ proof where
+  proof : isProp (Σ[ l ∈ ℕ ] ((suc m) ^ l ≤ x) × (x < (suc m) ^ suc l))
+  proof (l₀ , b^l₀≤ , <b^1+l₀) (l₁ , b^l₁≤ , <b^1+l₁) with l₀ ≟ l₁
+  ... | lt l₀<l₁ = ⊥.rec  (lemmaIsPropLogℕ <b^1+l₀ b^l₁≤ l₀<l₁)
+  ... | eq l₀≡l₁ = Σ≡Prop (λ _ → isProp× isProp≤ isProp≤) l₀≡l₁
+  ... | gt l₀>l₁ = ⊥.rec  (lemmaIsPropLogℕ <b^1+l₁ b^l₀≤ l₀>l₁)
+
+module LogTheory (logℕ : ∀ m n → Logℕ (suc (suc m)) (suc n)) where
+
+  log : (b : ℕ) → {2 ≤ᵗ b} → (x : ℕ) → {1 ≤ᵗ x} → ℕ
+  log (suc (suc m)) (suc n) = Logℕ.log (logℕ m n)
+
+  module _ (m : ℕ) where
+    private
+      b   = suc (suc m)
+      b-1 = suc m
+
+      logℕBase^ : ∀ n → Logℕ b (b ^ n)
+      logℕBase^ n .Logℕ.log     = n
+      logℕBase^ n .Logℕ.^log≤   = ≤-refl
+      logℕBase^ n .Logℕ.<^1+log = <-ssk^ {m = n} <-suc
+
+      logℕBase· : ∀ n → Logℕ b (b · suc n)
+      logℕBase· n .Logℕ.log     = suc (log b (suc n))
+      logℕBase· n .Logℕ.^log≤   = ≤-k·  {k = b}     (Logℕ.^log≤ (logℕ m n))
+      logℕBase· n .Logℕ.<^1+log = <-sk· {k = suc m} (Logℕ.<^1+log (logℕ m n))
+
+      logℕ1 : Logℕ b 1
+      logℕ1 .Logℕ.log     = 0
+      logℕ1 .Logℕ.^log≤   = ≤-refl
+      logℕ1 .Logℕ.<^1+log = suc-≤-suc zero-<suc
+
+    isContrLogℕ : ∀ x → {1 ≤ᵗ x} → isContr (Logℕ (suc (suc m)) x)
+    isContrLogℕ (suc n) .fst = logℕ m n
+    isContrLogℕ (suc n) .snd = isPropLogℕ (suc m) (suc n) (logℕ m n)
+
+    isUniqueLogℕ : ∀ {n} → {1≤n : 1 ≤ᵗ n} → (q : Logℕ b n) → log b n {1≤n} ≡ (Logℕ.log q)
+    isUniqueLogℕ {suc n} = cong Logℕ.log ∘ snd (isContrLogℕ _)
+
+    logBase^ : ∀ n → log b (b ^ n) {<→<ᵗ (0<^ n)} ≡ n
+    logBase^ = isUniqueLogℕ ∘ logℕBase^
+
+    logBase· : ∀ n → log b (b · suc n) ≡ suc (log b (suc n))
+    logBase· = isUniqueLogℕ ∘ logℕBase·
+
+    log1 : log b 1 ≡ 0
+    log1 = isUniqueLogℕ logℕ1
+
+    logBase : log b b ≡ 1
+    logBase =
+      cong (λ m → log b (suc m)) (sym (·-identityʳ b-1)) ∙∙ logBase· 0 ∙∙ cong suc log1
+
+    logMono≤ : ∀ x y {1≤x} {1≤y} → x ≤ y → log b x {1≤x} ≤ log b y {1≤y}
+    logMono≤ x@(suc x') y@(suc y') x≤y = pred-≤-pred $ <-ssk^-cancel {k = m} $ begin<
+      b ^ log b x       ≤⟨ Logℕ.^log≤ (logℕ m x') ⟩
+      x                 ≤⟨ x≤y ⟩
+      y                 <⟨ Logℕ.<^1+log (logℕ m y') ⟩
+      b ^ suc (log b y) ◾
+
+module LogCore (m : ℕ) where
+  private
+    b   = suc (suc m)
+    b-1 = suc m
+
+    /b≤f : ∀ n {f} → n ≤ᵗ f → (suc n / b) ≤ᵗ f
+    /b≤f n {f} n≤f =
+      ≤→≤ᵇ (begin< suc n / b <⟨ quotient<id n m ⟩ suc n ≤⟨ ≤ᵇ→≤ n≤f ⟩ suc f ◾)
+
+  hlog : ∀ n f → n ≤ᵗ f → ℕ
+  hlog   zero    f       n≤f = 0
+  hlog x@(suc n) (suc f) n≤f with Dichotomyℕ b x
+  ... | inl b≤x = suc (hlog (x / b) f (/b≤f n n≤f))
+  ... | inr x<b = 0
+
+  <base→hlog≡0 : ∀ {x f} → {t : x ≤ᵗ f} → (x < b) → hlog x f t ≡ 0
+  <base→hlog≡0   {zero}  {f}     x<b = refl
+  <base→hlog≡0 x@{suc n} {suc f} x<b with Dichotomyℕ b x
+  ... | inl b≤x = ⊥.rec (<-asym x<b b≤x)
+  ... | inr x<b = refl
+
+  ^hlog≤ : ∀ x f → {1 ≤ᵗ x} → (t : x ≤ᵗ f) → b ^ (hlog x f t) ≤ x
+  ^hlog≤ x@(suc n) (suc f) t with Dichotomyℕ b x
+  ... | inr x<b = ≤ᵇ→≤ tt
+  ... | inl b≤x with Dichotomyℕ b (x / b)
+  ... | inl b≤x/b = let 1≤x/b = ≤→≤ᵇ (≥→quotient≥1 n b-1 b≤x) in begin≤
+    b ^ suc (hlog (x / b) f (/b≤f n t))   ≤⟨ ≤-k· {k = b} (^hlog≤ (x / b) f {1≤x/b} _) ⟩
+    b · (x / b)                           ≤⟨ ≤SumRight {k = x % b} ⟩
+    x % b + b · (x / b)                 ≡→≤⟨ ≡%+·/ b x ⟩
+    x                                     ◾
+  ... | inr x/b<b = flip (subst (_≤ x)) b≤x $
+    b                                   ≡⟨ sym (·-identityʳ b) ⟩
+    b · b ^ 0                           ≡⟨ sym (cong (b ^_ ∘ suc) (<base→hlog≡0 x/b<b)) ⟩
+    b ^ suc (hlog (x / b) f (/b≤f n t)) ∎
+
+  <^1+hlog : ∀ x f → (t : x ≤ᵗ f) → x < b ^ suc (hlog x f t)
+  <^1+hlog   0       f       t = 0<^ {b-1} 1
+  <^1+hlog x@(suc n) (suc f) t with Dichotomyℕ b x
+  ... | inl b≤x = quotient<→<· _ b-1 _ (<^1+hlog (x / b) f (/b≤f n t))
+  ... | inr x<b = subst (x <_) (sym (·-identityʳ b)) x<b
+
+logℕ : ∀ m n → Logℕ (suc (suc m)) (suc n)
+logℕ m n .Logℕ.log     = LogCore.hlog     m (suc n) (suc n) (<ᵗsucm {n})
+logℕ m n .Logℕ.^log≤   = LogCore.^hlog≤   m (suc n) (suc n) (<ᵗsucm {n})
+logℕ m n .Logℕ.<^1+log = LogCore.<^1+hlog m (suc n) (suc n) (<ᵗsucm {n})
+
+open LogTheory (logℕ) public
+
+-- we prove this lemma here rather than in the `LogTheory` module,
+-- as it follows immediately from an auxiliary result used to define `logℕ`
+<base→log≡0 : ∀ m x {1<x} → (x < suc (suc m)) → log (suc (suc m)) x {1<x} ≡ 0
+<base→log≡0 m (suc n) = LogCore.<base→hlog≡0 m

Cubical/Data/Nat/Mod.agda

@@ -377,6 +377,10 @@ mod-lCancel d@(suc n) x y =
   (y + x mod d) mod d ≡⟨ cong (_mod d) (+-comm y (x mod d)) ⟩
   (x mod d + y) mod d ∎
 
+mod≤L : (m n : ℕ) → m mod n ≤ m
+mod≤L m   zero    = zero-≤
+mod≤L m n@(suc _) = subst (m mod n ≤_) (≡remainder+quotient n m) ≤SumLeft
+
 <→mod≡id : (m n : ℕ) → m < n → m mod n ≡ m
 <→mod≡id m zero    m<0     = ⊥.rec (¬-<-zero m<0)
 <→mod≡id m (suc n) (k , p) = cong (hmod 0 n m) (injSuc (sym p ∙ +-comm k (suc m)))
@@ -398,6 +402,70 @@ mod-lCancel d@(suc n) x y =
     step2 = cong (_∸ (m mod suc n)) (≡remainder+quotient (suc n) m)
     step3 = cong (m ∸_) (<→mod≡id m (suc n) m<sn)
 
+quotientUnipotent : (n : ℕ) → quotient suc n / suc n ≡ 1
+quotientUnipotent n =
+  let
+    x = suc n ; _/_ = quotient_/_ ; _%_ = remainder_/_
+  in
+    inj-sm· {m = n} $
+      x · x / x         ≡⟨⟩
+      0 + x · x / x     ≡⟨ sym $ cong (_+ x · x / x) (zero-charac x) ⟩
+      x % x + x · x / x ≡⟨ ≡remainder+quotient x x ⟩
+      x                 ≡⟨ sym $ ·-identityʳ x ⟩
+      x · 1             ∎
+
+≥→quotient≥1 : (m n : ℕ) → suc m ≥ suc n → 1 ≤ quotient suc m / suc n
+≥→quotient≥1 m n (r , p) =
+  let
+    a = suc m ; b = suc n
+    _/_ = quotient_/_ ; _%_ = remainder_/_
+  in
+    ≤-sk·-cancel {k = n} $ ≤-k+-cancel {k = remainder a / b} $
+      a % b + b · 1       ≡≤⟨ cong₂ ((_+_) ∘ _% b) (sym p) (·-identityʳ b) ⟩
+      (r + b) % b + b     ≡≤⟨ sym $ cong (_+ b) (mod-rUnit b r) ⟩
+      r % b + b           ≤≡⟨ ≤-+k {k = b} (mod≤L r b) ⟩
+      r + b                ≡⟨ p ⟩
+      a                    ≡⟨ sym $ ≡remainder+quotient b a ⟩
+      a % b + b · (a / b)  ∎
+    where open <-Reasoning
+
+quotient<id : (m n : ℕ) → (quotient suc m / suc (suc n)) < suc m
+quotient<id m n =
+  let
+    a = suc m ; b = suc (suc n) ; b-1 = suc n
+    _/_ = quotient_/_ ; _%_ = remainder_/_
+  in
+    case (a ≟ b) return (λ _ → a / b < a) of λ
+    { (lt a<b) →
+      a / b ≡<⟨ <→quotient≡0 a b a<b ⟩
+      0     <≡⟨ <ᵇ→< tt ⟩
+      a      ∎
+    ; (eq a≡b) →
+      a / b ≡<⟨ cong (_/ b) a≡b ∙ quotientUnipotent b-1 ⟩
+      1     <≡⟨ <ᵇ→< tt ⟩
+      b      ≡⟨ sym a≡b ⟩
+      a      ∎
+    ; (gt b<a) →
+      a / b             ≤<⟨ ≤SumLeft ⟩
+      b-1 · a / b       <≤⟨ <-suc ⟩
+      1 + b-1 · a / b    ≤⟨ ≤-+k (≥→quotient≥1 m b-1 (<-weaken b<a)) ⟩
+      b · a / b         ≤≡⟨ ≤SumRight {k = a % b} ⟩
+      a % b + b · a / b  ≡⟨ ≡remainder+quotient b a ⟩
+      a                  ∎
+    } where open <-Reasoning
+
+quotient<→<· : (m n k : ℕ) → quotient m / suc n < k → m < (suc n) · k
+quotient<→<· m n-1 k m/n<k =
+  let
+    n = suc n-1 ; _/_ = quotient_/_ ; _%_ = remainder_/_
+  in
+    m                 ≡<⟨ sym $ ≡remainder+quotient n m ⟩
+    m % n + n · m / n <≤⟨ <-+k (mod< n-1 m) ⟩
+    n + n · m / n     ≡≤⟨ sym $ ·-suc n (m / n) ⟩
+    n · suc (m / n)   ≤≡⟨ ≤-k· {k = n} m/n<k ⟩
+    n · k              ∎
+  where open <-Reasoning
+
 mod1≡0 : ∀ n → n mod 1 ≡ 0
 mod1≡0 n with (n mod 1) ≟ 0
 ... | lt <0 = ⊥.rec (¬-<-zero <0)

Cubical/Data/Nat/Order.agda

@@ -147,12 +147,23 @@ suc-< p = pred-≤-pred (≤-suc p)
            (d + m) · k   ≡⟨ cong (_· k) r ⟩
            n · k         ∎
 
+≤-k· : m ≤ n → k · m ≤ k · n
+≤-k· {k = k} = subst2 _≤_ (·-comm _ k) (·-comm _ k) ∘ ≤-·k
+
 <-k+-cancel : k + m < k + n → m < n
 <-k+-cancel {k} {m} {n} = ≤-k+-cancel ∘ subst (_≤ k + n) (sym (+-suc k m))
 
 ¬-<-zero : ¬ m < 0
 ¬-<-zero (k , p) = snotz ((sym (+-suc k _)) ∙ p)
 
+≤-·sk-cancel : m · suc k ≤ n · suc k → m ≤ n
+≤-·sk-cancel {zero}  {n = n}     = λ _ → zero-≤
+≤-·sk-cancel {suc m} {n = zero}  = ⊥.rec ∘ ¬-<-zero
+≤-·sk-cancel {suc m} {n = suc n} = suc-≤-suc ∘ ≤-·sk-cancel {m} {n = n} ∘ ≤-k+-cancel
+
+≤-sk·-cancel : suc k · m ≤ suc k · n → m ≤ n
+≤-sk·-cancel {k = k} = ≤-·sk-cancel ∘ subst2 _≤_ (·-comm (suc k) _) (·-comm (suc k) _)
+
 ¬m<m : ¬ m < m
 ¬m<m {m} = ¬-<-zero ∘ ≤-+k-cancel {k = m}
 
@@ -166,6 +177,9 @@ predℕ-≤-predℕ {zero} {suc n}  ineq = zero-≤
 predℕ-≤-predℕ {suc m} {zero}  ineq = ⊥.rec (¬-<-zero ineq)
 predℕ-≤-predℕ {suc m} {suc n} ineq = pred-≤-pred ineq
 
+zero-<suc : zero < suc n
+zero-<suc = suc-≤-suc zero-≤
+
 ¬m+n<m : ¬ m + n < m
 ¬m+n<m {m} {n} = ¬-<-zero ∘ <-k+-cancel ∘ subst (m + n <_) (sym (+-zero m))
 
@@ -238,6 +252,17 @@ predℕ-≤-predℕ {suc m} {suc n} ineq = pred-≤-pred ineq
            (d + suc m) · suc k               ≡⟨ cong (_· suc k) r ⟩
            n · suc k                         ∎
 
+<-sk· : m < n → suc k · m < suc k · n
+<-sk· {k = k} = subst2 _<_ (·-comm _ (suc k)) (·-comm _ (suc k)) ∘ <-·sk {k = k}
+
+<-·sk-cancel : m · suc k < n · suc k → m < n
+<-·sk-cancel {m}     {n = zero}  = ⊥.rec ∘ ¬-<-zero
+<-·sk-cancel {zero}  {n = suc n} = λ _ → zero-<suc
+<-·sk-cancel {suc m} {n = suc n} = suc-≤-suc ∘ <-·sk-cancel {m} {n = n} ∘ <-k+-cancel
+
+<-sk·-cancel : suc k · m < suc k · n → m < n
+<-sk·-cancel {k = k} = <-·sk-cancel ∘ subst2 _<_ (·-comm (suc k) _) (·-comm (suc k) _)
+
 ∸-≤ : ∀ m n → m ∸ n ≤ m
 ∸-≤ m zero = ≤-refl
 ∸-≤ zero (suc n) = ≤-refl
@@ -291,6 +316,34 @@ minGLB {suc m} {suc n} x≤sm x≤sn with m <ᵇ n
 ... | false = x≤sn
 ... | true  = x≤sm
 
+0<^ : ∀ n → 0 < (suc m) ^ n
+0<^ {m} (zero ) = <-suc
+0<^ {m} (suc n) = subst (_< (suc m ^ suc n)) (sym (0≡m·0 (suc m))) (<-sk· {k = m} (0<^ n))
+
+≤-sk^ : m ≤ n → (suc k) ^ m ≤ (suc k) ^ n
+≤-sk^ {zero}  {n}     {k} = λ _ → 0<^ n
+≤-sk^ {suc m} {zero}  {k} = ⊥.rec ∘ ¬-<-zero
+≤-sk^ {suc m} {suc n} {k} = ≤-k· {k = suc k} ∘ ≤-sk^ ∘ pred-≤-pred
+
+1<^suc : ∀ n → 1 < (suc (suc m)) ^ (suc n)
+1<^suc {m} zero    = suc-≤-suc (zero-<suc)
+1<^suc {m} (suc n) = <≤-trans (1<^suc n) (≤-sk^ (≤-sucℕ {suc n}))
+
+<-ssk^ : m < n → (suc (suc k)) ^ m < (suc (suc k)) ^ n
+<-ssk^ {m}     {zero}  {k} = ⊥.rec ∘ ¬-<-zero
+<-ssk^ {zero}  {suc n} {k} = λ _ → 1<^suc n
+<-ssk^ {suc m} {suc n} {k} = <-sk· {k = suc k} ∘ <-ssk^ ∘ pred-≤-pred
+
+≤-ssk^-cancel : (suc (suc k)) ^ m ≤ (suc (suc k)) ^ n → m ≤ n
+≤-ssk^-cancel {k} {zero}  {n}     = λ _ → zero-≤
+≤-ssk^-cancel {k} {suc m} {zero}  = ⊥.rec ∘ <-asym (1<^suc m)
+≤-ssk^-cancel {k} {suc m} {suc n} = suc-≤-suc ∘ ≤-ssk^-cancel ∘ ≤-sk·-cancel {suc k}
+
+<-ssk^-cancel : (suc (suc k)) ^ m < (suc (suc k)) ^ n → m < n
+<-ssk^-cancel {k} {m}     {zero}  = ⊥.rec ∘ flip <-asym (0<^ m)
+<-ssk^-cancel {k} {zero}  {suc n} = λ _ → zero-<suc
+<-ssk^-cancel {k} {suc m} {suc n} = suc-≤-suc ∘ <-ssk^-cancel ∘ <-sk·-cancel {suc k}
+
 -- Boolean order relations and their conversions to/from ≤ and <
 
 _≤ᵇ_ : ℕ → ℕ → Bool