{-# OPTIONS --safe #-}

open import Level hiding (suc)
open import Data.Sum as ⊎
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Data.Nat.Induction using (<-wellFounded)
open import Induction.WellFounded using (Acc; acc)
open import Data.Nat.Logarithm
open import Data.Nat.Logarithm.Core
open import Data.Sum.Properties as ⊎
open import Function.Base

open import Relation.Binary.PropositionalEquality 

module Utils where

⊎-map₂∘map₂ : ∀ {a b c e : Level} {A : Set a} {B : Set b} {C : Set c} {E : Set e} (f : B → C)  (g : A → B)
            → ⊎.map₂ f ∘ ⊎.map₂ g ≗ ⊎.map₂ {A = E} (f ∘ g)
⊎-map₂∘map₂ {E = E} f g x =
  begin
  ⊎.map₂ f (⊎.map₂ g x) ≡⟨⟩
  ⊎.map id f (⊎.map id g x) ≡⟨ map-map x ⟩
  ⊎.map (id ∘ id) (f ∘ g) x ≡⟨ map-cong (λ _ → refl) (λ _ → refl) x ⟩
  ⊎.map₂ (f ∘ g) x
  ∎
  where open ≡-Reasoning
  
 


-- a helper that iterates an endomap on X with exceptions in R.
-- We interpret the exception R as the teacher surrendering
iterate : ∀ {ℓ ℓr} {X : Set ℓ} {R : Set ℓr} → ℕ → (X → R ⊎ X) → (X → R ⊎ X)
iterate ℕ.zero _ = inj₂
iterate {ℓ} (ℕ.suc n) f q = case (f q) of λ
  { (inj₁ r) → inj₁ r
  ; (inj₂ q') → iterate n f q'
  }


m≤n⇒m+k≡n : ∀ {m n : ℕ} → m ≤ n → Σ[ k ∈ ℕ ] m + k ≡ n
m≤n⇒m+k≡n {m} {n} z≤n = n , refl
m≤n⇒m+k≡n (s≤s {m} {n} m≤n) with (m≤n⇒m+k≡n m≤n)
... | (k , m+k≡n) = k , cong ℕ.suc m+k≡n

2*n≡n+n : ∀ n →  * n ≡ n + n
2*n≡n+n n = (cong (n +_) (+-identityʳ _))

2*suc-n≡2+n+n : ∀ n →  * (ℕ.suc n) ≡  + (n + n)
2*suc-n≡2+n+n n = trans (cong (( + n) +_) (+-identityʳ _)) (+-suc ( + n) n)

2^⌊log2n⌋-acc≤n : ∀ n → (rs : Acc _<_ ( + n)) →  ^ (⌊log2⌋ ( + n) rs) ≤  + n
2^⌊log2n⌋-acc≤n ℕ.zero rs = s≤s z≤n
2^⌊log2n⌋-acc≤n (ℕ.suc n) (acc rs) =
  begin
   ^ (⌊log2⌋ (2+ n) (acc rs))       ≡⟨⟩
   *  ^ (⌊log2⌋ (ℕ.suc ⌊ n /2⌋) _) ≤⟨ *-monoʳ-≤  (2^⌊log2n⌋-acc≤n _ _ ) ⟩
   * (ℕ.suc ⌊ n /2⌋)                ≡⟨ 2*suc-n≡2+n+n _ ⟩
   + (⌊ n /2⌋ + ⌊ n /2⌋)            ≤⟨ +-monoʳ-≤ (2+ ⌊ n /2⌋) (⌊n/2⌋≤⌈n/2⌉ _)  ⟩
   + (⌊ n /2⌋ + ⌈ n /2⌉)            ≡⟨ cong ( +_) (⌊n/2⌋+⌈n/2⌉≡n _) ⟩
  2+ n
  ∎
  where open ≤-Reasoning

2^⌊log₂n⌋≤n : ∀ n → .{{ _ : NonZero n }} →  ^ ⌊log₂ n ⌋ ≤ n
2^⌊log₂n⌋≤n (ℕ.suc n) = 2^⌊log2n⌋-acc≤n n (<-wellFounded (ℕ.suc n))

2^⌊log₂n⌋≤1+n : ∀ n →  ^ ⌊log₂ n ⌋ ≤  + n
2^⌊log₂n⌋≤1+n ℕ.zero = s≤s z≤n
2^⌊log₂n⌋≤1+n (suc n) = ≤-trans (2^⌊log₂n⌋≤n (suc n)) (s≤s (m≤n+m n ))

n≤2^⌈log2n⌉-acc : ∀ n → (rs : Acc _<_ n) → n ≤  ^ (⌈log2⌉ n rs)
n≤2^⌈log2n⌉-acc ℕ.zero _ = z≤n
n≤2^⌈log2n⌉-acc (ℕ.suc ℕ.zero) _ = s≤s z≤n
n≤2^⌈log2n⌉-acc (2+ n) (acc rs) =
  begin
  2+ n ≡⟨ cong 2+ (⌊n/2⌋+⌈n/2⌉≡n _) ⟨
  2+ (⌊ n /2⌋ + ⌈ n /2⌉) ≤⟨ +-monoʳ-≤  (+-monoˡ-≤ _ (⌊n/2⌋≤⌈n/2⌉ n)) ⟩
  2+ (⌈ n /2⌉ + ⌈ n /2⌉) ≡⟨ 2*suc-n≡2+n+n _ ⟨
   * ( + ⌊  + n /2⌋) ≤⟨ *-monoʳ-≤  (n≤2^⌈log2n⌉-acc ( + ⌊  + n /2⌋) _) ⟩
   *  ^ (⌈log2⌉ ( + ⌊  + n /2⌋) _) ≡⟨⟩
   ^ (⌈log2⌉ (2+ n) (acc rs))
  ∎
  where open ≤-Reasoning

n≤2^⌈log₂n⌉ : ∀ n → n ≤  ^ ⌈log₂ n ⌉
n≤2^⌈log₂n⌉ n = n≤2^⌈log2n⌉-acc n (<-wellFounded n)

⌊n*2+1/2⌋≡⌊n*2/2⌋ : ∀ n →   ⌊ n *  +  /2⌋ ≡ ⌊ n *  /2⌋
⌊n*2+1/2⌋≡⌊n*2/2⌋ ℕ.zero = refl
⌊n*2+1/2⌋≡⌊n*2/2⌋ (ℕ.suc n) = cong ℕ.suc (⌊n*2+1/2⌋≡⌊n*2/2⌋ n)

⌊2*n+1/2⌋≡⌊2*n/2⌋ : ∀ n →   ⌊  * n +  /2⌋ ≡ ⌊  * n /2⌋
⌊2*n+1/2⌋≡⌊2*n/2⌋ n = begin
  ⌊  * n +  /2⌋ ≡⟨ cong (λ - → ⌊ - +  /2⌋) (*-comm  n) ⟩
  ⌊ n *  +  /2⌋ ≡⟨ ⌊n*2+1/2⌋≡⌊n*2/2⌋ n ⟩
  ⌊ n *  /2⌋ ≡⟨ cong ⌊_/2⌋ (*-comm n ) ⟩
  ⌊  * n /2⌋ 
  ∎
  where open ≡-Reasoning

-- some adjunctions
-- 
⌊_/2⌋-adj : ∀ {b} {m} → b ≤  * m +  → ⌊ b /2⌋ ≤ m
⌊_/2⌋-adj {b} {m} b≤m = begin
  ⌊ b /2⌋ ≤⟨ ⌊n/2⌋-mono b≤m ⟩
  ⌊  * m +  /2⌋ ≡⟨ ⌊2*n+1/2⌋≡⌊2*n/2⌋ m ⟩
  ⌊  * m /2⌋ ≡⟨ cong ⌊_/2⌋ (2*n≡n+n m) ⟩
  ⌊ m + m /2⌋ ≡⟨ n≡⌊n+n/2⌋ m ⟨
  m
  ∎
  where open ≤-Reasoning

2^⇒⌊log₂n⌋ : ∀ k n .{{ _ : NonZero n }} →  ^ k ≤ n → k ≤ ⌊log₂ n ⌋
2^⇒⌊log₂n⌋ k (ℕ.suc n) 2^k≤n = begin
  k                  ≡⟨ ⌊log₂[2^n]⌋≡n k ⟨
  ⌊log₂  ^ k ⌋      ≤⟨ ⌊log₂⌋-mono-≤ 2^k≤n ⟩
  ⌊log₂ ( + n) ⌋    ∎
  where open ≤-Reasoning

⌊log₂n⌋⇒2^ : ∀ k n .{{ _ : NonZero n }} → k ≤ ⌊log₂ n ⌋ →  ^ k ≤ n 
⌊log₂n⌋⇒2^ k n k≤log[n] = begin
   ^ k           ≤⟨ ^-monoʳ-≤  k≤log[n] ⟩
   ^ ⌊log₂ n ⌋   ≤⟨ 2^⌊log₂n⌋≤n n ⟩
  n               ∎
  where open ≤-Reasoning

≤-suc-pred : ∀ {m} → m ≤ suc (pred m)
≤-suc-pred {ℕ.zero} = z≤n
≤-suc-pred {suc m} = ≤-reflexive refl

>m-nonZero : ∀ {n} {m} → n > m → NonZero n
>m-nonZero n>m = >-nonZero (≤-<-trans z≤n n>m)

pred-≤ : ∀ {n} → pred n ≤ n
pred-≤ {ℕ.zero} = z≤n
pred-≤ {suc n} = help n
  where
    help : ∀ k → k ≤ suc k
    help ℕ.zero = z≤n
    help (suc k) = s≤s (help k)

bisect-sum : ∀ {c} {m} {k} →  ^ ( + c) ≤ m + k → k ≤ m →  ^ c ≤ m
bisect-sum {c} {m} {k} 2^suc[c]≤m+k k≤m = *-cancelˡ-≤  (begin
       *  ^ c ≡⟨⟩
       ^ (suc c) ≤⟨ 2^suc[c]≤m+k ⟩
      m + k ≤⟨ +-monoʳ-≤ m k≤m ⟩
      m + m ≡⟨ 2*n≡n+n m ⟨
       * m
      ∎)
  where
    open ≤-Reasoning

2*n≤2*k+1⇒n≤k : ∀ n k →  * n ≤  +  * k → n ≤ k
2*n≤2*k+1⇒n≤k n k ineq = begin
  n ≡⟨ n≡⌊n+n/2⌋ n ⟩
  ⌊ n + n /2⌋ ≡⟨ cong ⌊_/2⌋ (2*n≡n+n n) ⟨
  ⌊  * n /2⌋ ≤⟨ ⌊n/2⌋-mono ineq ⟩
  ⌊  +  * k /2⌋ ≡⟨ cong ⌊_/2⌋ (+-comm  _) ⟩
  ⌊  * k +  /2⌋ ≡⟨ ⌊2*n+1/2⌋≡⌊2*n/2⌋ k ⟩
  ⌊  * k /2⌋ ≡⟨ cong ⌊_/2⌋ (2*n≡n+n k) ⟩
  ⌊ k + k /2⌋ ≡⟨ n≡⌊n+n/2⌋ k ⟨
  k
  ∎
  where
    open ≤-Reasoning

2^c≤1+k : ∀ c k →  ^ (suc c) ≤  +  * k →  ^ c ≤  + k
2^c≤1+k c k ax = bisect-sum {c} { + k} {k + } ax k0≤k1 
  where
    open ≤-Reasoning
    k0≤k1 : k +  ≤  + k
    k0≤k1 = ≤-trans (≤-reflexive (+-identityʳ k)) (m≤n+m k )

2^k≤m⇒0<m : ∀ {k} {m} →  ^ k ≤ m →  < m
2^k≤m⇒0<m {ℕ.zero} {m} ineq = ineq
2^k≤m⇒0<m {suc k} {m} ineq = 2^k≤m⇒0<m {k} {m} (≤-trans (^-monoʳ-≤  (m≤n+m k )) ineq)

2^k<m<2^suc[k]⇒0<k : ∀ {k} {m} →  ^ k < m → m <  ^ ( + k) →  < k
2^k<m<2^suc[k]⇒0<k {ℕ.zero} {suc ℕ.zero} (s≤s ()) _
2^k<m<2^suc[k]⇒0<k {ℕ.zero} {2+ m} _ (s≤s (s≤s ()))
2^k<m<2^suc[k]⇒0<k {suc k} {m} _ _ = s≤s z≤n