Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/regular-language.agda @ 411:207e6c4e155c
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 29 Nov 2023 17:40:55 +0900 |
parents | db02b6938e04 |
children | b85402051cdb |
rev | line source |
---|---|
405 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
2 | |
65 | 3 module regular-language where |
4 | |
5 open import Level renaming ( suc to Suc ; zero to Zero ) | |
411 | 6 open import Data.List |
65 | 7 open import Data.Nat hiding ( _≟_ ) |
70 | 8 open import Data.Fin hiding ( _+_ ) |
411 | 9 open import Data.Empty |
10 open import Data.Unit | |
65 | 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 | |
70 | 16 open import nat |
65 | 17 open import automaton |
18 | |
19 language : { Σ : Set } → Set | |
20 language {Σ} = List Σ → Bool | |
21 | |
22 language-L : { Σ : Set } → Set | |
23 language-L {Σ} = List (List Σ) | |
24 | |
25 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} | |
330 | 26 Union {Σ} A B x = A x \/ B x |
65 | 27 |
330 | 28 split : {Σ : Set} → (x y : language {Σ} ) → language {Σ} |
65 | 29 split x y [] = x [] /\ y [] |
30 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/ | |
31 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t | |
32 | |
33 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} | |
34 Concat {Σ} A B = split A B | |
35 | |
405 | 36 -- {-# TERMINATING #-} |
37 -- Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ} | |
38 -- Star1 {Σ} A [] = true | |
39 -- Star0 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t) | |
383
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
330
diff
changeset
|
40 |
401 | 41 -- Terminating version of Star1 |
42 -- | |
43 | |
411 | 44 -- regular-langue (P *) ( a ∷ b ∷ c ∷ [] ) = |
45 -- (P []) \/ | |
46 -- (P (a ∷ []) /\ repeat P (b ∷ c ∷ []) ) \/ | |
47 -- (P (a ∷ b ∷ []) /\ repeat P (c ∷ []) ) \/ | |
48 -- (P (a ∷ b ∷ c ∷ []) | |
49 -- | |
50 -- repeat : {Σ : Set} → (x : language {Σ} ) → language {Σ} | |
51 -- repeat x [] = true | |
52 -- repeat x (h ∷ t) = (x [] /\ ? (h ∷ t)) \/ | |
53 -- repeat (λ t1 → x ( h ∷ t1 )) t | |
383
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
330
diff
changeset
|
54 |
411 | 55 repeat : {Σ : Set} → (P : List Σ → Bool) → (pre y : List Σ ) → Bool |
56 repeat P [] [] = true | |
57 repeat P (h ∷ t) [] = P (h ∷ t) | |
58 repeat P pre (h ∷ []) = P (pre ++ (h ∷ [])) | |
59 repeat P pre (h ∷ y@(_ ∷ _)) = | |
60 ((P (pre ++ (h ∷ []))) /\ repeat P [] y ) | |
61 \/ repeat P (pre ++ (h ∷ [])) y | |
62 | |
63 Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool | |
64 Star {Σ} x y = repeat x [] y | |
65 | 65 |
406 | 66 -- We have to prove definitions of Concat and Star are equivalent to the set theoretic definitions |
67 | |
68 -- 1. A ∪ B = { x | x ∈ A \/ x ∈ B } | |
69 -- 2. A ∘ B = { x | ∃ y ∈ A, z ∈ B, x = y ++ z } | |
70 -- 3. A* = { x | ∃ n ∈ ℕ, y1, y2, ..., yn ∈ A, x = y1 ++ y2 ++ ... ++ yn } | |
71 | |
72 -- lemma-Union : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) → Union A B x ≡ ( A x \/ B x ) | |
73 -- lemma-Union = ? | |
74 | |
411 | 75 -- lemma-Concat : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) |
406 | 76 -- → Concat A B x ≡ ( ∃ λ y → ∃ λ z → A y /\ B z /\ x ≡ y ++ z ) |
77 -- lemma-Concat = ? | |
78 | |
141 | 79 open import automaton-ex |
80 | |
87 | 81 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ ( |
411 | 82 ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ |
83 ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ | |
69 | 84 ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/ |
411 | 85 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B [] ) |
69 | 86 ) |
87 | 87 test-AB→split {_} {A} {B} = refl |
69 | 88 |
266 | 89 star-nil : {Σ : Set} → ( A : language {Σ} ) → Star A [] ≡ true |
90 star-nil A = refl | |
91 | |
267 | 92 open Automaton |
268 | 93 open import finiteSet |
94 open import finiteSetUtil | |
267 | 95 |
96 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where | |
97 field | |
268 | 98 states : Set |
99 astart : states | |
100 afin : FiniteSet states | |
267 | 101 automaton : Automaton states Σ |
102 contain : List Σ → Bool | |
103 contain x = accept automaton astart x | |
104 | |
268 | 105 open RegularLanguage |
106 | |
107 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set | |
108 isRegular A x r = A x ≡ contain r x | |
109 | |
411 | 110 RegularLanguage-is-language : { Σ : Set } → RegularLanguage Σ → language {Σ} |
111 RegularLanguage-is-language {Σ} R = RegularLanguage.contain R | |
267 | 112 |
113 RegularLanguage-is-language' : { Σ : Set } → RegularLanguage Σ → List Σ → Bool | |
114 RegularLanguage-is-language' {Σ} R x = accept (automaton R) (astart R) x where | |
115 open RegularLanguage | |
116 | |
117 -- a language is implemented by an automaton | |
65 | 118 |
411 | 119 -- postulate |
126 | 120 -- fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b} |
73 | 121 |
65 | 122 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ |
123 M-Union {Σ} A B = record { | |
124 states = states A × states B | |
125 ; astart = ( astart A , astart B ) | |
268 | 126 ; afin = fin-× (afin A) (afin B) |
65 | 127 ; automaton = record { |
128 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x ) | |
129 ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) ) | |
130 } | |
411 | 131 } |
65 | 132 |
133 closed-in-union : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B ) | |
134 closed-in-union A B [] = lemma where | |
135 lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡ | |
136 aend (automaton A) (astart A) \/ aend (automaton B) (astart B) | |
137 lemma = refl | |
138 closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where | |
411 | 139 lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) → |
65 | 140 accept (automaton A) qa t \/ accept (automaton B) qb t |
141 ≡ accept (automaton (M-Union A B)) (qa , qb) t | |
142 lemma1 [] qa qb = refl | |
143 lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h)) | |
144 | |
406 | 145 |
411 | 146 |
406 | 147 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x : List Σ ) : Set where |
148 field | |
149 sp0 sp1 : List Σ | |
150 sp-concat : sp0 ++ sp1 ≡ x | |
151 prop0 : A sp0 ≡ true | |
152 prop1 : B sp1 ≡ true | |
153 | |
154 open Split | |
155 | |
408 | 156 AB→split1 : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → {z : List Σ} → A x ≡ true → B y ≡ true → z ≡ x ++ y → Split A B z |
157 AB→split1 {Σ} A B x y {z} ax by z=xy = record { sp0 = x ; sp1 = y ; sp-concat = sym z=xy ; prop0 = ax ; prop1 = by } | |
158 | |
406 | 159 list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] ) |
408 | 160 list-empty++ [] [] _ = record { proj1 = refl ; proj2 = refl } |
406 | 161 list-empty++ [] (x ∷ y) () |
162 list-empty++ (x ∷ x₁) y () | |
163 | |
164 open _∧_ | |
165 | |
166 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
167 | |
168 c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true | |
169 → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) | |
170 → split (λ t1 → A (h ∷ t1)) B t ≡ true | |
171 c-split-lemma {Σ} A B h t eq p = sym ( begin | |
172 true | |
173 ≡⟨ sym eq ⟩ | |
411 | 174 split A B (h ∷ t ) |
406 | 175 ≡⟨⟩ |
176 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t | |
177 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩ | |
178 false \/ split (λ t1 → A (h ∷ t1)) B t | |
179 ≡⟨ bool-or-1 refl ⟩ | |
180 split (λ t1 → A (h ∷ t1)) B t | |
181 ∎ ) where | |
411 | 182 open ≡-Reasoning |
406 | 183 lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false |
184 lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A ) | |
185 lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B ) | |
186 | |
187 split→AB : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x | |
411 | 188 split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true |
189 split→AB {Σ} A B [] eq | yes eqa | yes eqb = | |
406 | 190 record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb } |
191 split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p )) | |
192 split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p )) | |
193 split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true | |
194 ... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py } | |
195 ... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) ) | |
196 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } | |
197 split→AB {Σ} A B (h ∷ t ) eq | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) ) | |
198 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S } | |
199 | |
200 AB→split : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true | |
201 AB→split {Σ} A B [] [] eqa eqb = begin | |
408 | 202 split A B [] ≡⟨⟩ |
203 A [] /\ B [] ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩ | |
406 | 204 true |
205 ∎ where open ≡-Reasoning | |
206 AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin | |
408 | 207 split A B (h ∷ y ) ≡⟨⟩ |
208 A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩ | |
209 true /\ true \/ split (λ t1 → A (h ∷ t1)) B y ≡⟨⟩ | |
210 true \/ split (λ t1 → A (h ∷ t1)) B y ≡⟨⟩ | |
211 true ∎ where open ≡-Reasoning | |
406 | 212 AB→split {Σ} A B (h ∷ t) y eqa eqb = begin |
408 | 213 split A B ((h ∷ t) ++ y) ≡⟨⟩ |
406 | 214 A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y) |
215 ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩ | |
408 | 216 A [] /\ B (h ∷ t ++ y) \/ true ≡⟨ bool-or-3 ⟩ |
217 true ∎ where open ≡-Reasoning | |
218 | |
406 | 219 |
411 | 220 split→AB1 : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x → split A B x ≡ true |
409 | 221 split→AB1 {Σ} A B x S = subst (λ k → split A B k ≡ true ) (sp-concat S) ( AB→split A B _ _ (prop0 S) (prop1 S) ) |
411 | 222 |
408 | 223 |
410 | 224 -- low of exclude middle of Split A B x |
225 lemma-concat : {Σ : Set} → ( A B : language {Σ} ) → (x : List Σ) → Split A B x ∨ ( ¬ Split A B x ) | |
226 lemma-concat {Σ} A B x with split A B x in eq | |
227 ... | true = case1 (split→AB A B x eq ) | |
411 | 228 ... | false = case2 (λ p → ¬-bool eq (split→AB1 A B x p )) |
410 | 229 |
230 -- Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} | |
231 -- Concat {Σ} A B = split A B | |
232 | |
233 Concat' : {Σ : Set} → ( A B : language {Σ} ) → (x : List Σ) → Set | |
234 Concat' {Σ} A B = λ x → Split A B x | |
235 | |
236 record StarProp {Σ : Set} (A : List Σ → Bool ) (x : List Σ ) : Set where | |
237 field | |
238 spn : List ( List Σ ) | |
239 spn-concat : foldr (λ k → k ++_ ) [] spn ≡ x | |
240 propn : foldr (λ k → λ j → A k /\ j ) true spn ≡ true | |
241 | |
242 open StarProp | |
243 | |
411 | 244 open import Data.List.Properties |
410 | 245 |
411 | 246 Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x |
247 Star→StarProp {Σ} A x ax = ss00 [] x ax where | |
248 ss00 : (pre x : List Σ) → repeat A pre x ≡ true → StarProp A (pre ++ x ) | |
249 ss00 [] [] eq = record { spn = [] ; spn-concat = refl ; propn = eq } | |
250 ss00 (h ∷ t) [] eq = record { spn = (h ∷ t) ∷ [] ; spn-concat = refl ; propn = bool-and-tt eq refl } | |
251 ss00 pre (h ∷ []) eq = record { spn = (pre ++ (h ∷ [])) ∷ [] ; spn-concat = ++-assoc pre _ _ | |
252 ; propn = bool-and-tt (trans (sym (ss01 pre (h ∷ []) refl )) eq) refl } where | |
253 ss01 : (pre x : List Σ) → x ≡ h ∷ [] → repeat A pre x ≡ A (pre ++ (h ∷ [])) | |
254 ss01 [] (h ∷ []) refl = refl | |
255 ss01 (x ∷ pre) (h ∷ []) refl = refl | |
256 ss00 pre (h ∷ y@(i ∷ t)) eq = ? where | |
257 ss01 : (pre x : List Σ) → x ≡ y → ( ((A (pre ++ (h ∷ []))) /\ repeat A [] y ) \/ repeat A (pre ++ (h ∷ [])) y ) ≡ repeat A pre (h ∷ y ) | |
258 ss01 = ? | |
259 ss02 : StarProp A (pre ++ h ∷ y ) | |
260 ss02 with (A (pre ++ (h ∷ []))) /\ repeat A [] y in eq1 | |
261 ... | true = ? | |
262 ... | false = ? where | |
263 ss03 : repeat A (pre ++ (h ∷ [])) y ≡ true | |
264 ss03 = ? | |
410 | 265 |
411 | 266 -- |
267 -- StarProp→Star : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x → Star A x ≡ true | |
268 -- StarProp→Star {Σ} A x sp = subst (λ k → Star A k ≡ true ) (spsx (spn sp) refl) ( sps1 (spn sp) refl ) where | |
269 -- spsx : (y : List ( List Σ ) ) → spn sp ≡ y → foldr (λ k → k ++_ ) [] y ≡ x | |
270 -- spsx y refl = spn-concat sp | |
271 -- sps1 : (y : List ( List Σ ) ) → spn sp ≡ y → Star A (foldr (λ k → k ++_ ) [] y) ≡ true | |
272 -- sps1 [] sp=y = refl | |
273 -- sps1 ([] ∷ t) sp=y = ? | |
274 -- sps1 ((x ∷ h) ∷ t) sp=y = ? | |
275 -- | |
276 -- | |
277 -- lemma-starprop : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x ∨ ( ¬ StarProp A x ) | |
278 -- lemma-starprop = ? | |
279 -- |