module non-regular where

open import Data.Nat
open import Data.Empty
open import Data.List
open import Data.Maybe hiding ( map )
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import logic
open import automaton
open import automaton-ex
open import finiteSetUtil
open import finiteSet
open import Relation.Nullary 
open import regular-language

open FiniteSet

inputnn :  List  In2 → Maybe (List In2)
inputnn [] = just []
inputnn  (i1 ∷ t) = just (i1 ∷ t)
inputnn  (i0 ∷ t) with inputnn t
... | nothing = nothing
... | just [] = nothing
... | just (i0 ∷ t1) = nothing   -- can't happen
... | just (i1 ∷ t1) = just t1   -- remove i1 from later part

inputnn1 :  List  In2 → Bool
inputnn1  s with inputnn  s 
... | nothing = false
... | just [] = true
... | just _ = false

t1 = inputnn1 ( i0 ∷ i1 ∷ [] )
t2 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )
t3 = inputnn1 ( i0 ∷ i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )

inputnn0 : ( n :  ℕ )  →  { Σ : Set  } → ( x y : Σ ) → List  Σ → List  Σ 
inputnn0 zero {_} _ _ s = s
inputnn0 (suc n) x y s = x  ∷ ( inputnn0 n x y ( y  ∷ s ) )

t4 : inputnn1 ( inputnn0 5 i0 i1 [] ) ≡ true
t4 = refl

t5 : ( n : ℕ ) → Set
t5 n = inputnn1 ( inputnn0 n i0 i1 [] ) ≡ true

--
--  if there is an automaton with n states , which accespt inputnn1, it has a trasition function.
--  The function is determinted by inputs,
--

open RegularLanguage
open Automaton

open _∧_

data Trace { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) : (is : List Σ) → ( List Q) → Set where
    tend  : {q : Q} → aend fa q ≡ true → Trace fa [] (q ∷ [])
    tnext : {q : Q} → {i : Σ} { is : List Σ} {qs : List Q} 
        → Trace fa is (δ fa q i  ∷ qs) → Trace fa (i ∷ is) ( q ∷ δ fa q i  ∷ qs ) 

tr-len :  { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → (qs : List Q) → Trace fa is (q ∷ qs) → ( length is ≡ length qs ) ∧ (suc (length is) ≡ length (trace fa q is ) )
tr-len {Q} {Σ} fa .[] q .[] (tend x) = ⟪ refl , refl ⟫
tr-len {Q} {Σ} fa (i ∷ is) q (q0 ∷ qs) (tnext t) = 
      ⟪ cong suc (proj1 (tr-len {Q} {Σ} fa is q0 qs t)) , cong suc (proj2 (tr-len {Q} {Σ} fa is q0 qs t)) ⟫

tr-accept→ : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q) → (qs : List Q) → Trace fa is (q ∷ qs) → accept fa q is ≡ true
tr-accept→ {Q} {Σ} fa [] q [] (tend x)  = x
tr-accept→ {Q} {Σ} fa (i ∷ is) q (x ∷ qs) (tnext tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) qs tr

tr-accept← : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is (trace fa q is)
tr-accept← {Q} {Σ} fa [] q ac = tend ac
tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext (tend ac )
tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext (tr-accept← fa (x1 ∷ is)  (δ fa q x)  ac) 

open Data.Maybe

-- head : {a : Set} → List a → Maybe a
-- head [] = nothing
-- head (h ∷ _ ) = just h

tr-append1 : { Q : Set } { Σ : Set  }
    → (fa : Automaton Q  Σ )
    → (i : Σ) → ( q : Q)  → (q0 : Q)
    → (is : List Σ)
    →  head (trace fa q is) ≡ just ( δ fa q0 i )
    → (tr : Trace fa is (trace fa q is) ) →  Trace fa (i ∷ is) (q0 ∷ (trace fa q is))
tr-append1 fa i q q0 is hd tr with trace fa q is
tr-append1 fa i q q0 is () tr | []
... | q₁ ∷ qs = tr01 hd where
      tr01 : just q₁ ≡ just (δ fa q0 i) → Trace fa (i ∷ is) (q0 ∷ q₁ ∷ qs)
      tr01 refl = tnext tr

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 

