Polynomial-vs-Exponential-Growth (Polynomial-vs-Exponential-Growth)

{-# OPTIONS --safe  #-}

-- -- Polynomial vs Exponential Growth ----------------------------------------
-- Lemmas showing that exponential functions grow faster than any
-- polynomial function ℕ → ℕ
-- ----------------------------------------------------------------------------

open import Level hiding (_⊔_)
import DFA as D
open import Data.Nat as ℕ
open import Data.List
import Data.Nat.Properties as ℕ
open import Data.Product
open import Function.Base
open import Data.Nat.Logarithm
open import Relation.Binary.PropositionalEquality
open import Utils

module Polynomial-vs-Exponential-Growth where


Polynomial : Set
Polynomial = List (ℕ × ℕ)

⟦poly_⟧[_] : Polynomial → ℕ → ℕ
⟦poly [] ⟧[ x ] = 0
⟦poly (coeff , power) ∷ p ⟧[ x ] = coeff * x ^ power + ⟦poly p ⟧[ x ]

-- -- Examples / sanity checks:
poly-example1 : ∀ x → ⟦poly (4 , 0) ∷ [] ⟧[ x ] ≡ 4
poly-example1 x = refl

poly-example2 : ∀ x → ⟦poly (5 , 2) ∷ (3 , 2) ∷ (4 , 0) ∷ [] ⟧[ x ] ≡ 5 * x ^ 2 + (3 * x ^ 2 + 4)
poly-example2 x = refl

n<2^n : ∀ n → n < 2 ^ n
n<2^n ℕ.zero = s≤s z≤n
n<2^n (ℕ.suc ℕ.zero) = s≤s (s≤s z≤n)
n<2^n (2+ n) = begin
  2 + (ℕ.suc n) ≤⟨ ℕ.+-monoʳ-≤ 2 (n<2^n n) ⟩
  2 + 2 ^ n ≡⟨ cong (2 +_) (ℕ.*-identityˡ (2 ^ n)) ⟨
  2 * 1 + 1 * 2 ^ n ≤⟨ ℕ.+-mono-≤ (ℕ.*-monoʳ-≤ 2 (ℕ.m^n>0 2 n)) (ℕ.*-monoˡ-≤ (2 ^ n) ((1 ≤ 2) ∋ s≤s z≤n)) ⟩
  2 * 2 ^ n + 2 * 2 ^ n ≡⟨ 2*n≡n+n (2 * 2 ^ n) ⟨
  2 * (2 * 2 ^ n) ≡⟨⟩
  2 ^ 2+ n
  ∎
  where open ℕ.≤-Reasoning

ℓ*m*n≡ℓ*n*m : ∀ ℓ m n → ℓ * m * n ≡ ℓ * n * m
ℓ*m*n≡ℓ*n*m ℓ m n = begin
  ℓ * m * n ≡⟨ ℕ.*-assoc ℓ m n ⟩
  ℓ * (m * n) ≡⟨ cong (ℓ *_) (ℕ.*-comm m n) ⟩
  ℓ * (n * m) ≡⟨ ℕ.*-assoc ℓ n m ⟨
  ℓ * n * m
  ∎
  where open ≡-Reasoning

n^b<2^n : ∀ (b : ℕ) → ∃[ n ] (n ≥ 2) × (n ^ b) < 2 ^ n
n^b<2^n ℕ.zero = 2 , (s≤s (s≤s z≤n) , s≤s (s≤s z≤n)) -- 1 , s≤s (s≤s z≤n)
n^b<2^n b@(suc _ ) = n , n≥2 , (begin
  ℕ.suc (n ^ b) ≡⟨⟩
  ℕ.suc (n ^ b) ≤⟨ ℕ.^-monoˡ-< b n<2^2m ⟩
  (2 ^ (2 * m)) ^ b ≡⟨ ℕ.^-*-assoc 2 (2 * m) b ⟩
  2 ^ (2 * m * b) ≡⟨  cong (2 ^_) (ℓ*m*n≡ℓ*n*m 2 m b) ⟩
  2 ^ (2 * b * m) ≡⟨⟩
  2 ^ n
  ∎)
  where
    m : ℕ
    m = ⌈log₂ 2 * b ⌉
    n : ℕ
    n = 2 * b * m

    open ℕ.≤-Reasoning

    2≤2b : 2 ≤ 2 * b
    2≤2b = (2 * 1 ≤ 2 * b) ∋  ℕ.*-monoʳ-≤ 2 ((1 ≤ b) ∋ s≤s z≤n)

    n≥2 : n ≥ 2
    n≥2 = begin
      2 ≡⟨⟩
      2 * ⌈log₂ 2 ⌉ ≤⟨ ℕ.*-mono-≤ 2≤2b (⌈log₂⌉-mono-≤ 2≤2b) ⟩
      2 * b * ⌈log₂ 2 * b ⌉
      ∎

    2b<2^m : 2 * b ≤ 2 ^ m
    2b<2^m = n≤2^⌈log₂n⌉ (2 * b)

    m<2^m : m < 2 ^ m
    m<2^m = n<2^n m
    -- Reasoning under the b'th root:
    n<2^2m : n < 2 ^ (2 * m)
    n<2^2m = begin
      ℕ.suc n ≡⟨⟩
      ℕ.suc (2 * b * m) ≤⟨ ℕ.*-monoʳ-< (2 * b) m<2^m ⟩
      (2 * b) * 2 ^ m ≤⟨ ℕ.*-monoˡ-≤ (2 ^ m) 2b<2^m ⟩
      2 ^ m * 2 ^ m ≡⟨ ℕ.^-distribˡ-+-* 2 m m ⟨
      2 ^ (m + m) ≡⟨ cong (2 ^_) (2*n≡n+n m) ⟨
      2 ^ (2 * m)
      ∎

cn^b<2^n : ∀ (c b : ℕ) → ∃[ n ] (n ≥ 2) × c * (n ^ b) < 2 ^ n
cn^b<2^n c b = n , (n≥2 , (begin
  ℕ.suc (c * n ^ b) ≤⟨ ℕ.+-monoʳ-≤ 1 cn^b≡n^blog ⟩
  ℕ.suc (n ^ (b + ⌈log₂ c ⌉)) ≤⟨ n^blog<2^n ⟩
  2 ^ n
  ∎
  ))
  where
    n,n^blog<2^n : ∃[ n ] (n ≥ 2) × (n ^ (b + ⌈log₂ c ⌉)) < 2 ^ n
    n,n^blog<2^n = n^b<2^n (b + ⌈log₂ c ⌉)

    n : ℕ
    n = proj₁ n,n^blog<2^n

    n≥2 : n ≥ 2
    n≥2 = proj₁ (proj₂ n,n^blog<2^n)

    n^blog<2^n : n ^ (b + ⌈log₂ c ⌉) < 2 ^ n
    n^blog<2^n = proj₂ (proj₂ n,n^blog<2^n)

    open ℕ.≤-Reasoning

    cn^b≡n^blog : c * n ^ b ≤ n ^ (b + ⌈log₂ c ⌉)
    cn^b≡n^blog = begin
      c * (n ^ b) ≡⟨ ℕ.*-comm c (n ^ b) ⟩
      (n ^ b) * c ≤⟨ ℕ.*-monoʳ-≤ (n ^ b) (n≤2^⌈log₂n⌉ c) ⟩
      (n ^ b) * 2 ^ ⌈log₂ c ⌉ ≤⟨ ℕ.*-monoʳ-≤ (n ^ b) (ℕ.^-monoˡ-≤ ⌈log₂ c ⌉ n≥2 ) ⟩ --- ℕ.*-monoʳ-≤ {!n ^ b!} {!!} ⟩
      (n ^ b) * n ^ ⌈log₂ c ⌉ ≡⟨ ℕ.^-distribˡ-+-* n b _ ⟨
      n ^ (b + ⌈log₂ c ⌉)
      ∎

c2+n^b<2^n : ∀ (c b : ℕ) → ∃[ n ] c * ((2 + n) ^ b) < 2 ^ n
c2+n^b<2^n c b with (cn^b<2^n (4 * c) b)
... | ℕ.suc ℕ.zero , s≤s () , _
... | (2+ n) , _ , ineq = n , ℕ.*-cancelˡ-< 4 _ _ (begin
  ℕ.suc (4 * (c * (2 + n) ^ b)) ≡⟨ cong ℕ.suc (ℕ.*-assoc 4 c _) ⟨
  ℕ.suc ((4 * c) * (2 + n) ^ b) ≤⟨ ineq ⟩
  2 ^ (2 + n) ≡⟨⟩
  2 * (2 * 2 ^ n) ≡⟨ ℕ.*-assoc 2 2 (2 ^ n) ⟨
  4 * 2 ^ n
  ∎)
  where
    open ℕ.≤-Reasoning

poly≤cn^b : ∀ P → ∃[ c ] ∃[ b ] ∀ n → .⦃ _ : NonZero n ⦄ → ⟦poly P ⟧[ n ] ≤ c * (n ^ b)
poly≤cn^b [] = 0 , (0 , λ n → z≤n)
poly≤cn^b ((c' , b') ∷ P) =
  let c , b , P≤cn^b = poly≤cn^b P in
  (c' + c) , b' ℕ.⊔ b , λ n →
    begin
    c' * n ^ b' + ⟦poly P ⟧[ n ] ≤⟨ ℕ.+-monoʳ-≤ _ (P≤cn^b n) ⟩
    c' * n ^ b' + c * n ^ b ≤⟨ ℕ.+-mono-≤ (ℕ.*-monoʳ-≤ c' (ℕ.^-monoʳ-≤ n (ℕ.m≤m⊔n b' b))) (ℕ.*-monoʳ-≤ c (ℕ.^-monoʳ-≤ n (ℕ.m≤n⊔m b' b))) ⟩
    c' * n ^ (b' ℕ.⊔ b) + c * n ^ (b' ℕ.⊔ b) ≡⟨ ℕ.*-distribʳ-+ _ c' c  ⟨
    (c' + c) * n ^ (b' ℕ.⊔ b)
    ∎
  where
    open ℕ.≤-Reasoning

poly[2+n]<k^n : ∀ k P → k ≥ 2 → ∃[ n ] ⟦poly P ⟧[ 2 + n ] < k ^ n
poly[2+n]<k^n k P k≥2 =
  let
    c , b , P≤cn^b = poly≤cn^b P
    n , c2n^b<2^n = c2+n^b<2^n c b
  in
  n , (begin
  ℕ.suc ⟦poly P ⟧[ 2 + n ] ≤⟨ ℕ.+-monoʳ-≤ 1 (P≤cn^b (2 + n)) ⟩
  ℕ.suc (c * (2 + n) ^ b) ≤⟨ c2n^b<2^n ⟩
  2 ^ n ≤⟨ ℕ.^-monoˡ-≤ n k≥2 ⟩
  k ^ n
  ∎)
  where
    open ℕ.≤-Reasoning