module sbconst2 where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.Fin
open import Data.List

open import automaton
open import nfa
open import logic
open NAutomaton
open Automaton
open import finiteSet
open FiniteSet
open import  Relation.Binary.PropositionalEquality hiding ( [_] )


open Bool

δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r /\ nδ r i q )

open FiniteSet

subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
    (NAutomaton Q  Σ ) → (astart : Q ) → (Automaton (Q → Bool)  Σ )  
subset-construction {Q} { Σ} {n} fin NFA astart = record {
        δ = λ q x → δconv fin ( Nδ NFA ) q x
     ;  aend = λ f → exists fin ( λ q → f q /\ Nend NFA q )
   } 

am2start = λ q1 → equal? finState1 ss q1

test4 = subset-construction finState1 am2 ss

test5 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i0  ∷ i1  ∷ i0  ∷ [] )
test6 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i1  ∷ i1  ∷ i1  ∷ [] )

subset-construction-lemma→ : { Q : Set } { Σ : Set  } { n  : ℕ }  → (fin : FiniteSet Q {n} ) →  
    (NFA : NAutomaton Q  Σ ) → (astart : Q )
    → (x : List Σ)
    → Naccept NFA fin ( λ q1 → equal? fin  astart q1) x ≡ true
    → accept (  subset-construction fin NFA astart ) ( λ q1 → equal? fin  astart q1) x ≡ true
subset-construction-lemma→ {Q} {Σ} {n} fin NFA astart x naccept = lemma1 x ( λ q1 → equal? fin  astart q1) naccept where
    lemma1 :  (x : List Σ) → ( states : Q → Bool )
       → Naccept NFA fin states x ≡ true
       → accept (  subset-construction fin NFA astart ) states x ≡ true
    lemma1 [] states naccept = naccept
    lemma1 (h ∷ t ) states naccept = lemma1 t (δconv fin (Nδ NFA) states h) naccept

subset-construction-lemma← : { Q : Set } { Σ : Set  } { n  : ℕ }  → (fin : FiniteSet Q {n} ) →  
    (NFA : NAutomaton Q  Σ ) → (astart : Q )
    → (x : List Σ)
    → accept (  subset-construction fin NFA astart ) ( λ q1 → equal? fin  astart q1) x ≡ true
    → Naccept NFA fin ( λ q1 → equal? fin  astart q1) x ≡ true
subset-construction-lemma← {Q} {Σ} {n} fin NFA astart x saccept = lemma2 x ( λ q1 → equal? fin  astart q1) saccept where
    lemma2 :  (x : List Σ) → ( states : Q → Bool )
       → accept (  subset-construction fin NFA astart ) states x ≡ true
       → Naccept NFA fin states x ≡ true
    lemma2 [] states saccept = saccept
    lemma2 (h ∷ t ) states saccept = lemma2 t (δconv fin (Nδ NFA) states h) saccept