# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1641203401 -32400
# Node ID 16e47a3c4eda79fea1b12612f773630aa87b8903
# Parent  fd07e3205cea4ae17e51e7dbc0c662736d60d454
...

diff -r fd07e3205cea -r 16e47a3c4eda automaton-in-agda/src/fin.agda
--- a/automaton-in-agda/src/fin.agda	Mon Jan 03 11:41:58 2022 +0900
+++ b/automaton-in-agda/src/fin.agda	Mon Jan 03 18:50:01 2022 +0900
@@ -132,6 +132,19 @@
 open import Data.List
 open import Relation.Binary.Definitions
 
+-- fin-count : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → ℕ
+-- fin-count q p[ = 0
+-- fin-count q (q0 ∷ qs ) with <-fcmp q q0 
+-- ... | tri-e = suc (fin-count q qs)
+-- ... | false = fin-count q qs
+
+-- fin-not-dup-in-list : { n : ℕ}  (qs : List (Fin n) ) → Set
+-- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1
+
+-- this is far easier
+-- fin-not-dup-in-list→len<n : { n : ℕ}  (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n
+-- fin-not-dup-in-list→len<n = ?
+
 fin-phase2 : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → Bool
 fin-phase2 q [] = false
 fin-phase2 q (x ∷ qs) with <-fcmp q x
diff -r fd07e3205cea -r 16e47a3c4eda automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Mon Jan 03 11:41:58 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Mon Jan 03 18:50:01 2022 +0900
@@ -115,7 +115,7 @@
        q=qd : QDSEQ finq qd z trace-yz
 
 --
--- using accept ≡ true may simplify the make-TA
+-- using accept ≡ true may simplify the pumping-lemma
 -- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧  ...
 --
 -- like this ...
@@ -136,11 +136,11 @@
        trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
        non-nil-y : ¬ (y ≡ [])
 
-make-TA : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 
+pumping-lemma : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 
      → (tr : Trace fa is q )
      → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
      → TA fa q is
-make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
+pumping-lemma {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
    open TA
    tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q )
        → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is
@@ -194,7 +194,8 @@
 open import nat
 
 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2)  → isRegular inputnn1  s r ) 
-lemmaNN r Rg = {!!} where
+lemmaNN r Rg = tann {TA.x TAnn} (TA.non-nil-y 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 i0 i1 []
@@ -237,7 +238,7 @@
     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 = make-TA (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06)
+    TAnn = pumping-lemma (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06)
     count : In2 → List In2 → ℕ
     count _ [] = 0
     count i0 (i0 ∷ s) = suc (count i0 s)
@@ -250,7 +251,10 @@
     nn11 {i1} (i0 ∷ s) t = nn11 s t 
     nn11 {i1} (i1 ∷ s) t = cong suc ( nn11 s t )
     nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
-    nn10 = {!!}
+    nn10 s p = nn101 s (subst (λ k → k ≡ true) (sym (Rg s)) p ) where
+        nn101 : (s : List In2) → inputnn1 s ≡ true →  count i0 s ≡ count i1 s
+        nn101 [] p = refl
+        nn101 (x ∷ s) p = {!!}
     i1-i0? : List In2 → Bool
     i1-i0? [] = false
     i1-i0? (i1 ∷ []) = false
@@ -279,8 +283,10 @@
     not-mono = {!!}
     mono-count : { s : List In2 } → mono-color s ≡ true   → (length s ≡ count i0 s) ∨ ( length s ≡ count i1 s)
     mono-count = {!!}
-    tann : {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 )
-    tann {x} {y} {z} ny axyz axyyz with mono-color y
+    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 with mono-color y
     ... | true = {!!}
     ... | false = {!!}