{-# OPTIONS --safe  #-}

-- -- No polynomial time bound for learners -----------------------------------
-- If the teacher only answers with yes/no on equivalence queries,
-- then learning is not possible in polynomial time.
-- ----------------------------------------------------------------------------

open import Level hiding (_⊔_)
import DFA as D
open import Data.Bool hiding (_<_; _≤_)
open import Data.Nat as ℕ
open import Data.Sum
open import Data.Fin using (Fin; fromℕ)
import Data.Fin as Fin
open import Data.Empty
open import Data.List
open import Data.Unit
open import Data.Maybe using (Maybe; just)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Unary.Any
open import Relation.Nullary.Decidable
import Data.Vec as V
import Data.Vec.Properties as V
open import Data.Vec using (Vec)
import Data.Nat.Properties as ℕ
open import Data.Product
open import Function.Base
open import Data.Nat.Logarithm
open import Relation.Binary.PropositionalEquality
open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; module CastReasoning)
open import Relation.Nullary.Negation.Core using (contraposition)
open import Utils
open import Auxiliary-Definitions
open import Finite

module DFA-Examples.DFA-Restricted-Bound (k : ℕ)  where
-- we work with an input alphabet of size k and require
-- that there are at least two input letters.

private
  A : Set 0ℓ
  A = Fin k

open import DFA A
open import DFA-Restricted-Learning A
open import Game-Definitions DFA F
open import Fin-Pigeonhole-Principle
open import DFA-Examples.Password-DFA k

open import Polynomial-vs-Exponential-Growth

-- decision procedures for finite types:
dec-Fin : ∀ {k} {P Q : Fin k → Set} → (f : ∀ i → P i ⊎ Q i) → ∃[ i ] (P i) ⊎ ∀ i → Q i
dec-Fin {ℕ.zero} f = inj₂ λ ()
dec-Fin {ℕ.suc k} f with (f Fin.zero)
... | inj₁ P0 = inj₁ (Fin.zero , P0)
... | inj₂ Q0 with (dec-Fin (λ i → f (Fin.suc i)))
...         | inj₁ (i , fi≡true) = inj₁ ((Fin.suc i) , fi≡true)
...         | inj₂ (all-i-≡false) = inj₂ λ
                   { Fin.zero → Q0
                   ; (Fin.suc i) → all-i-≡false i
                   }

-- Given a decidable predicate f on vectors of length n,
-- then this predicate holds for at least one vector w or fails
-- for all vectors of length n.
dec-Vec : ∀ n → (f : Vec A n → Bool) → ∃[ w ] f w ≡ true ⊎ ∀ w → f w ≡ false
dec-Vec ℕ.zero f with (f V.[]) in eq
... | true = inj₁ (V.[] , eq)
... | false = inj₂ λ { V.[] → eq }
dec-Vec (ℕ.suc n) f = case res of λ
  { (inj₁ (hd , tl , eq)) → inj₁ ((hd V.∷ tl) , eq)
  ; (inj₂ all-false) → inj₂ (λ { (hd V.∷ tl) → all-false hd tl })
  }
  where
    g : (i : Fin k) → (∃[ tl ] f (i V.∷ tl) ≡ true) ⊎ ∀ tl → f (i V.∷ tl) ≡ false
    g hd = dec-Vec n λ tl → f(hd V.∷ tl)
    res : ∃[ hd ] ∃[ tl ] f (hd V.∷ tl) ≡ true ⊎ ∀ hd tl → f (hd V.∷ tl) ≡ false
    res = dec-Fin g


record AT (n : ℕ) : Set where
  -- an adversarial teacher who keeps track of
  -- words of length n.
  constructor adv-teacher
  field
    words : List (V.Vec A n)

  len : ℕ
  len = length words

