Mercurial > hg > Members > kono > Proof > automaton

changeset 385:101080136450

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Jul 2023 21:20:16 +0900
parents a5c874396cc4
children 6ef927ac832c
files automaton-in-agda/src/derive.agda automaton-in-agda/src/non-regular.agda automaton-in-agda/src/pumping.agda
diffstat 3 files changed, 319 insertions(+), 196 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Wed Jul 26 09:36:00 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Wed Jul 26 21:20:16 2023 +0900
@@ -257,25 +257,14 @@
 sbempty? < x > f = false
 
 sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r → Bool
-sbderive r f s record { s = t ; is-sub = is-sub } with rg-eq? (derivative r s) t | f record { s = r ; is-sub = sunit  }
-... | yes _ | true = true
-... | no _ | true = false
-... | yes _ | false = false
-... | no _ | false = false
-
-ISB→Regex : (r : Regex Σ) →  (ISB r → Bool) → Regex Σ
-ISB→Regex ε f with f record { s = ε ; is-sub = sunit  }
-... | true = ε
-... | false = φ
-ISB→Regex φ f = φ
-ISB→Regex (r *) f =  ( ISB→Regex  r (λ i → f record { s = ISB.s i ; is-sub = sub* (ISB.is-sub i) } ) ) *
-ISB→Regex (x & y) f =   ISB→Regex  x (λ i → f record { s = ISB.s i ; is-sub = sub&1 x y _ (ISB.is-sub i) } )   
-                     || ISB→Regex  y (λ i → f record { s = ISB.s i ; is-sub = sub&2 x y _ (ISB.is-sub i) } )   
-ISB→Regex (x || y) f =  ISB→Regex  x (λ i → f record { s = ISB.s i ; is-sub = sub|1 (ISB.is-sub i) } )   
-                     || ISB→Regex  y (λ i → f record { s = ISB.s i ; is-sub = sub|2 (ISB.is-sub i) } )   
-ISB→Regex < x > f with f record { s = < x > ; is-sub = sunit  }
-... | true = < x >
-... | false = φ
+sbderive ε f s record { s = .ε ; is-sub = sunit } = ?
+sbderive φ f s record { s = t ; is-sub = is-sub } = false
+sbderive (r *) f s record { s = t ; is-sub = is-sub } = ?
+sbderive (r & r₁) f s record { s = t ; is-sub = is-sub } = ?
+sbderive (r || r₁) f s record { s = .(r || r₁) ; is-sub = sunit } = ?
+sbderive (r || r₁) f s record { s = t ; is-sub = (sub|1 is-sub) } = ?
+sbderive (r || r₁) f s record { s = t ; is-sub = (sub|2 is-sub) } = ?
+sbderive < x > f s record { s = t ; is-sub = is-sub } = ?
 
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
 --    this is not correct because it contains s || s || s || .....
--- a/automaton-in-agda/src/non-regular.agda	Wed Jul 26 09:36:00 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Wed Jul 26 21:20:16 2023 +0900
@@ -13,49 +13,99 @@
 open import Relation.Nullary 
 open import regular-language
 open import nat
+open import pumping
 
 
 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
+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
 
-inputnn1 :  List  In2 → Bool
-inputnn1  s with inputnn  s 
-... | nothing = false
-... | just [] = true
-... | just _ = false
+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 ∷ [] )
 
-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 : inputnn1 ( inputnn0 5  )  ≡ true
 t4 = refl
 
 t5 : ( n : ℕ ) → Set
-t5 n = inputnn1 ( inputnn0 n i0 i1 [] ) ≡ true
+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 i0 i1 [] ) ≡ true
-nn01 zero = refl
-nn01 (suc i) = {!!} where 
-      nn02 : (i : ℕ) → ( x : List In2) → inputnn ( inputnn0 i i0 i1 x ) ≡ inputnn x
-      nn02 zero _ = refl
-      nn02 (suc i) x with inputnn (inputnn0 (suc i) i0 i1 x)
-      ... | nothing = {!!}
-      ... | just []  = {!!}
-      ... | just (i0 ∷ t1)   = {!!}
-      ... | just (i1 ∷ t1)   = {!!}
+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,
@@ -66,138 +116,6 @@
 
 open _∧_
 
