Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/regular-star.agda @ 403:c298981108c1
fix for std-lib 2.0
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Sep 2023 11:32:01 +0900 |
| parents | 708570e55a91 |
| children |
| rev | line source |
|---|---|
|
383
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
274
diff
changeset
|
1 {-# OPTIONS --allow-unsolved-metas #-} |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
274
diff
changeset
|
2 |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
3 module regular-star where |
| 141 | 4 |
| 5 open import Level renaming ( suc to Suc ; zero to Zero ) | |
| 6 open import Data.List | |
| 7 open import Data.Nat hiding ( _≟_ ) | |
| 8 open import Data.Fin hiding ( _+_ ) | |
| 9 open import Data.Empty | |
| 10 open import Data.Unit | |
| 11 open import Data.Product | |
| 12 -- open import Data.Maybe | |
| 13 open import Relation.Nullary | |
| 14 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 15 open import logic | |
| 16 open import nat | |
| 17 open import automaton | |
| 268 | 18 open import regular-language |
| 141 | 19 |
| 20 open import nfa | |
| 21 open import sbconst2 | |
| 268 | 22 open import finiteSet |
| 23 open import finiteSetUtil | |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
24 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
|
25 open import regular-concat |
| 141 | 26 |
| 268 | 27 open Automaton |
| 28 open FiniteSet | |
| 29 | |
| 269 | 30 open RegularLanguage |
| 268 | 31 |
|
383
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
274
diff
changeset
|
32 -- |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
274
diff
changeset
|
33 -- Star (contain A) = Concat (contain A) ( Star (contain A ) ) \/ Empty |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
274
diff
changeset
|
34 -- |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
274
diff
changeset
|
35 |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
36 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
|
37 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
|
38 module Star-NFA where |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
39 δ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
|
40 δ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
|
41 ... | 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
|
42 ... | 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
|
43 nend : states A → Bool |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
44 nend q = aend (automaton A) q |
| 141 | 45 |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
46 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
|
47 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
|
48 |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
49 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
|
50 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
|
51 |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
52 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
|
53 M-Star {Σ} A = record { |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
54 states = states A → Bool |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
55 ; astart = Star-NFA-start A |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
56 ; afin = fin→ (afin A) |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
57 ; 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
|
58 } |
| 141 | 59 |
| 60 open Split | |
| 61 | |
| 62 open _∧_ | |
| 63 | |
| 64 open NAutomaton | |
| 65 open import Data.List.Properties | |
| 66 | |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
67 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
|
68 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
|
69 NFA = (Star-NFA A ) |
| 141 | 70 |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
71 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
|
72 closed-in-star→ star = {!!} |
| 163 | 73 |
| 74 open Found | |
| 141 | 75 |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
76 closed-in-star← : contain (M-Star A ) x ≡ true → Star (contain A) x ≡ true |
| 403 | 77 closed-in-star← C with subset-construction-lemma← (SNFA-exist A ) NFA (Star-NFA-start A) x C |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
78 ... | CC = {!!} |
| 141 | 79 |
| 80 | |
| 81 | |
| 82 |