⟨ Index | Module NatExamples.LogLearner 
{-# OPTIONS --safe #-}

open import Level using (0ℓ)
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Nat as ℕ hiding (_⊔_)
open import Data.Nat.Properties
open import Data.Nat.Logarithm
import Data.Nat.Properties as ℕ
open import Relation.Binary.PropositionalEquality.Core

open import NatLearning
open import Learner-Correctness ℕ F NatLearning-Semantics

open import Utils

module NatExamples.LogLearner where

-- A learner that guesses a secret k within 2 + 2 * log(k) steps.

bound : ℕ → ℕ
bound sec = 3 + ⌊log₂ sec ⌋ + ⌊log₂ sec ⌋

data LogLearner : Set where
  0≤ : LogLearner
  2^_< : (k : ℕ) → LogLearner
  [_,+2^_,_] : (b : ℕ) → (e : ℕ) → e ≤ ⌊log₂ b ⌋ → LogLearner

-- instead of commenting on the semantics of above constructors,
-- we directly *define* the semantics:
_∋_ : LogLearner → ℕ → Set
-- Case 1: the secret is greater or equal than 0 (we know nothing)
_∋_ 0≤ sec = ⊤
-- Case 2: the secret is greater than 2 ^ k
_∋_ 2^ k < sec = 2 ^ k < sec
-- Case 3: the secret is greater or equal b, but less than 2 ^ e steps away from b.
-- Here, we could also give a tighter bound, but this interval
-- is simpler and still achieves the logarithmic runtime.
_∋_ [ b ,+2^ e , _ ] sec = b ≤ sec × sec < b + 2 ^ e

-- Initially, we only know that the secret is ≥ 0
q₀ : LogLearner
q₀ = 0≤

δ : LogLearner → F ℕ LogLearner 
δ 0≤ = guess 1 1 λ
  { too-high → [ 0 ,+2^ 0 , z≤n ] -- the secret must be 0, i.e. < 0 + 2^0
  ; too-low → 2^ 0 < -- the secret is greater than 1=2^0
  }
δ 2^ k < = guess (2 ^ suc k) (2 ^ suc k) λ
  -- if 2 ^ (1 + k) is too high, then the secret is within
  --  [1 + 2 ^ k , 2 ^ (k + 1) - 1]
  { too-high → [ (2 ^ k) ,+2^ k , ≤-reflexive (sym (⌊log₂[2^n]⌋≡n k)) ]
  ; too-low → 2^ (suc k) <
  }
δ [ b ,+2^ 0 , _ ] =
  -- the secret is greater/equal b but must be < b + 2^0.
  -- So it is necessarily b and the 'next' state does
  -- not matter, because it can't be reached anyway.
  guess b b (λ _ → q₀)
δ [ b ,+2^ suc e , ineq ] =
  -- divide the interval [ b , b + 2^(1+e) ) by two:
  guess (b + 2 ^ e) (b + 2 ^ e) λ
  -- and in the next state, enter either the left
  -- or the right half
  { too-high → [ b ,+2^ e , e≤⌊log₂b⌋ ]
  ; too-low → [ b + 2 ^ e ,+2^ e , ≤-trans e≤⌊log₂b⌋ (⌊log₂⌋-mono-≤ (m≤m+n b (2 ^ e))) ]
  }
  where
    e≤⌊log₂b⌋ : e ≤ ⌊log₂ b ⌋ 
    e≤⌊log₂b⌋ = ≤-trans (m≤n+m e 1) ineq

ticks : LogLearner → ℕ
ticks 0≤ = 0
ticks 2^ k < = 1 + k
ticks [ b ,+2^ e , _ ] = 2 + ⌊log₂ b ⌋ + (⌊log₂ b ⌋ ∸ e)

in-time : ∀ q sec → q ∋ sec → ticks q < bound sec
in-time 0≤ sec tt = s≤s z≤n
in-time 2^ k < (suc sec) (s≤s 2^k≤n) = (begin -- +-monoʳ-≤ 1 
  1 + ticks (2^ k <)    ≡⟨⟩
  2 + k             ≤⟨ +-monoʳ-≤ 2 (2^⇒⌊log₂n⌋ k (sec) 2^k≤n ) ⟩
  2 + ⌊log₂ sec ⌋ ≤⟨ +-monoʳ-≤ 2 (⌊log₂⌋-mono-≤ (m≤n+m sec 1)) ⟩
  2 + ⌊log₂ suc sec ⌋ ≤⟨ +-monoʳ-≤ 2 (m≤n+m _ (1 + ⌊log₂ suc sec ⌋)) ⟩
  3 + ⌊log₂ suc sec ⌋ + ⌊log₂ suc sec ⌋
  ∎)
  where
    open ≤-Reasoning
    instance
      sec-nonzero : NonZero sec
      sec-nonzero = >m-nonZero (2^k≤m⇒0<m {k} {_} 2^k≤n)

in-time [ b ,+2^ e , _ ] sec (b≤sec , sec<b+2^e) = +-monoʳ-≤ 3 (begin
  ⌊log₂ b ⌋ + (⌊log₂ b ⌋ ∸ e)  ≤⟨ +-monoʳ-≤ ⌊log₂ b ⌋ (m∸n≤m _ e) ⟩
  ⌊log₂ b ⌋ + ⌊log₂ b ⌋  ≤⟨ +-mono-≤ (⌊log₂⌋-mono-≤ b≤sec) (⌊log₂⌋-mono-≤ b≤sec) ⟩
  ⌊log₂ sec ⌋ + ⌊log₂ sec ⌋
  ∎)
  where open ≤-Reasoning

δ-preserves-∋ : ∀ {q} {sec} → q ∋ sec → ⟦F δ q ⟧ ⊧F∀ λ {(_∈resp , q') → sec ∈resp → q' ∋ sec × ticks q < ticks q'}
δ-preserves-∋ {0≤} {sec} 0≤sec = λ
  { too-high sec<1 → (z≤n , sec<1) , s≤s z≤n
  ; too-low 1<sec → 1<sec , s≤s z≤n
  }
δ-preserves-∋ {2^ k <} {sec} 2^k<sec = λ
  { too-high sec<2^suc[k] →
             (<⇒≤ 2^k<sec , subst (sec <_) (2*n≡n+n (2 ^ k)) sec<2^suc[k])
             , s≤s (s≤s (begin
               k ≡⟨ ⌊log₂[2^n]⌋≡n k ⟨
               ⌊log₂ 2 ^ k ⌋ ≤⟨ m≤m+n ⌊log₂ 2 ^ k ⌋ _ ⟩
               ⌊log₂ 2 ^ k ⌋ + (⌊log₂ 2 ^ k ⌋ ∸ k)
               ∎))
  ; too-low 2^suc[k]<sec → 2^suc[k]<sec , s≤s (s≤s ≤-refl)
  }
  where open ≤-Reasoning

δ-preserves-∋ {[ b ,+2^ zero , x ]} {sec} (b≤sec , sec<b+1) =
  let
    b≡sec : b ≡ sec
    b≡sec = ≤-antisym b≤sec (≤-pred (subst (_<_ sec) (+-comm b 1) sec<b+1))
  in
  λ
  { too-high b>sec → ⊥-elim (<⇒≢ b>sec (sym b≡sec))
  ; too-low b<sec → ⊥-elim (<⇒≢ b<sec b≡sec)
  }
δ-preserves-∋ {[ b ,+2^ suc e , ineq-1+e≤⌊log₂b⌋ ]} {sec} (b≤sec , sec<2^suc[e]) =
  let
    tick-decreases = begin
      suc (2 + ⌊log₂ b ⌋ + (⌊log₂ b ⌋ ∸ suc e)) ≡⟨⟩
      (3 + ⌊log₂ b ⌋ + (⌊log₂ b ⌋ ∸ suc e)) ≡⟨ cong (2 +_) (+-suc _ _) ⟨
      (2 + ⌊log₂ b ⌋ + suc (⌊log₂ b ⌋ ∸ suc e)) ≤⟨ +-monoʳ-≤ (2 + ⌊log₂ b ⌋) (∸-monoʳ-< (≤-reflexive refl) ineq-1+e≤⌊log₂b⌋) ⟩
      -- ^--- this is the only argument in the entire file where we use the inequality ineq-1+e≤⌊log₂b⌋
      2 + ⌊log₂ b ⌋ + (⌊log₂ b ⌋ ∸ e)
      ∎
  in
  λ
  { too-high sec<b+2^e → (b≤sec , sec<b+2^e)
    , tick-decreases
  ; too-low b+2^e<sec → (<⇒≤ b+2^e<sec , (begin
        suc sec ≤⟨ sec<2^suc[e] ⟩
        b + 2 ^ (1 + e)  ≡⟨ cong (b +_) (2*n≡n+n (2 ^ e)) ⟩
        b + (2 ^ e + 2 ^ e) ≡⟨ +-assoc b _ _ ⟨
        (b + 2 ^ e) + 2 ^ e
        ∎)
    ) , (begin
      suc (2 + ⌊log₂ b ⌋ + (⌊log₂ b ⌋ ∸ suc e)) ≤⟨ tick-decreases ⟩
      2 + ⌊log₂ b ⌋ + (⌊log₂ b ⌋ ∸ e) ≤⟨ +-monoʳ-≤ 2 (+-mono-≤ (⌊log₂⌋-mono-≤ (m≤m+n b _)) (∸-monoˡ-≤ e (⌊log₂⌋-mono-≤ (m≤m+n b _)))) ⟩
      2 + ⌊log₂ b + 2 ^ e ⌋ + (⌊log₂ b + 2 ^ e ⌋ ∸ e)
      ∎)
  }
  where open ≤-Reasoning

log-learner : Learner 0ℓ
log-learner = record { C = LogLearner ; R = ℕ ; q₀ = q₀ ; learner-on = record { δ = δ } }

logLearnStepBounded : Learner-Stepping δ q₀ bound
logLearnStepBounded = record
  { ticks = ticks
  ; allows = _∋_
  ; q₀-correct = λ sec → tt
  ; ticks-below-bound = in-time
  ; preserve = δ-preserves-∋
  }

log-learner-bound : ∀ {ℓt} (teacher : NatTeacher ℓt)
                       → log-learner defeats teacher with-bound (λ d → 3 + ⌊log₂ d ⌋ + ⌊log₂ d ⌋)
log-learner-bound teacher =
  Correctness.learner-correct
    (Teacher.teacher-on (mkTeacher teacher))
    (Learner.learner-on log-learner)
    (Learner.q₀ log-learner) (bound) logLearnStepBounded (NatTeacher.st₀ teacher)