-data Trace { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) : (is : List Σ) → Q → Set where
-    tend  : {q : Q} → aend fa q ≡ true → Trace fa [] q
-    tnext : (q : Q) → {i : Σ} { is : List Σ} 
-        → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q 
-
-tr-len :  { Q : Set } { Σ : Set  }
-    → (fa : Automaton Q  Σ )
-    → (is : List Σ) → (q : Q) → Trace fa is q → suc (length is) ≡ length (trace fa q is ) 
-tr-len {Q} {Σ} fa .[] q (tend x) = refl 
-tr-len {Q} {Σ} fa (i ∷ is) q (tnext .q t) = cong suc (tr-len {Q} {Σ} fa is (δ fa q i) t)
-
-tr-accept→ : { Q : Set } { Σ : Set  }
-    → (fa : Automaton Q  Σ )
-    → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true
-tr-accept→ {Q} {Σ} fa [] q (tend x)  = x
-tr-accept→ {Q} {Σ} fa (i ∷ is) q  (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr
-
-tr-accept← : { Q : Set } { Σ : Set  }
-    → (fa : Automaton Q  Σ )
-    → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is q
-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) 
-
-tr→qs : { Q : Set } { Σ : Set  }
-    → (fa : Automaton Q  Σ )
-    → (is : List Σ) → (q : Q) → Trace fa is q → List Q
-tr→qs fa [] q (tend x) = []
-tr→qs fa (i ∷ is) q (tnext q tr) = q ∷ tr→qs fa is (δ fa q i) tr 
-
-tr→qs=is : { Q : Set } { Σ : Set  }
-    → (fa : Automaton Q  Σ )
-    → (is : List Σ) → (q : Q) → (tr : Trace fa is q ) → length is ≡  length (tr→qs fa is q tr)
-tr→qs=is fa .[] q (tend x) = refl
-tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is  (δ fa q i) tr)
-
-open Data.Maybe
-
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
-open import Relation.Binary.Definitions
-open import Data.Unit using (⊤ ; tt)
-open import Data.Nat.Properties
-
-data QDSEQ { Q : Set } { Σ : Set  } { fa : Automaton  Q  Σ} ( finq : FiniteSet Q) (qd : Q) (z1 :  List Σ) :
-       {q : Q} {y2 : List Σ} → Trace fa (y2 ++ z1) q → Set where
-   qd-nil :  (q : Q) → (tr : Trace fa z1 q) → equal? finq qd q ≡ true → QDSEQ finq qd z1 tr
-   qd-next : {i : Σ} (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) (δ fa q i)) → equal? finq qd q ≡ false
-       → QDSEQ finq qd z1 tr 
-       → QDSEQ finq qd z1 (tnext q tr)
-
-record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
-    field
-       y z : List Σ
-       yz=is : y ++ z ≡ is 
-       trace-z    : Trace fa z  qd
-       trace-yz   : Trace fa (y ++ z)  q
-       q=qd : QDSEQ finq qd z trace-yz
-
---
--- using accept ≡ true may simplify the pumping-lemma
--- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧  ...
---
--- like this ...
--- record TA2 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
---     field
---        y z : List Σ
---        yz=is : y ++ z ≡ is 
---        trace-z    : accpet fa z qd ≡ true
---        trace-yz   : accept fa (y ++ z)  q ≡ true
---        q=qd  : last (tr→qs fa q trace-yz) ≡ just qd 
---        ¬q=qd : non-last (tr→qs fa q trace-yz) ≡ just qd 
-
-record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
-    field
-       x y z : List Σ
-       xyz=is : x ++ y ++ z ≡ is 
-       trace-xyz  : Trace fa (x ++ y ++ z)  q
-       trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
-       non-nil-y : ¬ (y ≡ [])
-
-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
-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
-   tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
-   ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq
-        ; trace-z  = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr }
-   ... | false | record { eq = ne } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
-       ; q=qd = tra-08
-       ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
-            ta : TA1 fa finq (δ fa q i) qd is
-            ta = tra-phase2 (δ fa q i) is tr p 
-            tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i)
-            tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr
-            tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta))
-            tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p))  ne (TA1.q=qd ta)
-   tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa q is
-   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q
-   ... | true | record { eq = eq } = record { x = [] ; y = i ∷ TA1.y ta ;  z = TA1.z ta ; xyz=is =  cong (i ∷_ ) (TA1.yz=is ta)
-           ; non-nil-y = λ ()
-           ; trace-xyz  = tnext q (TA1.trace-yz ta)
-           ; trace-xyyz = tnext q tra-05 } where
-        ta : TA1 fa finq (δ fa q i ) qd is
-        ta = tra-phase2 (δ fa q i ) is tr p 
-        y1 = TA1.y ta
-        z1 = TA1.z ta
-        tryz0 : Trace fa (y1 ++ z1) (δ fa qd i)
-        tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr
-        tryz : Trace fa (i ∷ y1 ++ z1) qd
-        tryz = tnext qd tryz0
-        -- create Trace (y ++ y ++ z)
-        tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
-               →  QDSEQ finq qd z1 {q} {y2} tr 
-               → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
-        tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q
-        ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
-        ... | false | record { eq = ne } = ⊥-elim ( ¬-bool  refl x₁ ) 
-        tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _  _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q
-        ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl ) 
-        ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) 
-        tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i)
-        tra-05 with equal→refl finq eq
-        ... | refl = tra-04 y1  (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta)
-   ... | false | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) 
-           ; non-nil-y = non-nil-y ta
-            ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
-        ta : TA fa (δ fa q i ) is
-        ta = tra-phase1 (δ fa q i ) is tr p
 
 open RegularLanguage
 open import Data.Nat.Properties