≢-cotrans : ∀ {b b' : Bool} → b ≡ false → b' ≡ true → b ≢ b'
≢-cotrans refl refl ()


module for-length (n : ℕ) where
  open AT

  -- teacher-correct : ∀ {ℓr : Level} {R : Set ℓr} {ℓ : Level} {X : Set ℓ} →
  mem-query : (st : AT n) → List A → Bool × AT n
  mem-query st w with (length w ℕ.≟ n)
  ... | yes refl  = false , adv-teacher (V.fromList w ∷ st .words)
  ... | no _  = false , adv-teacher (st .words)
  equiv-query : AT n → DFA → Maybe (AT n)
  equiv-query st dfa with dec-Vec n (λ w → ⟦DFA dfa ⟧ (V.toList w))
        -- if there is some word of length n accepted by the DFA
        -- then save it in our list
  ... | inj₁ (w , _) = just (adv-teacher (w ∷ st .words))
  ... | inj₂ _ = just st
  teacher : DFATeacher 0ℓ
  teacher = record
    { T = AT n
    ; st₀ = record
      { words = []
      }
    ; answer-member = mem-query
    ; answer-equiv = equiv-query
    }
  teacher-nat : Teacherδ (AT n)
  teacher-nat = Teacher.δ (DFATeacher⇒Teacher teacher)

  module with-learner {ℓr : Level} {R : Set ℓr} {ℓc : Level} {C : Set ℓc} (c : Learnerδ R C) where
    open Game DFALearning-Semantics teacher-nat c
    len[∷]<k^n : ∀ r (ℓ : List (Vec A n)) → ( + r) + length ℓ < k ^ n
                                          → r + ( + length ℓ) < k ^ n
    len[∷]<k^n r ℓ ineq =
                    (begin
                    ℕ.suc (r + ( + length (ℓ))) ≡⟨ cong ℕ.suc (ℕ.+-suc r _) ⟩
                    ℕ.suc (( + r) + length (ℓ)) ≤⟨ ineq ⟩
                    k ^ n
                    ∎)
                    where open ℕ.≤-Reasoning

    -- the lower bound: if a teacher has answered 'len' many queries already,
    -- then the teacher can defined for another r rounds if r + len < k ^ n
    game-lower-bound : ∀ r (t : AT n) (q : C)
                       → r + AT.len t < k ^ n
                       → Σ[ w ∈ Vec A n ] w ∉ AT.words t × still-possible (t , q) r (password-dfa w) 
    game-lower-bound ℕ.zero t q len[t]<k^n = w , w∉t , tt
      where
        w : Vec A n
        w = proj₁ (find-missing (AT.words t) len[t]<k^n)
        dfa[w] : DFA
        dfa[w] = password-dfa w
        w∉t : w ∉ (AT.words t)
        w∉t = proj₂ (find-missing (AT.words t) len[t]<k^n)
    game-lower-bound (ℕ.suc r) t q 1+r+t<k^n with (c q)
    ... | membership v next with (length v ℕ.≟ n)
    ...     | (no neq-len) =
              let
                w , w∉t , still-poss = game-lower-bound r t (next false) (ℕ.≤-<-trans (ℕ.m≤n+m _ ) 1+r+t<k^n)
              in
              w , w∉t , password-dfa-rejects-other-lengths w v neq-len , still-poss
    ...     | (yes refl) =
              w , (λ w∈t → w∉v∷t (there w∈t))
                , password-dfa-rejects-everything-else w v w≢v
                , proj₂ (proj₂ IH)
              where
                t' = (adv-teacher (V.fromList v ∷ t .words))
                q' = next false
                opaque
                  IH : Σ[ w ∈ Vec A n ] w ∉ AT.words t' × still-possible (t' , q') r (password-dfa w)
                  IH = game-lower-bound r t' q' (len[∷]<k^n r (t .words) 1+r+t<k^n)

                w : Vec A n
                w = proj₁ IH
                w∉v∷t = proj₁ (proj₂ IH)
                w≢v : (V.toList w ≡ v) → ⊥
                w≢v toList[w]≡v = w∉v∷t (here (begin
                  w ≡⟨ V.fromList∘toList w ⟨
                  V.cast (V.length-toList w) (V.fromList (V.toList w))
                    ≡⟨ V.cast-fromList toList[w]≡v ⟩
                  V.fromList v
                  ∎))
                  where open ≡-Reasoning
    game-lower-bound (ℕ.suc r) t q 1+r+t<k^n | equivalence hyp ret q'
                     with dec-Vec n (λ w → ⟦DFA hyp ⟧ (V.toList w))
    ... | (inj₁ (v , v∈L[hyp])) =
          -- if the hypothesis accepts a word v of length n,
          -- then v distinguishes the hypothesis from our password dfa:
          w , ((λ w∈t → w∉v∷t (there w∈t))
            , (V.toList v , ≢-cotrans v∉L[pwdfa] v∈L[hyp]) , proj₂ (proj₂ IH))
          where
            t' = (adv-teacher (v ∷ t .words))
            opaque
              IH : Σ[ w ∈ Vec A n ] w ∉ AT.words t' × still-possible (t' , q') r (password-dfa w)
              IH = game-lower-bound r t' q' (len[∷]<k^n r (t .words) 1+r+t<k^n)
            w : Vec A n
            w = proj₁ IH
            w∉v∷t = proj₁ (proj₂ IH)
            w≢v : w ≢ v
            w≢v w≡v = w∉v∷t (here w≡v)
            toList[w]≢toList[v] : V.toList w ≢ V.toList v
            toList[w]≢toList[v] toL[w]≡toL[v] = w≢v (begin
              w ≡⟨ V.toList-injective refl v w (sym toL[w]≡toL[v]) ⟨
              V.cast refl v ≡⟨ V.cast-is-id refl v ⟩
              v
              ∎)
              where open ≡-Reasoning

            v∉L[pwdfa] : ⟦DFA password-dfa w ⟧ (V.toList v) ≡ false
            v∉L[pwdfa] =
              password-dfa-rejects-everything-else w (V.toList v) toList[w]≢toList[v]
    ... | (inj₂ ∀v→v∉L[hyp]) =
          -- if the hypothesis rejects any word of length n
          -- then w is the distinguishing word
          w , w∉t
            , (V.toList w , ≢-sym (≢-cotrans (∀v→v∉L[hyp] w) (password-dfa-accepts-w w)))
            , proj₂ (proj₂ IH)
          where
            t' = adv-teacher (t .words)
            opaque
              IH : Σ[ w ∈ Vec A n ] w ∉ AT.words t' × still-possible (t' , q') r (password-dfa w)
              IH = game-lower-bound r t' q' (ℕ.≤-<-trans (ℕ.m≤n+m _ ) 1+r+t<k^n)
            w : Vec A n
            w = proj₁ IH
            w∉t = proj₁ (proj₂ IH)
      

-- Main theorem:
--
-- originally proven in Section 2.3 of:
-- Dana Angluin. Queries and concept learning.
-- Mach. Learn., 2(4):319–342, 1987. doi: 10.1007/BF00116828.
--
-- Assume that there are at least two input symbols.
-- We show that for every polynomial P, there is a teacher
-- such that no learner can win the learning game with bound P.
-- Concretely: for every learner, there is some dfa (namely a password-dfa)
-- such that all answers by the teacher are consistent with this dfa.
--
-- The dfa has n + 2 states, where n is the length of the password
-- and any learner fails to learn the password dfa within P(n + 2)
-- queries.
thm-adversarial-teacher : k ≥  → ∀ {ℓc : Level} (P : Polynomial) →
   ∃[ teacher ] ∀ (learner : Learner ℓc)
    → ∃[ dfa ] learner can't-learn dfa from teacher within ⟦poly P ⟧[ DFA.states dfa ] rounds

thm-adversarial-teacher k≥2 P =
  teacher , λ learner →
    let w , _ , still-poss =
          with-learner.game-lower-bound
            (Learner.δ learner)
            P[  + n ]
            st₀
            (Learner.q₀ learner)
            P[2+n]<k^n
    in
    (password-dfa w) , still-poss
  where
    opaque
        bound : ∃[ n ] ⟦poly P ⟧[  + n ] < k ^ n
        bound = poly[2+n]<k^n k P k≥2
    n : ℕ
    n = proj₁ bound
    P[_] = ⟦poly P ⟧[_]
    P[2+n]<k^n : P[  + n ] +  < k ^ n
    P[2+n]<k^n = begin
      ℕ.suc (P[  + n ] + ) ≡⟨ cong ℕ.suc (ℕ.+-identityʳ _) ⟩
      ℕ.suc (P[  + n ]) ≤⟨ proj₂ bound ⟩
      k ^ n
      ∎
      where open ℕ.≤-Reasoning
    st₀ : AT n
    st₀ = adv-teacher []

    instance
      k-nonZero : NonZero k
      k-nonZero = >-nonZero (ℕ.≤-trans (s≤s z≤n) k≥2)

    0<k^n :  < k ^ n
    0<k^n = ℕ.m^n>0 k n
    open for-length n