------------------------------------------------------------------------
-- The Agda standard library
--
-- Logarithm base 2 core definitions and properties
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Nat.Logarithm.Core where

open import Data.Nat.Base using (ℕ; _<_; zero; suc; _+_; ⌊_/2⌋; ⌈_/2⌉;
  _≤_; z≤n; s≤s; _∸_; NonZero; _*_; _^_)
open import Data.Nat.Properties
open import Data.Nat.Induction using (<-wellFounded)
open import Induction.WellFounded using (Acc; acc)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; cong; sym)
open import Relation.Binary.PropositionalEquality.Properties
  using (module ≡-Reasoning)

------------------------------------------------------------------------
-- Logarithm base 2

-- Floor version

⌊log2⌋ : ∀ n → Acc _<_ n → ℕ
⌊log2⌋ 0          _        = 0
⌊log2⌋ 1          _        = 0
⌊log2⌋ (suc n′@(suc n)) (acc rs) = 1 + ⌊log2⌋ (suc ⌊ n /2⌋) (rs (⌊n/2⌋<n n′))


-- Ceil version

⌈log2⌉ : ∀ n → Acc _<_ n → ℕ
⌈log2⌉ 0                _        = 0
⌈log2⌉ 1                _        = 0
⌈log2⌉ (suc (suc n)) (acc rs) = 1 + ⌈log2⌉ (suc ⌈ n /2⌉) (rs (⌈n/2⌉<n n))

------------------------------------------------------------------------
-- Properties of ⌊log2⌋

