Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/regular-star.agda @ 285:6e85b8b0d8db

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove ls<n
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Dec 2021 00:28:29 +0900
parents 1c8ed1220489
children 708570e55a91
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
270
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
1 module regular-star where
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level renaming ( suc to Suc ; zero to Zero )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.List
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Nat hiding ( _≟_ )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.Fin hiding ( _+_ )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Data.Empty
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Data.Unit
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Data.Product
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 -- open import Data.Maybe
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Relation.Nullary
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import logic
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import nat
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import automaton
268
8006cbd87b20 fix concat dfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
16 open import regular-language
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 open import nfa
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 open import sbconst2
268
8006cbd87b20 fix concat dfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
20 open import finiteSet
8006cbd87b20 fix concat dfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
21 open import finiteSetUtil
270
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
22 open import Relation.Binary.PropositionalEquality hiding ( [_] )
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
23 open import regular-concat
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
268
8006cbd87b20 fix concat dfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
25 open Automaton
8006cbd87b20 fix concat dfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
26 open FiniteSet
8006cbd87b20 fix concat dfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
27
269
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
28 open RegularLanguage
268
8006cbd87b20 fix concat dfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
29
270
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
30 Star-NFA : {Σ : Set} → (A : RegularLanguage Σ ) → NAutomaton (states A ) Σ
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
31 Star-NFA {Σ} A = record { Nδ = δnfa ; Nend = nend }
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
32 module Star-NFA where
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
33 δnfa : states A → Σ → states A → Bool
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
34 δnfa q i q₁ with aend (automaton A) q
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
35 ... | true = equal? (afin A) ( astart A) q₁
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
36 ... | false = equal? (afin A) (δ (automaton A) q i) q₁
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
37 nend : states A → Bool
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
38 nend q = aend (automaton A) q
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
270
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
40 Star-NFA-start : {Σ : Set} → (A : RegularLanguage Σ ) → states A → Bool
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
41 Star-NFA-start A q = equal? (afin A) (astart A) q \/ aend (automaton A) q
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
42
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
43 SNFA-exist : {Σ : Set} → (A : RegularLanguage Σ ) → (states A → Bool) → Bool
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
44 SNFA-exist A qs = exists (afin A) qs
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
45
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
46 M-Star : {Σ : Set} → (A : RegularLanguage Σ ) → RegularLanguage Σ
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
47 M-Star {Σ} A = record {
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
48 states = states A → Bool
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
49 ; astart = Star-NFA-start A
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
50 ; afin = fin→ (afin A)
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
51 ; automaton = subset-construction (SNFA-exist A ) (Star-NFA A )
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
52 }
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 open Split
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 open _∧_
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 open NAutomaton
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 open import Data.List.Properties
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
270
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
61 closed-in-star : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Star (contain A) ) x ( M-Star A )
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
62 closed-in-star {Σ} A B x = ≡-Bool-func closed-in-star→ closed-in-star← where
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
63 NFA = (Star-NFA A )
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
270
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
65 closed-in-star→ : Star (contain A) x ≡ true → contain (M-Star A ) x ≡ true
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
66 closed-in-star→ star = {!!}
163
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
67
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 141
diff changeset
68 open Found
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
270
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
70 closed-in-star← : contain (M-Star A ) x ≡ true → Star (contain A) x ≡ true
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
71 closed-in-star← C with subset-construction-lemma← (SNFA-exist A ) NFA {!!} x C
dd98e7e5d4a5 derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
72 ... | CC = {!!}
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76