{-# OPTIONS --safe #-}
-- -----------------------------------------
-- An example definition of the simplest teacher
-- possible: initialized with a number, the teacher
-- answers all queries entirely honestly
-- -----------------------------------------
import Level as L
open import Level using (Level)

open import Data.Empty
open import Data.Nat as ℕ hiding (_⊔_)
open import Data.Nat.Properties as ℕ
open import Data.Nat
open import Data.Nat.Logarithm
open import Data.Maybe using (Maybe; just; nothing)
import Data.Maybe as Maybe
open import Data.Product as Σ
open import Data.Sum as ⊎
open import Data.Unit
open import Function.Base
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions
open import Relation.Unary
open import Relation.Nullary
open import Utils

module NatExamples.HonestTeacher {ℓr : Level} (R : Set ℓr) where
open import NatLearning

honest-teacher : ℕ → Teacherδ ⊤
honest-teacher secret = mkTeacherδ λ { tt hyp →
      case (<-cmp secret hyp) of λ
      { (tri≈ _ secret≡hyp _) → nothing
      ; (tri< secret<hyp _ _) → just (too-high , tt)
      ; (tri> _ _ secret>hyp) → just (too-low , tt)
      }
  }