Mercurial > hg > Members > kono > Proof > automaton
comparison agda/flcagl.agda @ 52:8438c989d5a7
fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 02 Oct 2019 13:19:44 +0900 |
parents | bc0400528027 |
children | eddc4ad8e99a |
comparison
equal
deleted
inserted
replaced
51:bc0400528027 | 52:8438c989d5a7 |
---|---|
69 _∪_ : ∀{i} (k l : Lang i) → Lang i | 69 _∪_ : ∀{i} (k l : Lang i) → Lang i |
70 ν (k ∪ l) = ν k ∨ ν l | 70 ν (k ∪ l) = ν k ∨ ν l |
71 δ (k ∪ l) x = δ k x ∪ δ l x | 71 δ (k ∪ l) x = δ k x ∪ δ l x |
72 | 72 |
73 | 73 |
74 _·'_ : ∀{i} (k l : Lang i) → Lang i | 74 _·_ : ∀{i} (k l : Lang i) → Lang i |
75 ν (k ·' l) = ν k ∧ ν l | |
76 δ (k ·' l) x = let k′l = δ k x ·' l in if ν k then k′l ∪ δ l x else k′l | |
77 | |
78 _·_ : ∀{i} (k l : Lang i ) → Lang i | |
79 ν (k · l) = ν k ∧ ν l | 75 ν (k · l) = ν k ∧ ν l |
80 δ (_·_ {i} k l) {j} x = | 76 δ (k · l) x = let k′l = δ k x · l in if ν k then k′l ∪ δ l x else k′l |
77 | |
78 _*_ : ∀{i} (k l : Lang i ) → Lang i | |
79 ν (k * l) = ν k ∧ ν l | |
80 δ (_*_ {i} k l) {j} x = | |
81 let | 81 let |
82 k′l : Lang j | 82 k′l : Lang j |
83 k′l = _·_ {j} (δ k {j} x) l | 83 k′l = _*_ {j} (δ k {j} x) l |
84 in if ν k then _∪_ {j} k′l (δ l {j} x) else k′l | 84 in if ν k then _∪_ {j} k′l (δ l {j} x) else k′l |
85 | 85 |
86 _* : ∀{i} (l : Lang i) → Lang i | 86 _* : ∀{i} (l : Lang i) → Lang i |
87 ν (l *) = true | 87 ν (l *) = true |
88 δ (l *) x = δ l x · (l *) | 88 δ (l *) x = δ l x · (l *) |
216 ≈⟨ ≅refl ⟩ | 216 ≈⟨ ≅refl ⟩ |
217 (if false then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m) | 217 (if false then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m) |
218 ∎ | 218 ∎ |
219 where open EqR (Bis _) | 219 where open EqR (Bis _) |
220 ≅δ (concat-union-distribl k {l} {m}) a | true | false = begin | 220 ≅δ (concat-union-distribl k {l} {m}) a | true | false = begin |
221 (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) | 221 (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩ |
222 ≈⟨ ≅refl ⟩ | 222 ((δ k a ∪ δ l a) · m ) ∪ δ m a ≈⟨ union-congl (concat-union-distribl _) ⟩ |
223 ((δ k a ∪ δ l a) · m ) ∪ δ m a | 223 (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨ union-assoc _ ⟩ |
224 ≈⟨ union-congl (concat-union-distribl _) ⟩ | 224 δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨ union-congr ( union-comm _ _) ⟩ |
225 (δ k a · m ∪ δ l a · m) ∪ δ m a | 225 δ k a · m ∪ δ m a ∪ δ l a · m ≈⟨ ≅sym ( union-assoc _ ) ⟩ |
226 ≈⟨ union-assoc _ ⟩ | 226 (δ k a · m ∪ δ m a) ∪ δ l a · m ≈⟨ ≅refl ⟩ |
227 δ k a · m ∪ ( δ l a · m ∪ δ m a ) | |
228 ≈⟨ union-congr ( union-comm _ _) ⟩ | |
229 δ k a · m ∪ δ m a ∪ δ l a · m | |
230 ≈⟨ ≅sym ( union-assoc _ ) ⟩ | |
231 (δ k a · m ∪ δ m a) ∪ δ l a · m | |
232 ≈⟨ ≅refl ⟩ | |
233 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if false then δ l a · m ∪ δ m a else δ l a · m)) | 227 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if false then δ l a · m ∪ δ m a else δ l a · m)) |
234 ∎ | 228 ∎ |
235 where open EqR (Bis _) | 229 where open EqR (Bis _) |
236 ≅δ (concat-union-distribl k {l} {m}) a | true | true = begin | 230 ≅δ (concat-union-distribl k {l} {m}) a | true | true = begin |
237 (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) | 231 (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩ |
238 ≈⟨ ≅refl ⟩ | 232 (δ k a ∪ δ l a) · m ∪ δ m a ≈⟨ union-congl ( concat-union-distribl _ ) ⟩ |
239 (δ k a ∪ δ l a) · m ∪ δ m a | 233 (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨ union-assoc _ ⟩ |
240 ≈⟨ union-congl ( concat-union-distribl _ ) ⟩ | 234 δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨ ≅sym ( union-congr ( union-congr ( union-idem _ ) ) ) ⟩ |
241 (δ k a · m ∪ δ l a · m) ∪ δ m a | 235 δ k a · m ∪ ( δ l a · m ∪ (δ m a ∪ δ m a) ) ≈⟨ ≅sym ( union-congr ( union-assoc _ )) ⟩ |
242 ≈⟨ union-assoc _ ⟩ | 236 δ k a · m ∪ ( (δ l a · m ∪ δ m a ) ∪ δ m a ) ≈⟨ union-congr ( union-congl ( union-comm _ _) ) ⟩ |
243 δ k a · m ∪ ( δ l a · m ∪ δ m a ) | 237 δ k a · m ∪ ( (δ m a ∪ δ l a · m ) ∪ δ m a ) ≈⟨ ≅sym ( union-assoc _ ) ⟩ |
244 ≈⟨ ≅sym ( union-congr ( union-congr ( union-idem _ ) ) ) ⟩ | 238 ( δ k a · m ∪ (δ m a ∪ δ l a · m )) ∪ δ m a ≈⟨ ≅sym ( union-congl ( union-assoc _ ) ) ⟩ |
245 δ k a · m ∪ ( δ l a · m ∪ (δ m a ∪ δ m a) ) | 239 ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a ≈⟨ union-assoc _ ⟩ |
246 ≈⟨ ≅sym ( union-congr ( union-assoc _ )) ⟩ | 240 (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a ≈⟨ ≅refl ⟩ |
247 δ k a · m ∪ ( (δ l a · m ∪ δ m a ) ∪ δ m a ) | 241 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m)) |
248 ≈⟨ union-congr ( union-congl ( union-comm _ _) ) ⟩ | |
249 δ k a · m ∪ ( (δ m a ∪ δ l a · m ) ∪ δ m a ) | |
250 ≈⟨ ≅sym ( union-assoc _ ) ⟩ | |
251 ( δ k a · m ∪ (δ m a ∪ δ l a · m )) ∪ δ m a | |
252 ≈⟨ ≅sym ( union-congl ( union-assoc _ ) ) ⟩ | |
253 ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a | |
254 ≈⟨ union-assoc _ ⟩ | |
255 (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a | |
256 ≈⟨ ≅refl ⟩ | |
257 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m)) | |
258 ∎ | 242 ∎ |
259 where open EqR (Bis _) | 243 where open EqR (Bis _) |
260 | 244 |
261 postulate | 245 postulate |
262 concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅ | 246 concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅ |
308 ∎ where open EqR (Bis _) | 292 ∎ where open EqR (Bis _) |
309 | 293 |
310 star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l * | 294 star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l * |
311 ≅ν (star-concat-idem l) = refl | 295 ≅ν (star-concat-idem l) = refl |
312 ≅δ (star-concat-idem l) a = begin | 296 ≅δ (star-concat-idem l) a = begin |
313 δ ((l *) · (l *)) a | 297 δ ((l *) · (l *)) a ≈⟨ union-congl (concat-assoc _) ⟩ |
314 ≈⟨ union-congl (concat-assoc _) ⟩ | 298 δ l a · (l * · l *) ∪ δ l a · l * ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩ |
315 δ l a · (l * · l *) ∪ δ l a · l * | 299 δ l a · l * ∪ δ l a · l * ≈⟨ union-idem _ ⟩ |
316 ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩ | 300 δ (l *) a ∎ where open EqR (Bis _) |
317 δ l a · l * ∪ δ l a · l * | |
318 ≈⟨ union-idem _ ⟩ | |
319 δ (l *) a | |
320 ∎ where open EqR (Bis _) | |
321 | 301 |
322 star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l * | 302 star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l * |
323 ≅ν (star-idem l) = refl | 303 ≅ν (star-idem l) = refl |
324 ≅δ (star-idem l) a = begin | 304 ≅δ (star-idem l) a = begin |
325 δ ((l *) *) a ≈⟨ concat-assoc (δ l a) ⟩ | 305 δ ((l *) *) a ≈⟨ concat-assoc (δ l a) ⟩ |
475 lang (starA s0 da) ss ≅⟨ i ⟩≅ | 455 lang (starA s0 da) ss ≅⟨ i ⟩≅ |
476 lang (powA (acceptingInitial s0 da)) ss · (lang da s0) * | 456 lang (powA (acceptingInitial s0 da)) ss · (lang da s0) * |
477 starA-correct : ∀{i S} (da : DA S) (s0 : S) → | 457 starA-correct : ∀{i S} (da : DA S) (s0 : S) → |
478 lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) * | 458 lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) * |
479 | 459 |
460 record NAutomaton ( Q : Set ) ( Σ : Set ) | |
461 : Set where | |
462 field | |
463 Nδ : Q → Σ → Q → Bool | |
464 Nstart : Q → Bool | |
465 Nend : Q → Bool | |
466 | |
467 postulate | |
468 exists : { S : Set} → ( S → Bool ) → Bool | |
469 | |
470 nlang : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i | |
471 Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x )) | |
472 Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) | |
473 | |
474 -- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i | |
475 -- Lang.ν (nlang' nfa s) = DA.ν nfa s | |
476 -- Lang.δ (nlang' nfa s) a = nlang' nfa (DA.δ nfa s a) | |
477 |