Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/non-regular.agda @ 317:16e47a3c4eda

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 Mon, 03 Jan 2022 18:50:01 +0900
parents fd07e3205cea
children 4a00e5f2b793
comparison
equal deleted inserted replaced
316:fd07e3205cea 317:16e47a3c4eda
113 trace-z : Trace fa z qd 113 trace-z : Trace fa z qd
114 trace-yz : Trace fa (y ++ z) q 114 trace-yz : Trace fa (y ++ z) q
115 q=qd : QDSEQ finq qd z trace-yz 115 q=qd : QDSEQ finq qd z trace-yz
116 116
117 -- 117 --
118 -- using accept ≡ true may simplify the make-TA 118 -- using accept ≡ true may simplify the pumping-lemma
119 -- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧ ... 119 -- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧ ...
120 -- 120 --
121 -- like this ... 121 -- like this ...
122 -- record TA2 { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) ( q qd : Q ) (is : List Σ) : Set where 122 -- record TA2 { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) ( q qd : Q ) (is : List Σ) : Set where
123 -- field 123 -- field
134 xyz=is : x ++ y ++ z ≡ is 134 xyz=is : x ++ y ++ z ≡ is
135 trace-xyz : Trace fa (x ++ y ++ z) q 135 trace-xyz : Trace fa (x ++ y ++ z) q
136 trace-xyyz : Trace fa (x ++ y ++ y ++ z) q 136 trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
137 non-nil-y : ¬ (y ≡ []) 137 non-nil-y : ¬ (y ≡ [])
138 138
139 make-TA : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 139 pumping-lemma : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ)
140 → (tr : Trace fa is q ) 140 → (tr : Trace fa is q )
141 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true 141 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
142 → TA fa q is 142 → TA fa q is
143 make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where 143 pumping-lemma {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
144 open TA 144 open TA
145 tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) 145 tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q )
146 → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is 146 → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is
147 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q 147 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
148 ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq 148 ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq
192 open RegularLanguage 192 open RegularLanguage
193 open import Data.Nat.Properties 193 open import Data.Nat.Properties
194 open import nat 194 open import nat
195 195
196 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) 196 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r )
197 lemmaNN r Rg = {!!} where 197 lemmaNN r Rg = tann {TA.x TAnn} (TA.non-nil-y TAnn ) {!!} (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyz TAnn) )
198 (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyyz TAnn) ) where
198 n : ℕ 199 n : ℕ
199 n = suc (finite (afin r)) 200 n = suc (finite (afin r))
200 nn = inputnn0 n i0 i1 [] 201 nn = inputnn0 n i0 i1 []
201 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true 202 nn01 : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
202 nn01 zero = refl 203 nn01 zero = refl
235 length (inputnn0 n i0 i1 []) ≡⟨ tr→qs=is (automaton r) (inputnn0 n i0 i1 []) (astart r) nn04 ⟩ 236 length (inputnn0 n i0 i1 []) ≡⟨ tr→qs=is (automaton r) (inputnn0 n i0 i1 []) (astart r) nn04 ⟩
236 length nntrace ∎ where open ≤-Reasoning 237 length nntrace ∎ where open ≤-Reasoning
237 nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04) 238 nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04)
238 nn06 = dup-in-list>n (afin r) nntrace nn05 239 nn06 = dup-in-list>n (afin r) nntrace nn05
239 TAnn : TA (automaton r) (astart r) nn 240 TAnn : TA (automaton r) (astart r) nn
240 TAnn = make-TA (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06) 241 TAnn = pumping-lemma (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06)
241 count : In2 → List In2 → ℕ 242 count : In2 → List In2 → ℕ
242 count _ [] = 0 243 count _ [] = 0
243 count i0 (i0 ∷ s) = suc (count i0 s) 244 count i0 (i0 ∷ s) = suc (count i0 s)
244 count i1 (i1 ∷ s) = suc (count i1 s) 245 count i1 (i1 ∷ s) = suc (count i1 s)
245 count x (_ ∷ s) = count x s 246 count x (_ ∷ s) = count x s
248 nn11 {i0} (i0 ∷ s) t = cong suc ( nn11 s t ) 249 nn11 {i0} (i0 ∷ s) t = cong suc ( nn11 s t )
249 nn11 {i0} (i1 ∷ s) t = nn11 s t 250 nn11 {i0} (i1 ∷ s) t = nn11 s t
250 nn11 {i1} (i0 ∷ s) t = nn11 s t 251 nn11 {i1} (i0 ∷ s) t = nn11 s t
251 nn11 {i1} (i1 ∷ s) t = cong suc ( nn11 s t ) 252 nn11 {i1} (i1 ∷ s) t = cong suc ( nn11 s t )
252 nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s 253 nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
253 nn10 = {!!} 254 nn10 s p = nn101 s (subst (λ k → k ≡ true) (sym (Rg s)) p ) where
255 nn101 : (s : List In2) → inputnn1 s ≡ true → count i0 s ≡ count i1 s
256 nn101 [] p = refl
257 nn101 (x ∷ s) p = {!!}
254 i1-i0? : List In2 → Bool 258 i1-i0? : List In2 → Bool
255 i1-i0? [] = false 259 i1-i0? [] = false
256 i1-i0? (i1 ∷ []) = false 260 i1-i0? (i1 ∷ []) = false
257 i1-i0? (i0 ∷ []) = false 261 i1-i0? (i0 ∷ []) = false
258 i1-i0? (i1 ∷ i0 ∷ s) = true 262 i1-i0? (i1 ∷ i0 ∷ s) = true
277 is-10 : s ≡ s0 ++ i1 ∷ i0 ∷ s1 281 is-10 : s ≡ s0 ++ i1 ∷ i0 ∷ s1
278 not-mono : { s : List In2 } → ¬ (mono-color s ≡ true) → Is10 (s ++ s) 282 not-mono : { s : List In2 } → ¬ (mono-color s ≡ true) → Is10 (s ++ s)
279 not-mono = {!!} 283 not-mono = {!!}
280 mono-count : { s : List In2 } → mono-color s ≡ true → (length s ≡ count i0 s) ∨ ( length s ≡ count i1 s) 284 mono-count : { s : List In2 } → mono-color s ≡ true → (length s ≡ count i0 s) ∨ ( length s ≡ count i1 s)
281 mono-count = {!!} 285 mono-count = {!!}
282 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 ) 286 tann : {x y z : List In2} → ¬ y ≡ []
283 tann {x} {y} {z} ny axyz axyyz with mono-color y 287 → x ++ y ++ z ≡ nn
288 → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true )
289 tann {x} {y} {z} ny eq axyz axyyz with mono-color y
284 ... | true = {!!} 290 ... | true = {!!}
285 ... | false = {!!} 291 ... | false = {!!}
286 292