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 import nat
open import pumping


open FiniteSet

list-eq :  List  In2 → List  In2 → Bool
list-eq [] [] = true
list-eq [] (x ∷ s1) = false
list-eq (x ∷ s) [] = false
list-eq (i0 ∷ s) (i0 ∷ s1) = false
list-eq (i0 ∷ s) (i1 ∷ s1) = false
list-eq (i1 ∷ s) (i0 ∷ s1) = false
list-eq (i1 ∷ s) (i1 ∷ s1) = list-eq s s1 

input-addi0 : ( n :  ℕ )  → List In2 →  List  In2 
input-addi0 zero x = x
input-addi0 (suc i) x = i0 ∷ input-addi0 i x

input-addi1 : ( n :  ℕ )  →  List  In2 
input-addi1 zero = []
input-addi1 (suc i) = i1 ∷ input-addi1 i

inputnn0 : ( n :  ℕ )  →  List  In2 
inputnn0 n = input-addi0 n (input-addi1 n)

inputnn1-i1 : (i : ℕ) → List In2 → Bool
inputnn1-i1 zero [] = true
inputnn1-i1 (suc _) [] = false
inputnn1-i1 zero (i1 ∷ x)  = false
inputnn1-i1 (suc i) (i1 ∷ x)  = inputnn1-i1 i x
inputnn1-i1 zero (i0 ∷ x)  = false
inputnn1-i1 (suc _) (i0 ∷ x)  = false

inputnn1-i0 : (i : ℕ) → List In2 → ℕ ∧ List In2
inputnn1-i0 i [] = ⟪ i , [] ⟫
inputnn1-i0 i (i1 ∷ x)  = ⟪ i , (i1 ∷ x)  ⟫
inputnn1-i0 i (i0 ∷ x)  = inputnn1-i0 (suc i) x  

open _∧_

inputnn1 : List In2 → Bool
inputnn1 x = inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x))

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

t4 : inputnn1 ( inputnn0 5  )  ≡ true
t4 = refl

t5 : ( n : ℕ ) → Set
t5 n = inputnn1 ( inputnn0 n  )  ≡ true

cons-inject : {A : Set} {x1 x2 : List A } { a : A } → a ∷ x1 ≡ a ∷ x2 → x1 ≡ x2
cons-inject refl = refl

append-[] : {A : Set} {x1 : List A } → x1 ++ [] ≡ x1
append-[] {A} {[]} = refl
append-[] {A} {x ∷ x1} = cong (λ k → x ∷ k) (append-[] {A} {x1} )

open import Data.Nat.Properties
open import  Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality

nn01  : (i : ℕ) → inputnn1 ( inputnn0 i  ) ≡ true
nn01  i = subst₂ (λ j k → inputnn1-i1 j k ≡ true) (sym (nn07 i 0 refl)) (sym (nn09 i)) (nn04 i)  where
     nn07 : (j x : ℕ) → x + j ≡ i  → proj1 ( inputnn1-i0 x (input-addi0 j (input-addi1 i))) ≡ x + j
     nn07 zero x eq with input-addi1 i | inspect input-addi1 i
     ... | [] | _ = +-comm 0 _
     ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where
          nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t )
          nn08 zero ()
          nn08 (suc i) ()
     ... | i1 ∷ t | _ = +-comm 0 _
     nn07 (suc j) x eq = trans (nn07 j (suc x) (trans (cong (λ k → k + j) (+-comm 1 _ )) (trans (+-assoc x _ _) eq)) ) 
                                               (trans (+-assoc 1 x _) (trans (cong (λ k → k + j) (+-comm 1 _) ) (+-assoc x 1 _) ))
     nn09 : (x : ℕ) → proj2 ( inputnn1-i0 0 (input-addi0 x (input-addi1 i))) ≡ input-addi1 i
     nn09 zero with input-addi1 i | inspect input-addi1 i
     ... | [] | _ = refl
     ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where
          nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t )
          nn08 zero ()
          nn08 (suc i) ()
     ... | i1 ∷ t | _ = refl
     nn09 (suc j) = trans (nn10 (input-addi0 j (input-addi1 i)) 0) (nn09 j ) where
         nn10 : (y : List In2) → (j : ℕ) → proj2 (inputnn1-i0 (suc j) y) ≡ proj2 (inputnn1-i0 j y )
         nn10 [] _ = refl
         nn10 (i0 ∷ y) j = nn10 y (suc j)
         nn10 (i1 ∷ y) _ = refl
     nn04 : (i : ℕ) → inputnn1-i1 i (input-addi1 i) ≡ true
     nn04 zero = refl
     nn04 (suc i) = nn04 i

--
--  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 _∧_


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

lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2)  → isRegular inputnn1  s r ) 
lemmaNN r Rg = tann {TA.x TAnn} (TA.non-nil-y TAnn ) (TA.xyz=is TAnn) (tr-accept→ (automaton r) _  (astart r) (TA.trace-xyz TAnn) )
       (tr-accept→ (automaton r) _  (astart r) (TA.trace-xyyz TAnn) ) where
    n : ℕ
    n = suc (finite (afin r))
    nn =  inputnn0 n 
    nn03 : accept (automaton r) (astart r) nn ≡ true
    nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n)
    nn09 : (n m : ℕ) → n ≤ n + m
    nn09 zero m = z≤n
    nn09 (suc n) m = s≤s (nn09 n m)
    nn04 :  Trace (automaton r) nn (astart r)
    nn04 = tr-accept← (automaton r) nn (astart r) nn03 
    nntrace = tr→qs (automaton r) nn (astart r) nn04
    nn07 : (n : ℕ) →  length (inputnn0 n  ) ≡ n + n 
    nn07 i = nn19 i where
        nn17 : (i : ℕ) → length (input-addi1 i) ≡ i
        nn17 zero = refl
        nn17 (suc i)= cong suc (nn17 i)
        nn18 : (i j : ℕ) →  length (input-addi0 j (input-addi1 i)) ≡ j +  length (input-addi1 i )
        nn18 i zero = refl
        nn18 i (suc j)= cong suc (nn18 i j)
        nn19 : (i : ℕ) → length (input-addi0 i ( input-addi1 i )) ≡ i + i
        nn19 i = begin
            length (input-addi0 i ( input-addi1 i )) ≡⟨ nn18 i i ⟩
            i + length (input-addi1 i)  ≡⟨ cong (λ k → i + k) ( nn17 i) ⟩
            i + i  ∎ where open ≡-Reasoning 
    nn05 : length nntrace > finite (afin r)
    nn05 = begin
         suc (finite (afin r))  ≤⟨ nn09 _ _ ⟩
         n + n   ≡⟨ sym (nn07 n) ⟩
         length (inputnn0 n  ) ≡⟨ tr→qs=is (automaton r) (inputnn0 n  ) (astart r) nn04 ⟩
         length nntrace ∎  where open ≤-Reasoning
    nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04)
    nn06 = dup-in-list>n (afin r) nntrace nn05

    TAnn : TA (automaton r) (astart r) nn
    TAnn = pumping-lemma (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06)

    open import Tactic.MonoidSolver using (solve; solve-macro)

    tann : {x y z : List In2} → ¬ y ≡ []
       → x ++ y ++ z ≡ nn
       → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z)  ≡ true )
    tann {x} {y} {z} ny eq axyz axyyz = ¬-bool (nn10 x y z (trans (Rg (x ++ y ++ z)) axyz ) ) (trans (Rg (x ++ y ++ y ++ z)) axyyz ) where
          count0 : (x : List In2) → ℕ
          count0 [] = 0
          count0 (i0 ∷ x) = suc (count0 x)
          count0 (i1 ∷ x) = count0 x
          count1 : (x : List In2) → ℕ
          count1 [] = 0
          count1 (i1 ∷ x) = suc (count1 x)
          count1 (i0 ∷ x) = count1 x
          nn15 : (x : List In2 ) → inputnn1 z ≡ true → count0 z ≡ count1 z
          nn15 = ?
          cong0 : (x y : List In2 ) → count0 (x ++ y ) ≡ count0 x + count0 y
          cong0 [] y = refl
          cong0 (i0 ∷ x)  y = cong suc (cong0 x y)
          cong0 (i1 ∷ x)  y = cong0 x y
          cong1 : (x y : List In2 ) → count1 (x ++ y ) ≡ count1 x + count1 y
          cong1 [] y = refl
          cong1 (i1 ∷ x)  y = cong suc (cong1 x y)
          cong1 (i0 ∷ x)  y = cong1 x y
          record i1i0 (z : List In2) : Set where
             field
                a b : List In2
                i10 : z ≡ a ++ (i1 ∷ i0 ∷ b )
          nn12 : (z : List In2 ) → inputnn1 z ≡ true → ¬ i1i0 z
          nn12 = ?
          nn11 : (x y z : List In2 ) → inputnn1  (x ++ y ++ z) ≡ true → ¬ ( inputnn1  (x ++ y ++ y ++ z) ≡ true )
          nn11 x y z xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) ; b = i1i0.b (bb23 bb22) ++ y ; i10 = bb24 } )  where
               nn21 : count0 x + count0 y + count0 y + count0 z ≡ count1 x + count1 y + count1 y + count1 z
               nn21 = begin
                    (count0 x + count0 y + count0 y) + count0 z ≡⟨ solve +-0-monoid ⟩
                    count0 x + (count0 y + (count0 y + count0 z))  ≡⟨ sym (cong (λ k → count0 x + (count0 y + k)) (cong0  y _ )) ⟩
                    count0 x + (count0 y + count0 (y ++ z))  ≡⟨ sym (cong (λ k → count0 x + k) (cong0  y _ )) ⟩
                    count0 x + (count0 (y ++ y ++ z))  ≡⟨ sym (cong0  x _ ) ⟩
                    count0 (x ++ y ++ y ++ z) ≡⟨ ? ⟩
                    count1 (x ++ y ++ y ++ z) ≡⟨ ? ⟩
                    count1 x + count1 y + count1 y + count1 z ∎ where open ≡-Reasoning
               nn20 : count0 x + count0 y + count0 z ≡ count1 x + count1 y + count1 z
               nn20 = ?
               bb22 : count0 y ≡ count1 y
               bb22 = ?
               bb23 : count0 y ≡ count1 y → i1i0 (y ++ y)
               bb23 = ? 
               bb24 : x ++ y ++ y ++ z ≡ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ y
               bb24 = begin
                    x ++ y ++ y ++ z ≡⟨ ? ⟩
                    (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ y where open ≡

          nn10 : (x y z : List In2 ) → inputnn1  (x ++ y ++ z) ≡ true → inputnn1  (x ++ y ++ y ++ z) ≡ false
          nn10 x y z eq with inputnn1  (x ++ y ++ y ++ z)  | inspect inputnn1  (x ++ y ++ y ++ z)  
          ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z eq eq1 )
          ... | false | _ = refl