{-# OPTIONS --allow-unsolved-metas #-} 
module automaton where
open import Level hiding ( suc ; zero )
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality -- hiding (_⇔_)
open import logic
open import Data.List 

record Automaton {n : Level} (Q : Set n) (Σ : Set ) : Set ((Level.suc n) ) where
  field
    δ : Q → Σ → Q
    F : Q → Set 

open Automaton

accept : {n  : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → Q → List Σ → Set 
accept {n} {Q} {Σ} atm q [] = F atm q
accept {n} {Q} {Σ} atm q (x ∷ input) = 
    accept atm (δ atm q x ) input

trace : {n  : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → accept A start input → List Q
trace {n} {Q} {Σ} A q [] a = q ∷ []
trace {n} {Q} {Σ} A q (x ∷ t) a = q ∷ ( trace A (δ A q x) t a )

data Q3 : Set where
  q₁ : Q3
  q₂ : Q3
  q₃ : Q3

data Σ2 : Set where
  s0 : Σ2
  s1 : Σ2

δ16 : Q3 → Σ2 → Q3
δ16 q₁ s0 = q₁
δ16 q₁ s1 = q₂
δ16 q₂ s0 = q₃
δ16 q₂ s1 = q₂
δ16 q₃ s0 = q₂
δ16 q₃ s1 = q₂

δ16' : Q3 → Σ2 → Q3
δ16' q₁ s0 = q₁
δ16' q₁ s1 = q₂
δ16' q₂ s0 = q₃
δ16' q₂ s1 = q₂
δ16' q₃ s0 = q₂
δ16' q₃ s1 = q₃

data a16end : Q3 → Set where
   a16q2 : a16end q₂

data exists-in-Q3 (P : Q3 → Set) :  Set where
  qe1 :  P q₁ → exists-in-Q3 P
  qe2 :  P q₂ → exists-in-Q3 P
  qe3 :  P q₃ → exists-in-Q3 P

a16 : Automaton Q3 Σ2
a16 = record { δ = δ16 ; F = λ q → a16end q }

a16' : Automaton Q3 Σ2
a16' = record { δ = δ16' ; F = λ q → q ≡ q₂ }

--
--  ∷  →   ∷ →   ∷ →  []
--  ↓     ↓      ↓
--  s0    s0     s1
--
input1 : List Σ2
input1 = s0 ∷ s0 ∷ s1 ∷ []

input2 : List Σ2
input2 = s0 ∷ s0 ∷ s0 ∷ []

test1 : accept a16 q₁ input1 
test1 =  a16q2 

lemma0 : accept a16 q₁ input1 ≡ a16end q₂
lemma0 = begin
       accept a16 q₁  ( s0 ∷ s0 ∷ s1 ∷ [] )
    ≡⟨ refl  ⟩  --   x ≡ x
       accept a16 q₁  ( s0 ∷ s1 ∷ [] )
    ≡⟨⟩
       accept a16 q₁  ( s1 ∷ [] )
    ≡⟨⟩
       accept a16 q₂ []
    ≡⟨⟩
       a16end q₂
    ∎ where open ≡-Reasoning

lemma1 : List Q3
lemma1 = trace a16 q₁ input1 a16q2

test1' : accept a16' q₁ input1 
test1' = refl

lemma2 : List Q3
lemma2 = trace a16' q₁ input1 refl

test2 : ¬ ( accept a16 q₁ input2 )
test2 ()

open import Data.Bool
open import Data.Unit

-- contains at least 1 s1
c1 : List Σ2 → Set
c1 [] = ⊥
c1 (s1 ∷ t) = ⊤
c1 (_ ∷ t) = c1 t 

-- even number of s0
even0 : List Σ2 → Set
odd0 : List Σ2 → Set
odd0 [] = ⊥
odd0 (s0 ∷ t) = even0 t
odd0 (s1 ∷ t) = odd0 t
even0 [] = ⊤
even0 (s0 ∷ t) = odd0 t
even0 (s1 ∷ t) = even0 t

-- after

a0 : List Σ2 → Set
a0 [] = ⊥
a0 (s1 ∷ t ) = even0 t
a0 (s0 ∷ t ) = a0 t

-- data ⊥ : Set 
--
-- data ⊤ : Set where
--    tt : ⊤
--    tt : ⊤

lemma-a :  (x : List Σ2 ) →  accept a16' q₁ x → a0 x
lemma-a x a = a1 x a where
   a3 : (x : List Σ2 ) → accept a16' q₃ x →  odd0 x
   a2 : (x : List Σ2 ) → accept a16' q₂ x →  even0 x
   a3 [] ()
   a3 (s0 ∷ t) a = a2 t a
   a3 (s1 ∷ t) a = a3 t a
   a2 [] a = tt
   a2 (s0 ∷ t) a = a3 t a
   a2 (s1 ∷ t) a = a2 t a
   a1 : (x : List Σ2 ) →  accept a16' q₁ x → a0 x
   a1 [] ()    -- a16' does not accept []
   a1 (s0 ∷ t) a = a1 t a
   a1 (s1 ∷ t) a = a2 t a

-- ¬_ :  Set → Set
-- ¬_ _ =  ⊥

lemma-not-a : ¬ (  (x : List Σ2 ) →  accept a16 q₁ x → a0 x )
lemma-not-a not1 with not1 (s1 ∷ s0 ∷ s1 ∷ [] ) a16q2
... | ()

-- can we prove negation similar to the lemma-a?
-- lemma-not-a' :  ¬ ((x : List Σ2 ) →  accept a16 q₁ x → a0 x)
-- lemma-not-a' not = {!!} where
--    a3 : (x : List Σ2 ) → accept a16 q₃ x →  odd0 x
--    a2 : (x : List Σ2 ) → accept a16 q₂ x →  even0 x
--    a3 (s0 ∷ t) a = a2 t a
--    a3 (s1 ∷ t) a = {!!}
--    a2 [] a = tt
--    a2 (s0 ∷ t) a = a3 t a
--    a2 (s1 ∷ t) a = a2 t a
--    a1 : (x : List Σ2 ) →  accept a16 q₁ x → a0 x
--    a1 [] ()
--    a1 (s0 ∷ t) a = a1 t a
--    a1 (s1 ∷ t) a = a2 t a

open import Data.Nat

evenℕ : ℕ → Set
oddℕ : ℕ → Set
oddℕ zero = ⊥
oddℕ (suc n) = evenℕ n
evenℕ zero = ⊤
evenℕ (suc n) = oddℕ n

count-s0 : (x : List Σ2 ) → ℕ
count-s0 [] = zero
count-s0 (s0 ∷ t) = suc ( count-s0 t )
count-s0 (s1 ∷ t) = count-s0 t 

e1 : (x : List Σ2 ) → even0 x → evenℕ ( count-s0 x )
o1 : (x : List Σ2 ) → odd0 x → oddℕ ( count-s0 x )
e1 [] e = tt
e1 (s0 ∷ t) o = o1 t o
e1 (s1 ∷ t) e = e1 t e
o1 [] () 
o1 (s0 ∷ t) e = e1 t e
o1 (s1 ∷ t) o = o1 t o

δ19 : Q3 → Σ2 → Q3
δ19 q₁ s0 = q₁
δ19 q₁ s1 = q₂
δ19 q₂ s0 = q₁
δ19 q₂ s1 = q₂
δ19 q₃ _ = q₁

a19 : Automaton Q3 Σ2
a19 = record { δ = δ19 ; F = λ q → q ≡ q₁ }

--  input is empty or ends in s0

end0 : List Σ2 → Set
end0 [] = ⊤
end0 (s0 ∷ [] )  =  ⊤
end0 (s1 ∷ [] )  =  ⊥
end0 (x ∷ t )  =  end0 t

lemma-b :  (x : List Σ2 ) →  accept a19 q₁ x → end0 x
lemma-b = {!!}