{-# OPTIONS --safe #-}
open import Level hiding (suc)
import Level as L

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; map)
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.GuessingLearner {ℓr : Level} (R : Set ℓr) (ret : ℕ → R) where
open import NatLearning


learnerδ : Learnerδ R (Lift ℓr ℕ)
learnerδ (lift n) = guess n (ret n) λ
  { too-high → lift (pred n)
  ; too-low → lift (suc n)
  }

lucky-first-guess : ℕ → Learner ℓr
lucky-first-guess init = record
  { C = Lift ℓr ℕ
  ; R = R
  ; q₀ = lift init
  ; learner-on = record
    { δ = learnerδ
    }
  }


-- A set X is (at most) singleton, if all its elements are equal
IsSingleton : ∀ {ℓ} (X : Set ℓ) → Set ℓ
IsSingleton X = ∀ (x x' : X) → x ≡ x'

module StatelessTeacher {ℓt} (teacher : NatTeacher ℓt) (singleton : IsSingleton (NatTeacher.T teacher)) where
    -- open Game teacher learner
    module teacher = NatTeacher teacher
    open Game NatLearning-Semantics (mkTeacherδ teacher.δ) learnerδ

    -- If the teacher answers 'nothing', the learner wins:
    case-nothing : (n : ℕ) (st : teacher.T) → teacher.δ st n ≡ nothing
          → (∀ sec → learner (st , lift n) finds sec within  rounds)
    case-nothing n st eq sec rewrite eq = tt


    -- Some special cases where the teacher
    -- gives contradictory answers:
    -- The number 0 can't be too high:
    case-zero-too-high : (st : teacher.T)
                         → ∃[ st' ] teacher.δ st  ≡ just (too-high , st')
                         → ∀ sec → learner (st , lift ) finds sec within  rounds
    case-zero-too-high st (st' , eq) sec rewrite eq =
      λ 1≤0 → case 1≤0 of λ ()

    -- If there is a number that is too high and its predecessor is too low,
    -- then this is a contradiction, so the learner wins:
    case-<> : (n : ℕ) (st : teacher.T)
            → ∃[ st' ] ∃[ st'' ] teacher.δ st (suc n) ≡ just (too-high , st')
                             × teacher.δ st' n ≡ just (too-low , st'')
            → ∀ sec → learner (st , lift (suc n)) finds sec within  rounds
    case-<> n st (st' , st'' , eq1 , eq2) rewrite eq1 rewrite eq2 = λ
       { ℕ.zero 1≤suc[n] suc[n]≤0 → case suc[n]≤0 of λ ()
       ; (suc sec) (s≤s 1+sec≤n) (s≤s n≤sec) → <-irrefl refl (≤-trans 1+sec≤n n≤sec)
       }

    case-too-high : (n : ℕ) (st : teacher.T) → (∃[ st' ] teacher.δ st n ≡ just (too-high , st'))
          → ∃[ q₀ ] ∀ sec → (learner (st , lift q₀) finds sec within  rounds)
    case-too-high ℕ.zero st (st' , eq) =  , case-zero-too-high st (st' , eq)
    case-too-high (suc n) st (st' , eq) with (teacher.δ st' n) in eq'
    ... | nothing rewrite (singleton st st') = n , (case-nothing n st' eq')
    ... | just (too-high , st'') rewrite (singleton st st') = case-too-high n st' (st'' , eq')
    ... | just (too-low , st'') = suc n , case-<> n st (st' , st'' , eq , eq')

    thm-in-module : ∃[ query ] Maybe.map proj₁ (teacher.δ teacher.st₀ query) ≢ just too-low
          → ∃[ learner ] (∀ secret → learner learns secret from teacher within  rounds)
    thm-in-module (n , δ[n]≢too-low) with (teacher.δ teacher.st₀ n) in eq
    ... | just (too-low , _) = ⊥-elim (δ[n]≢too-low refl)
    ... | nothing = lucky-first-guess n , case-nothing n teacher.st₀ eq
    ... | just (too-high , st') =
        let
          m , learner-guesses-m = case-too-high n teacher.st₀ (st' , eq)
        in
        lucky-first-guess m , learner-guesses-m


-- -- for every teacher:
module theorems {ℓt} (teacher : NatTeacher ℓt) where
  -- Theorem: if there is a single query for which
  -- the teacher answers something different than 'too-low',
  -- then there is a learner that wins agains the teacher
  -- within 2 queries, no matter what the secret was.
  module teacher = NatTeacher teacher
  teacher-defeated-within-2-rounds :
    IsSingleton (NatTeacher.T teacher)
    → ∃[ query ] Maybe.map proj₁ (teacher.δ teacher.st₀ query) ≢ just too-low
    → ∃[ learner ] learner defeats teacher with-bound (λ secret → )
  teacher-defeated-within-2-rounds singl query = StatelessTeacher.thm-in-module teacher singl query

  learner-finds-every-secret :
    IsSingleton (NatTeacher.T teacher)
    → ∃[ query ] Maybe.map proj₁ (teacher.δ teacher.st₀ query) ≢ just too-low
    → ∃[ learner ] ∀ secret → learner learns secret from teacher within  rounds
  learner-finds-every-secret singl query = StatelessTeacher.thm-in-module teacher singl query