record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) {is : List Σ} { qs : List Q } (tr : Trace fa is qs) : Set where
    field
       x y z : List Σ
       qx qy qz : List Q
       non-nil-y : ¬ y ≡ []
       trace0 : Trace fa (x ++ y ++ z) (qx ++ qy ++ qz) 
       trace1 : Trace fa (x ++ y ++ y ++ z) (qx ++ qy ++ qy ++ qz) 
       trace-eq : trace0 ≅ tr

tr-append : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q )
     →  dup-in-list finq q qs ≡ true
     →  (tr : Trace fa is qs ) → TA fa tr
tr-append {Q} {Σ} fa finq q is qs dup tr = tra-phase1 qs is tr dup where
   open TA
   tra-phase3 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → {!!}
        → (qy : List Q) → (iy : List Σ)  → (ty : Trace fa iy qy ) → phase2 finq q qy ≡ true → {!!}
        → Trace fa (iy ++ is) (qy ++ qs)
   tra-phase3 = {!!}
   tra-phase2 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → phase2 finq q qs ≡ true
        → (qy : List Q) → (iy : List Σ)  → (ty : Trace fa iy qy ) → phase2 finq q qy ≡ true
        → TA fa tr
   tra-phase2 (q0 ∷ []) is (tend x₁) p qy iy ty py = {!!}
   tra-phase2 (q0 ∷ (q₁ ∷ qs)) (x ∷ is) (tnext tr) p qy iy ty py with equal? finq q q0
   ... | true = {!!}
   ... | false = {!!} where
       tr1 : TA fa tr
       tr1 = tra-phase2 (q₁ ∷ qs) is tr p qy iy ty py
   tra-phase1 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → phase1 finq q qs ≡ true  → TA fa tr
   tra-phase1 (q0 ∷ []) is (tend x₁) p = {!!}
   tra-phase1 (q0 ∷ (q₁ ∷ qs)) (i ∷ is) (tnext tr) p with equal? finq q q0
   ... | true = record { x = i ∷ x tr2 ; y = y tr2 ; z = z tr2
          ; qx = q0 ∷ qx tr2 ; qy = qy tr2 ;qz = qz  tr2
          ; trace0 = {!!}
          ; trace1 = {!!}
          ; non-nil-y = non-nil-y tr2 ; trace-eq = {!!} } where
       tr2 : TA fa tr
       tr2 = tra-phase2 (q₁ ∷ qs) is tr p (q₁ ∷ qs) is tr p
       -- tr3 : Trace fa (x tr2 ++ y tr2 ++ z tr2) (qx tr2 ++ qy tr2 ++ qz tr2) →  Trace fa ((i ∷ x tr2) ++ y tr2 ++ z tr2)  (q0 ∷ qx tr2 ++ qy tr2 ++ qz tr2)
       -- tr3 tr = tnext {!!}
   ... | false = {!!} where
       tr1 : TA fa tr
       tr1 = tra-phase1 (q₁ ∷ qs) is tr p

open RegularLanguage
open import Data.Nat.Properties
open import nat

lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2)  → isRegular inputnn1  s r ) 
lemmaNN r Rg = {!!} where
    n : ℕ
    n = suc (finite (afin r))
    nn =  inputnn0 n i0 i1 []
    nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
    nn01 zero = refl
    nn01 (suc i) with nn01 i
    ... | t = {!!}
    nn03 : accept (automaton r) (astart r) nn ≡ true
    nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n)
    count : In2 → List In2 → ℕ
    count _ [] = 0
    count i0 (i0 ∷ s) = suc (count i0 s)
    count i1 (i1 ∷ s) = suc (count i1 s)
    count x (_ ∷ s) = count x s
    nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
    nn10 = {!!}
    nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t
    nn11 = {!!}
    nntrace = trace (automaton r) (astart r) nn
    nn04 :  Trace (automaton r) nn nntrace
    nn04 = tr-accept← (automaton r) nn (astart r) nn03 
    nn07 : (n : ℕ) →  length (inputnn0 n i0 i1 []) ≡ n + n 
    nn07 n = subst (λ k → length (inputnn0 n i0 i1 []) ≡ k) (+-comm (n + n) _ ) (nn08 n [] )where
       nn08 : (n : ℕ) → (s : List In2) → length (inputnn0 n i0 i1 s) ≡ n + n + length s
       nn08 zero s = refl
       nn08 (suc n) s = begin
         length (inputnn0 (suc n) i0 i1 s) ≡⟨ refl ⟩
         suc (length (inputnn0 n i0 i1 (i1 ∷ s))) ≡⟨ cong suc (nn08 n (i1 ∷ s)) ⟩
         suc (n + n + suc (length s)) ≡⟨ +-assoc (suc n) n _  ⟩
         suc n + (n + suc (length s)) ≡⟨ cong (λ k → suc n + k) (sym (+-assoc n  _ _))  ⟩
         suc n + ((n + 1) + length s) ≡⟨ cong (λ k → suc n + (k + length s)) (+-comm n _) ⟩
         suc n + (suc n + length s) ≡⟨ sym (+-assoc (suc n)  _ _) ⟩
         suc n + suc n + length s  ∎  where open ≡-Reasoning
    nn09 : (n m : ℕ) → n ≤ n + m
    nn09 zero m = z≤n
    nn09 (suc n) m = s≤s (nn09 n m)
    nn05 : length nntrace > finite (afin r)
    nn05 = begin
         suc (finite (afin r))  ≤⟨ nn09 _ _ ⟩
         n + n   ≡⟨ sym (nn07 n) ⟩
         length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s  ⟩
         suc (length (inputnn0 (suc (finite (afin r))) i0 i1 [])) ≡⟨ proj2 (tr-len (automaton r) (inputnn0 n i0 i1 []) (astart r)
                  (trace (automaton r) (δ (automaton r) (astart r) i0) (inputnn0 (finite (afin r)) i0 i1 (i1 ∷ [])))
                  (tr-accept← (automaton r) _ _ nn03 )) ⟩
         length nntrace ∎  where open ≤-Reasoning
    nn02 : TA (automaton r) nn04
    nn02 = tr-append (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) nn04 where
        nn06 : Dup-in-list ( afin r) nntrace
        nn06 = dup-in-list>n (afin r) nntrace nn05
    nn12 : (x y z : List In2)
        → ¬ y ≡ []
        → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true →  ¬ (accept (automaton r) (astart r)  (x ++ y ++ y ++ z) ≡ true)
    nn12 x y z p q = {!!} where
         mono-color : List In2 → Bool
         mono-color [] = true
         mono-color (i0 ∷ s) = mono-color0 s where
              mono-color0 : List In2 → Bool
              mono-color0 [] = true
              mono-color0 (i1 ∷ s) = false
              mono-color0 (i0 ∷ s) = mono-color0 s
         mono-color (i1 ∷ s) = mono-color1 s where
              mono-color1 : List In2 → Bool
              mono-color1 [] = true
              mono-color1 (i0 ∷ s) = false
              mono-color1 (i1 ∷ s) = mono-color1 s
         mono-color (i1 ∷ s) = {!!}
         i1-i0? : List In2 → Bool
         i1-i0? [] = false
         i1-i0? (i1 ∷ []) = false
         i1-i0? (i0 ∷ []) = false
         i1-i0? (i1 ∷ i0 ∷ s) = true
         i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1)  
         nn13 : mono-color y ≡ true → count i0  (x ++ y ++ z) ≡  count i1 (x ++ y ++ z) → 
             ¬ ( count i0   (x ++ y ++ y ++ z) ≡  count i1  (x ++ y ++ y ++ z) )
         nn13 = {!!}
         nn16 :  (s : List In2 ) →  accept  (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
         nn16 = {!!}
         nn15 :  (s : List In2 ) → i1-i0? s ≡ true → accept  (automaton r) (astart r) s ≡ false
         nn15 = {!!}
         nn14 : mono-color y ≡ false → i1-i0? (x ++ y ++ y ++ z) ≡ true
         nn14 = {!!}
         nn17 : accept (automaton r) (astart r) (x ++ y ++ z) ≡ true →  ¬ (accept (automaton r) (astart r)  (x ++ y ++ y ++ z) ≡ true)
         nn17 p q with mono-color y | inspect mono-color y
         ... | true | record { eq = eq } = {!!}
         ... | false | record { eq = eq } = {!!} -- q ( nn15 (x ++ y ++ z) (nn14 eq))