⌊log2⌋-acc-irrelevant : ∀ a {acc acc'} → ⌊log2⌋ a acc ≡ ⌊log2⌋ a acc'
⌊log2⌋-acc-irrelevant 0            {_}      {_}       = refl
⌊log2⌋-acc-irrelevant 1            {_}      {_}       = refl
⌊log2⌋-acc-irrelevant (suc (suc n)) {acc rs} {acc rs'} =
  cong suc (⌊log2⌋-acc-irrelevant (suc ⌊ n /2⌋))

⌊log2⌋-cong-irr : ∀ {a b} {acc acc'} → (p : a ≡ b) →
                ⌊log2⌋ a acc ≡ ⌊log2⌋ b acc'
⌊log2⌋-cong-irr {acc = ac} refl = ⌊log2⌋-acc-irrelevant _ {ac}

⌊log2⌋-mono-≤ : ∀ {a b} {acc acc'} → a ≤ b → ⌊log2⌋ a acc ≤ ⌊log2⌋ b acc'
⌊log2⌋-mono-≤ {_}           {_}     z≤n       = z≤n
⌊log2⌋-mono-≤ {_}           {_}     (s≤s z≤n) = z≤n
⌊log2⌋-mono-≤ {acc = acc _} {acc _} (s≤s (s≤s p)) =
  s≤s (⌊log2⌋-mono-≤ (⌊n/2⌋-mono (+-monoʳ-≤ 2 p)))

⌊log2⌋⌊n/2⌋≡⌊log2⌋n∸1 : ∀ n {acc} {acc'} →
                        ⌊log2⌋ ⌊ n /2⌋ acc ≡ ⌊log2⌋ n acc' ∸ 1
⌊log2⌋⌊n/2⌋≡⌊log2⌋n∸1 0             {_}      {_}       = refl
⌊log2⌋⌊n/2⌋≡⌊log2⌋n∸1 1             {_}      {_}       = refl
⌊log2⌋⌊n/2⌋≡⌊log2⌋n∸1 (suc (suc n)) {acc rs} {acc rs'} =
  ⌊log2⌋-acc-irrelevant (suc ⌊ n /2⌋)

⌊log2⌋2*b≡1+⌊log2⌋b : ∀ n {acc acc'} .{{ _ : NonZero n}} →
                      ⌊log2⌋ (2 * n) acc ≡ 1 + ⌊log2⌋ n acc'
⌊log2⌋2*b≡1+⌊log2⌋b (suc n) = begin
  ⌊log2⌋ (suc (n + suc (n + zero))) _              ≡⟨ ⌊log2⌋-cong-irr (cong (λ x → suc (n + suc x)) (+-comm n zero)) ⟩
  ⌊log2⌋ (suc (n + suc n)) (<-wellFounded _)       ≡⟨ ⌊log2⌋-cong-irr {acc' = <-wellFounded _} (cong suc (+-comm n (suc n))) ⟩
  ⌊log2⌋ (suc (suc n + n)) (<-wellFounded _)       ≡⟨ cong suc (⌊log2⌋-cong-irr {a = suc ⌊ n + n /2⌋} refl) ⟩
  suc (⌊log2⌋ (suc ⌊ n + n /2⌋) (<-wellFounded _)) ≡⟨ cong suc (⌊log2⌋-cong-irr (cong suc (sym (n≡⌊n+n/2⌋ n)))) ⟩
  suc (⌊log2⌋ (suc n) _)                           ∎
  where open ≡-Reasoning

⌊log2⌋2^n≡n : ∀ n {acc} → ⌊log2⌋ (2 ^ n) acc ≡ n
⌊log2⌋2^n≡n zero    = refl
⌊log2⌋2^n≡n (suc n) = begin
  ⌊log2⌋ ((2 ^ n) + ((2 ^ n) + zero)) _ ≡⟨ ⌊log2⌋2*b≡1+⌊log2⌋b (2 ^ n) {{m^n≢0 2 n}} ⟩
  1 + ⌊log2⌋ (2 ^ n) (<-wellFounded _)  ≡⟨ cong suc (⌊log2⌋2^n≡n n) ⟩
  suc n                                 ∎
  where open ≡-Reasoning

------------------------------------------------------------------------
-- Properties of ⌈log2⌉

⌈log2⌉-acc-irrelevant : ∀ n {acc acc'} → ⌈log2⌉ n acc ≡ ⌈log2⌉ n acc'
⌈log2⌉-acc-irrelevant zero          {acc rs} {acc rs₁} = refl
⌈log2⌉-acc-irrelevant (suc zero)    {acc rs} {acc rs₁} = refl
⌈log2⌉-acc-irrelevant (suc (suc n)) {acc rs} {acc rs'} =
  cong suc (⌈log2⌉-acc-irrelevant (suc ⌊ suc n /2⌋))

⌈log2⌉-cong-irr : ∀ {m n} {acc acc'} → (_ : m ≡ n) →
                  ⌈log2⌉ m acc ≡ ⌈log2⌉ n acc'
⌈log2⌉-cong-irr {acc = ac} refl = ⌈log2⌉-acc-irrelevant _ {ac}

⌈log2⌉-mono-≤ : ∀ {m n} {acc acc'} → m ≤ n → ⌈log2⌉ m acc ≤ ⌈log2⌉ n acc'
⌈log2⌉-mono-≤ {_}            {_}       z≤n           = z≤n
⌈log2⌉-mono-≤ {_}            {_}       (s≤s z≤n)     = z≤n
⌈log2⌉-mono-≤ {acc = acc rs} {acc rs'} (s≤s (s≤s p)) =
  s≤s (⌈log2⌉-mono-≤ (⌈n/2⌉-mono (+-monoʳ-≤ 2 p)))

⌈log2⌉⌈n/2⌉≡⌈log2⌉n∸1 : ∀ n {acc} {acc'} →
                        ⌈log2⌉ ⌈ n /2⌉ acc ≡ ⌈log2⌉ n acc' ∸ 1
⌈log2⌉⌈n/2⌉≡⌈log2⌉n∸1 zero          {_}      {_}       = refl
⌈log2⌉⌈n/2⌉≡⌈log2⌉n∸1 (suc zero)    {_}      {_}       = refl
⌈log2⌉⌈n/2⌉≡⌈log2⌉n∸1 (suc (suc n)) {acc rs} {acc rs'} =
  ⌈log2⌉-acc-irrelevant (suc ⌊ suc n /2⌋)

⌈log2⌉2*n≡1+⌈log2⌉n : ∀ n {acc acc'} .{{_ : NonZero n}} →
                      ⌈log2⌉ (2 * n) acc ≡ 1 + ⌈log2⌉ n acc'
⌈log2⌉2*n≡1+⌈log2⌉n (suc n) = begin
  ⌈log2⌉ (suc (n + suc (n + zero))) _              ≡⟨ ⌈log2⌉-cong-irr (cong (λ x → suc (n + suc x)) (+-comm n zero)) ⟩
  ⌈log2⌉ (suc (n + suc n)) (<-wellFounded _)       ≡⟨ ⌈log2⌉-cong-irr {acc' = <-wellFounded _} (cong suc (+-comm n (suc n))) ⟩
  ⌈log2⌉ (suc (suc n + n)) (<-wellFounded _)       ≡⟨ cong suc (⌈log2⌉-cong-irr {m = suc ⌈ n + n /2⌉} refl) ⟩
  suc (⌈log2⌉ (suc ⌈ n + n /2⌉) (<-wellFounded _)) ≡⟨ cong suc (⌈log2⌉-cong-irr (cong suc (sym (n≡⌈n+n/2⌉ n)))) ⟩
  suc (⌈log2⌉ (suc n) _)                           ∎
  where open ≡-Reasoning

⌈log2⌉2^n≡n : ∀ n {acc} → ⌈log2⌉ (2 ^ n) acc ≡ n
⌈log2⌉2^n≡n zero    = refl
⌈log2⌉2^n≡n (suc n) = begin
  ⌈log2⌉ ((2 ^ n) + ((2 ^ n) + zero)) _ ≡⟨ ⌈log2⌉2*n≡1+⌈log2⌉n (2 ^ n) {{m^n≢0 2 n}} ⟩
  1 + ⌈log2⌉ (2 ^ n) (<-wellFounded _)  ≡⟨ cong suc (⌈log2⌉2^n≡n n) ⟩
  suc n                                 ∎
  where open ≡-Reasoning