@@ -208,7 +126,7 @@
        (tr-accept→ (automaton r) _  (astart r) (TA.trace-xyyz TAnn) ) where
     n : ℕ
     n = suc (finite (afin r))
-    nn =  inputnn0 n i0 i1 []
+    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
@@ -217,23 +135,24 @@
     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 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
+    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 i0 i1 []) ≡⟨ tr→qs=is (automaton r) (inputnn0 n i0 i1 []) (astart r) nn04 ⟩
+         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
@@ -241,12 +160,65 @@
     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 = ?
+          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 = ?
+          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
+
 
+
+
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton-in-agda/src/pumping.agda	Wed Jul 26 21:20:16 2023 +0900
@@ -0,0 +1,162 @@
+module pumping 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 FiniteSet
+
+--
+--  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 Σ) → Q → Set where
+    tend  : {q : Q} → aend fa q ≡ true → Trace fa [] q
+    tnext : (q : Q) → {i : Σ} { is : List Σ} 
+        → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q 
+
+tr-len :  { Q : Set } { Σ : Set  }
+    → (fa : Automaton Q  Σ )
+    → (is : List Σ) → (q : Q) → Trace fa is q → suc (length is) ≡ length (trace fa q is ) 
+tr-len {Q} {Σ} fa .[] q (tend x) = refl 
+tr-len {Q} {Σ} fa (i ∷ is) q (tnext .q t) = cong suc (tr-len {Q} {Σ} fa is (δ fa q i) t)
+
+tr-accept→ : { Q : Set } { Σ : Set  }
+    → (fa : Automaton Q  Σ )
+    → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true
+tr-accept→ {Q} {Σ} fa [] q (tend x)  = x
+tr-accept→ {Q} {Σ} fa (i ∷ is) q  (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr
+
+tr-accept← : { Q : Set } { Σ : Set  }
+    → (fa : Automaton Q  Σ )
+    → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is q
+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) 
+
+tr→qs : { Q : Set } { Σ : Set  }
+    → (fa : Automaton Q  Σ )
+    → (is : List Σ) → (q : Q) → Trace fa is q → List Q
+tr→qs fa [] q (tend x) = []
+tr→qs fa (i ∷ is) q (tnext q tr) = q ∷ tr→qs fa is (δ fa q i) tr 
+
+tr→qs=is : { Q : Set } { Σ : Set  }
+    → (fa : Automaton Q  Σ )
+    → (is : List Σ) → (q : Q) → (tr : Trace fa is q ) → length is ≡  length (tr→qs fa is q tr)
+tr→qs=is fa .[] q (tend x) = refl
+tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is  (δ fa q i) tr)
+
+open Data.Maybe
+
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+open import Relation.Binary.Definitions
+open import Data.Unit using (⊤ ; tt)
+open import Data.Nat.Properties
+
+data QDSEQ { Q : Set } { Σ : Set  } { fa : Automaton  Q  Σ} ( finq : FiniteSet Q) (qd : Q) (z1 :  List Σ) :
+       {q : Q} {y2 : List Σ} → Trace fa (y2 ++ z1) q → Set where
+   qd-nil :  (q : Q) → (tr : Trace fa z1 q) → equal? finq qd q ≡ true → QDSEQ finq qd z1 tr
+   qd-next : {i : Σ} (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) (δ fa q i)) → equal? finq qd q ≡ false
+       → QDSEQ finq qd z1 tr 
+       → QDSEQ finq qd z1 (tnext q tr)
+
+record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
+    field
+       y z : List Σ
+       yz=is : y ++ z ≡ is 
+       trace-z    : Trace fa z  qd
+       trace-yz   : Trace fa (y ++ z)  q
+       q=qd : QDSEQ finq qd z trace-yz
+
+--
+-- using accept ≡ true may simplify the pumping-lemma
+-- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧  ...
+--
+-- like this ...
+-- record TA2 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
+--     field
+--        y z : List Σ
+--        yz=is : y ++ z ≡ is 
+--        trace-z    : accpet fa z qd ≡ true
+--        trace-yz   : accept fa (y ++ z)  q ≡ true
+--        q=qd  : last (tr→qs fa q trace-yz) ≡ just qd 
+--        ¬q=qd : non-last (tr→qs fa q trace-yz) ≡ just qd 
+
+record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
+    field
+       x y z : List Σ
+       xyz=is : x ++ y ++ z ≡ is 
+       trace-xyz  : Trace fa (x ++ y ++ z)  q
+       trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
+       non-nil-y : ¬ (y ≡ [])
+
+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
+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
+   tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
+   ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq
+        ; trace-z  = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr }
+   ... | false | record { eq = ne } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
+       ; q=qd = tra-08
+       ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
+            ta : TA1 fa finq (δ fa q i) qd is
+            ta = tra-phase2 (δ fa q i) is tr p 
+            tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i)
+            tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr
+            tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta))
+            tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p))  ne (TA1.q=qd ta)
+   tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa q is
+   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q
+   ... | true | record { eq = eq } = record { x = [] ; y = i ∷ TA1.y ta ;  z = TA1.z ta ; xyz=is =  cong (i ∷_ ) (TA1.yz=is ta)
+           ; non-nil-y = λ ()
+           ; trace-xyz  = tnext q (TA1.trace-yz ta)
+           ; trace-xyyz = tnext q tra-05 } where
+        ta : TA1 fa finq (δ fa q i ) qd is
+        ta = tra-phase2 (δ fa q i ) is tr p 
+        y1 = TA1.y ta
+        z1 = TA1.z ta
+        tryz0 : Trace fa (y1 ++ z1) (δ fa qd i)
+        tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr
+        tryz : Trace fa (i ∷ y1 ++ z1) qd
+        tryz = tnext qd tryz0
+        -- create Trace (y ++ y ++ z)
+        tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
+               →  QDSEQ finq qd z1 {q} {y2} tr 
+               → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
+        tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q
+        ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
+        ... | false | record { eq = ne } = ⊥-elim ( ¬-bool  refl x₁ ) 
+        tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _  _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q
+        ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl ) 
+        ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) 
+        tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i)
+        tra-05 with equal→refl finq eq
+        ... | refl = tra-04 y1  (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta)
+   ... | false | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) 
+           ; non-nil-y = non-nil-y ta
+            ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
+        ta : TA fa (δ fa q i ) is
+        ta = tra-phase1 (δ fa q i ) is tr p
+