{-# OPTIONS --safe #-}

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

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

module NatExamples.LinearLearner where

-- we simply output the learned secret as the outcome of
-- the learning game
R : Set
R = ℕ

record LinearLearner : Set where
  constructor lower-bound
  field
    lower-bound : ℕ

-- the state means that the learner knows that the
-- hidden number is greater or equal 'lower-bound'
P : LinearLearner → ℕ → Set
P (lower-bound b) = b ≤_

δ : LinearLearner → F R LinearLearner 
δ (lower-bound b) =
  guess b b λ
  { too-high → lower-bound b -- contradiction! so anything is OK
  ; too-low → lower-bound (ℕ.suc b) -- increase lower bound by 1
  }

q₀ : LinearLearner
q₀ = lower-bound 

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

linearLearnCorrect : Learner-Stepping δ q₀ (λ n →  + n)
linearLearnCorrect =
  record
  { ticks = LinearLearner.lower-bound
  ; allows = P
  ; q₀-correct = λ n → z≤n
  ; ticks-below-bound = λ { (lower-bound b) n b≤n → s≤s b≤n }
  ; preserve = λ
    { {lower-bound b} b≤n too-high b>n → ⊥-elim (ℕ.<⇒≱ b>n b≤n)
    ; {lower-bound b} b≤n too-low b<n → b<n , s≤s (ℕ.≤-reflexive refl)
    }
  }

linear-learner-bound : ∀ {ℓt} (teacher : NatTeacher ℓt)
                       → linear-learner defeats teacher with-bound ( +_)
linear-learner-bound teacher =
  Correctness.learner-correct
    (Teacher.teacher-on (mkTeacher teacher))
    (Learner.learner-on linear-learner)
    (Learner.q₀ linear-learner) ( +_) linearLearnCorrect (NatTeacher.st₀ teacher)