|
266
|
1 {-# OPTIONS --sized-types #-}
|
|
46
|
2 open import Relation.Nullary
|
|
|
3 open import Relation.Binary.PropositionalEquality
|
|
|
4 module flcagl
|
|
|
5 (A : Set)
|
|
|
6 ( _≟_ : (a b : A) → Dec ( a ≡ b ) ) where
|
|
|
7
|
|
|
8 open import Data.Bool hiding ( _≟_ )
|
|
|
9 -- open import Data.Maybe
|
|
|
10 open import Level renaming ( zero to Zero ; suc to succ )
|
|
|
11 open import Size
|
|
|
12
|
|
|
13 module List where
|
|
|
14
|
|
|
15 data List (i : Size) (A : Set) : Set where
|
|
|
16 [] : List i A
|
|
|
17 _∷_ : {j : Size< i} (x : A) (xs : List j A) → List i A
|
|
|
18
|
|
|
19
|
|
|
20 map : ∀{i A B} → (A → B) → List i A → List i B
|
|
|
21 map f [] = []
|
|
|
22 map f ( x ∷ xs)= f x ∷ map f xs
|
|
|
23
|
|
|
24 foldr : ∀{i} {A B : Set} → (A → B → B) → B → List i A → B
|
|
|
25 foldr c n [] = n
|
|
|
26 foldr c n (x ∷ xs) = c x (foldr c n xs)
|
|
|
27
|
|
|
28 any : ∀{i A} → (A → Bool) → List i A → Bool
|
|
|
29 any p xs = foldr _∨_ false (map p xs)
|
|
|
30
|
|
|
31 module Lang where
|
|
|
32
|
|
|
33 open List
|
|
|
34
|
|
|
35 record Lang (i : Size) : Set where
|
|
|
36 coinductive
|
|
|
37 field
|
|
|
38 ν : Bool
|
|
|
39 δ : ∀{j : Size< i} → A → Lang j
|
|
|
40
|
|
|
41 open Lang
|
|
|
42
|
|
|
43 _∋_ : ∀{i} → Lang i → List i A → Bool
|
|
|
44 l ∋ [] = ν l
|
|
|
45 l ∋ ( a ∷ as ) = δ l a ∋ as
|
|
|
46
|
|
|
47 trie : ∀{i} (f : List i A → Bool) → Lang i
|
|
|
48 ν (trie f) = f []
|
|
|
49 δ (trie f) a = trie (λ as → f (a ∷ as))
|
|
|
50
|
|
|
51 ∅ : ∀{i} → Lang i
|
|
|
52 ν ∅ = false
|
|
|
53 δ ∅ x = ∅
|
|
|
54
|
|
|
55 ε : ∀{i} → Lang i
|
|
|
56 ν ε = true
|
|
|
57 δ ε x = ∅
|
|
|
58
|
|
|
59 open import Relation.Nullary.Decidable
|
|
|
60
|
|
|
61 char : ∀{i} (a : A) → Lang i
|
|
|
62 ν (char a) = false
|
|
|
63 δ (char a) x = if ⌊ a ≟ x ⌋ then ε else ∅
|
|
|
64
|
|
|
65 compl : ∀{i} (l : Lang i) → Lang i
|
|
|
66 ν (compl l) = not (ν l)
|
|
|
67 δ (compl l) x = compl (δ l x)
|
|
|
68
|
|
|
69
|
|
|
70 _∪_ : ∀{i} (k l : Lang i) → Lang i
|
|
|
71 ν (k ∪ l) = ν k ∨ ν l
|
|
|
72 δ (k ∪ l) x = δ k x ∪ δ l x
|
|
|
73
|
|
|
74
|
|
52
|
75 _·_ : ∀{i} (k l : Lang i) → Lang i
|
|
|
76 ν (k · l) = ν k ∧ ν l
|
|
|
77 δ (k · l) x = let k′l = δ k x · l in if ν k then k′l ∪ δ l x else k′l
|
|
46
|
78
|
|
52
|
79 _*_ : ∀{i} (k l : Lang i ) → Lang i
|
|
|
80 ν (k * l) = ν k ∧ ν l
|
|
|
81 δ (_*_ {i} k l) {j} x =
|
|
46
|
82 let
|
|
|
83 k′l : Lang j
|
|
52
|
84 k′l = _*_ {j} (δ k {j} x) l
|
|
46
|
85 in if ν k then _∪_ {j} k′l (δ l {j} x) else k′l
|
|
|
86
|
|
|
87 _* : ∀{i} (l : Lang i) → Lang i
|
|
|
88 ν (l *) = true
|
|
|
89 δ (l *) x = δ l x · (l *)
|
|
|
90
|
|
|
91 record _≅⟨_⟩≅_ (l : Lang ∞ ) i (k : Lang ∞) : Set where
|
|
|
92 coinductive
|
|
|
93 field ≅ν : ν l ≡ ν k
|
|
|
94 ≅δ : ∀ {j : Size< i } (a : A ) → δ l a ≅⟨ j ⟩≅ δ k a
|
|
|
95
|
|
|
96 open _≅⟨_⟩≅_
|
|
|
97
|
|
|
98 ≅refl : ∀{i} {l : Lang ∞} → l ≅⟨ i ⟩≅ l
|
|
|
99 ≅ν ≅refl = refl
|
|
|
100 ≅δ ≅refl a = ≅refl
|
|
|
101
|
|
|
102
|
|
|
103 ≅sym : ∀{i} {k l : Lang ∞} (p : l ≅⟨ i ⟩≅ k) → k ≅⟨ i ⟩≅ l
|
|
|
104 ≅ν (≅sym p) = sym (≅ν p)
|
|
|
105 ≅δ (≅sym p) a = ≅sym (≅δ p a)
|
|
|
106
|
|
|
107 ≅trans : ∀{i} {k l m : Lang ∞}
|
|
|
108 ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m
|
|
|
109 ≅ν (≅trans p q) = trans (≅ν p) (≅ν q)
|
|
|
110 ≅δ (≅trans p q) a = ≅trans (≅δ p a) (≅δ q a)
|
|
|
111
|
|
|
112 open import Relation.Binary
|
|
|
113
|
|
|
114 ≅isEquivalence : ∀(i : Size) → IsEquivalence _≅⟨ i ⟩≅_
|
|
|
115 ≅isEquivalence i = record { refl = ≅refl; sym = ≅sym; trans = ≅trans }
|
|
|
116
|
|
|
117 Bis : ∀(i : Size) → Setoid _ _
|
|
|
118 Setoid.Carrier (Bis i) = Lang ∞
|
|
|
119 Setoid._≈_ (Bis i) = _≅⟨ i ⟩≅_
|
|
|
120 Setoid.isEquivalence (Bis i) = ≅isEquivalence i
|
|
|
121
|
|
266
|
122 -- import Relation.Binary.EqReasoning as EqR
|
|
|
123 import Relation.Binary.Reasoning.Setoid as EqR
|
|
46
|
124
|
|
|
125 ≅trans′ : ∀ i (k l m : Lang ∞)
|
|
|
126 ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m
|
|
|
127 ≅trans′ i k l m p q = begin
|
|
|
128 k ≈⟨ p ⟩
|
|
|
129 l ≈⟨ q ⟩
|
|
|
130 m ∎ where open EqR (Bis i)
|
|
|
131
|
|
|
132 open import Data.Bool.Properties
|
|
|
133
|
|
|
134 union-assoc : ∀{i} (k {l m} : Lang ∞) → ((k ∪ l) ∪ m ) ≅⟨ i ⟩≅ ( k ∪ (l ∪ m) )
|
|
|
135 ≅ν (union-assoc k) = ∨-assoc (ν k) _ _
|
|
|
136 ≅δ (union-assoc k) a = union-assoc (δ k a)
|
|
|
137 union-comm : ∀{i} (l k : Lang ∞) → (l ∪ k ) ≅⟨ i ⟩≅ ( k ∪ l )
|
|
|
138 ≅ν (union-comm l k) = ∨-comm (ν l) _
|
|
|
139 ≅δ (union-comm l k) a = union-comm (δ l a) (δ k a)
|
|
|
140 union-idem : ∀{i} (l : Lang ∞) → (l ∪ l ) ≅⟨ i ⟩≅ l
|
|
|
141 ≅ν (union-idem l) = ∨-idem _
|
|
|
142 ≅δ (union-idem l) a = union-idem (δ l a)
|
|
|
143 union-emptyl : ∀{i}{l : Lang ∞} → (∅ ∪ l ) ≅⟨ i ⟩≅ l
|
|
|
144 ≅ν union-emptyl = refl
|
|
|
145 ≅δ union-emptyl a = union-emptyl
|
|
|
146
|
|
|
147 union-cong : ∀{i}{k k′ l l′ : Lang ∞}
|
|
49
|
148 (p : k ≅⟨ i ⟩≅ k′) (q : l ≅⟨ i ⟩≅ l′ ) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l′ )
|
|
46
|
149 ≅ν (union-cong p q) = cong₂ _∨_ (≅ν p) (≅ν q)
|
|
|
150 ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a)
|
|
|
151
|
|
|
152 withExample : (P : Bool → Set) (p : P true) (q : P false) →
|
|
|
153 {A : Set} (g : A → Bool) (x : A) → P (g x)
|
|
|
154 withExample P p q g x with g x
|
|
|
155 ... | true = p
|
|
|
156 ... | false = q
|
|
|
157
|
|
|
158 rewriteExample : {A : Set} {P : A → Set} {x : A} (p : P x)
|
|
|
159 {g : A → A} (e : g x ≡ x) → P (g x)
|
|
|
160 rewriteExample p e rewrite e = p
|
|
|
161
|
|
47
|
162 infixr 6 _∪_
|
|
46
|
163 infixr 7 _·_
|
|
|
164 infix 5 _≅⟨_⟩≅_
|
|
49
|
165
|
|
|
166 union-congl : ∀{i}{k k′ l : Lang ∞}
|
|
|
167 (p : k ≅⟨ i ⟩≅ k′) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l )
|
|
|
168 union-congl eq = union-cong eq ≅refl
|
|
|
169
|
|
|
170 union-congr : ∀{i}{k l l′ : Lang ∞}
|
|
|
171 (p : l ≅⟨ i ⟩≅ l′) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k ∪ l′ )
|
|
|
172 union-congr eq = union-cong ≅refl eq
|
|
|
173
|
|
|
174 union-swap24 : ∀{i} ({x y z w} : Lang ∞) → (x ∪ y) ∪ z ∪ w
|
|
|
175 ≅⟨ i ⟩≅ (x ∪ z) ∪ y ∪ w
|
|
|
176 union-swap24 {_} {x} {y} {z} {w} = begin
|
|
|
177 (x ∪ y) ∪ z ∪ w
|
|
|
178 ≈⟨ union-assoc x ⟩
|
|
|
179 x ∪ y ∪ z ∪ w
|
|
|
180 ≈⟨ union-congr (≅sym ( union-assoc y)) ⟩
|
|
|
181 x ∪ ((y ∪ z) ∪ w)
|
|
|
182 ≈⟨ ≅sym ( union-assoc x ) ⟩
|
|
|
183 (x ∪ ( y ∪ z)) ∪ w
|
|
|
184 ≈⟨ union-congl (union-congr (union-comm y z )) ⟩
|
|
|
185 ( x ∪ (z ∪ y)) ∪ w
|
|
|
186 ≈⟨ union-congl (≅sym ( union-assoc x )) ⟩
|
|
|
187 ((x ∪ z) ∪ y) ∪ w
|
|
|
188 ≈⟨ union-assoc (x ∪ z) ⟩
|
|
|
189 (x ∪ z) ∪ y ∪ w
|
|
|
190 ∎
|
|
|
191 where open EqR (Bis _)
|
|
46
|
192
|
|
|
193 concat-union-distribr : ∀{i} (k {l m} : Lang ∞) → k · ( l ∪ m ) ≅⟨ i ⟩≅ ( k · l ) ∪ ( k · m )
|
|
48
|
194 ≅ν (concat-union-distribr k) = ∧-distribˡ-∨ (ν k) _ _
|
|
46
|
195 ≅δ (concat-union-distribr k) a with ν k
|
|
|
196 ≅δ (concat-union-distribr k {l} {m}) a | true = begin
|
|
47
|
197 δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a)
|
|
51
|
198 ≈⟨ union-congl (concat-union-distribr _) ⟩
|
|
47
|
199 (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a)
|
|
49
|
200 ≈⟨ union-swap24 ⟩
|
|
47
|
201 (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a)
|
|
46
|
202 ∎
|
|
|
203 where open EqR (Bis _)
|
|
|
204 ≅δ (concat-union-distribr k) a | false = concat-union-distribr (δ k a)
|
|
|
205
|
|
50
|
206 concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m )
|
|
|
207 ≅ν (concat-union-distribl k {l} {m}) = ∧-distribʳ-∨ _ (ν k) _
|
|
|
208 ≅δ (concat-union-distribl k {l} {m}) a with ν k | ν l
|
|
|
209 ≅δ (concat-union-distribl k {l} {m}) a | false | false = concat-union-distribl (δ k a)
|
|
|
210 ≅δ (concat-union-distribl k {l} {m}) a | false | true = begin
|
|
|
211 (if false ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m)
|
|
|
212 ≈⟨ ≅refl ⟩
|
|
51
|
213 ((δ k a ∪ δ l a) · m ) ∪ δ m a
|
|
|
214 ≈⟨ union-congl (concat-union-distribl _) ⟩
|
|
|
215 (δ k a · m ∪ δ l a · m) ∪ δ m a
|
|
|
216 ≈⟨ union-assoc _ ⟩
|
|
|
217 (δ k a · m) ∪ ( δ l a · m ∪ δ m a )
|
|
50
|
218 ≈⟨ ≅refl ⟩
|
|
|
219 (if false then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m)
|
|
|
220 ∎
|
|
|
221 where open EqR (Bis _)
|
|
|
222 ≅δ (concat-union-distribl k {l} {m}) a | true | false = begin
|
|
52
|
223 (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
|
|
|
224 ((δ k a ∪ δ l a) · m ) ∪ δ m a ≈⟨ union-congl (concat-union-distribl _) ⟩
|
|
|
225 (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨ union-assoc _ ⟩
|
|
|
226 δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨ union-congr ( union-comm _ _) ⟩
|
|
|
227 δ k a · m ∪ δ m a ∪ δ l a · m ≈⟨ ≅sym ( union-assoc _ ) ⟩
|
|
|
228 (δ k a · m ∪ δ m a) ∪ δ l a · m ≈⟨ ≅refl ⟩
|
|
50
|
229 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if false then δ l a · m ∪ δ m a else δ l a · m))
|
|
|
230 ∎
|
|
|
231 where open EqR (Bis _)
|
|
|
232 ≅δ (concat-union-distribl k {l} {m}) a | true | true = begin
|
|
52
|
233 (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
|
|
|
234 (δ k a ∪ δ l a) · m ∪ δ m a ≈⟨ union-congl ( concat-union-distribl _ ) ⟩
|
|
|
235 (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨ union-assoc _ ⟩
|
|
|
236 δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨ ≅sym ( union-congr ( union-congr ( union-idem _ ) ) ) ⟩
|
|
|
237 δ k a · m ∪ ( δ l a · m ∪ (δ m a ∪ δ m a) ) ≈⟨ ≅sym ( union-congr ( union-assoc _ )) ⟩
|
|
|
238 δ k a · m ∪ ( (δ l a · m ∪ δ m a ) ∪ δ m a ) ≈⟨ union-congr ( union-congl ( union-comm _ _) ) ⟩
|
|
|
239 δ k a · m ∪ ( (δ m a ∪ δ l a · m ) ∪ δ m a ) ≈⟨ ≅sym ( union-assoc _ ) ⟩
|
|
|
240 ( δ k a · m ∪ (δ m a ∪ δ l a · m )) ∪ δ m a ≈⟨ ≅sym ( union-congl ( union-assoc _ ) ) ⟩
|
|
|
241 ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a ≈⟨ union-assoc _ ⟩
|
|
|
242 (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a ≈⟨ ≅refl ⟩
|
|
|
243 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m))
|
|
50
|
244 ∎
|
|
|
245 where open EqR (Bis _)
|
|
|
246
|
|
47
|
247 postulate
|
|
|
248 concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅
|
|
|
249 concat-emptyr : ∀{i} l → l · ∅ ≅⟨ i ⟩≅ ∅
|
|
|
250 concat-unitl : ∀{i} l → ε · l ≅⟨ i ⟩≅ l
|
|
|
251 concat-unitr : ∀{i} l → l · ε ≅⟨ i ⟩≅ l
|
|
|
252 star-empty : ∀{i} → ∅ * ≅⟨ i ⟩≅ ε
|
|
46
|
253
|
|
49
|
254 concat-congl : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → l · m ≅⟨ i ⟩≅ k · m
|
|
|
255 ≅ν (concat-congl {i} {m} p ) = cong (λ x → x ∧ ( ν m )) ( ≅ν p )
|
|
|
256 ≅δ (concat-congl {i} {m} {l} {k} p ) a with ν k | ν l | ≅ν p
|
|
|
257 ≅δ (concat-congl {i} {m} {l} {k} p) a | false | false | refl = concat-congl (≅δ p a)
|
|
|
258 ≅δ (concat-congl {i} {m} {l} {k} p) a | true | true | refl = union-congl (concat-congl (≅δ p a))
|
|
|
259
|
|
|
260 concat-congr : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → m · l ≅⟨ i ⟩≅ m · k
|
|
|
261 ≅ν (concat-congr {i} {m} {_} {k} p ) = cong (λ x → ( ν m ) ∧ x ) ( ≅ν p )
|
|
|
262 ≅δ (concat-congr {i} {m} {l} {k} p ) a with ν m | ν k | ν l | ≅ν p
|
|
|
263 ≅δ (concat-congr {i} {m} {l} {k} p) a | false | x | .x | refl = concat-congr p
|
|
|
264 ≅δ (concat-congr {i} {m} {l} {k} p) a | true | x | .x | refl = union-cong (concat-congr p ) ( ≅δ p a )
|
|
|
265
|
|
|
266 concat-assoc : ∀{i} (k {l m} : Lang ∞) → (k · l) · m ≅⟨ i ⟩≅ k · (l · m)
|
|
|
267 ≅ν (concat-assoc {i} k {l} {m} ) = ∧-assoc ( ν k ) ( ν l ) ( ν m )
|
|
|
268 ≅δ (concat-assoc {i} k {l} {m} ) a with ν k
|
|
51
|
269 ≅δ (concat-assoc {i} k {l} {m}) a | false = concat-assoc _
|
|
49
|
270 ≅δ (concat-assoc {i} k {l} {m}) a | true with ν l
|
|
|
271 ≅δ (concat-assoc {i} k {l} {m}) a | true | false = begin
|
|
|
272 ( if false then (δ k a · l ∪ δ l a) · m ∪ δ m a else (δ k a · l ∪ δ l a) · m )
|
|
|
273 ≈⟨ ≅refl ⟩
|
|
|
274 (δ k a · l ∪ δ l a) · m
|
|
51
|
275 ≈⟨ concat-union-distribl _ ⟩
|
|
49
|
276 ((δ k a · l) · m ) ∪ ( δ l a · m )
|
|
51
|
277 ≈⟨ union-congl (concat-assoc _) ⟩
|
|
49
|
278 (δ k a · l · m ) ∪ ( δ l a · m )
|
|
|
279 ≈⟨ ≅refl ⟩
|
|
|
280 δ k a · l · m ∪ (if false then δ l a · m ∪ δ m a else δ l a · m)
|
|
|
281 ∎ where open EqR (Bis _)
|
|
|
282 ≅δ (concat-assoc {i} k {l} {m}) a | true | true = begin
|
|
|
283 (if true then (δ k a · l ∪ δ l a) · m ∪ δ m a else (δ k a · l ∪ δ l a) · m)
|
|
|
284 ≈⟨ ≅refl ⟩
|
|
|
285 ((( δ k a · l ) ∪ δ l a) · m ) ∪ δ m a
|
|
51
|
286 ≈⟨ union-congl (concat-union-distribl _ ) ⟩
|
|
49
|
287 ((δ k a · l) · m ∪ ( δ l a · m )) ∪ δ m a
|
|
51
|
288 ≈⟨ union-congl ( union-congl (concat-assoc _)) ⟩
|
|
49
|
289 (( δ k a · l · m ) ∪ ( δ l a · m )) ∪ δ m a
|
|
51
|
290 ≈⟨ union-assoc _ ⟩
|
|
49
|
291 ( δ k a · l · m ) ∪ ( ( δ l a · m ) ∪ δ m a )
|
|
|
292 ≈⟨ ≅refl ⟩
|
|
|
293 δ k a · l · m ∪ (if true then δ l a · m ∪ δ m a else δ l a · m)
|
|
|
294 ∎ where open EqR (Bis _)
|
|
|
295
|
|
46
|
296 star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l *
|
|
|
297 ≅ν (star-concat-idem l) = refl
|
|
|
298 ≅δ (star-concat-idem l) a = begin
|
|
52
|
299 δ ((l *) · (l *)) a ≈⟨ union-congl (concat-assoc _) ⟩
|
|
|
300 δ l a · (l * · l *) ∪ δ l a · l * ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩
|
|
|
301 δ l a · l * ∪ δ l a · l * ≈⟨ union-idem _ ⟩
|
|
|
302 δ (l *) a ∎ where open EqR (Bis _)
|
|
46
|
303
|
|
|
304 star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l *
|
|
|
305 ≅ν (star-idem l) = refl
|
|
|
306 ≅δ (star-idem l) a = begin
|
|
47
|
307 δ ((l *) *) a ≈⟨ concat-assoc (δ l a) ⟩
|
|
48
|
308 δ l a · ((l *) · ((l *) *)) ≈⟨ concat-congr ( concat-congr (star-idem l )) ⟩
|
|
|
309 δ l a · ((l *) · (l *)) ≈⟨ concat-congr (star-concat-idem l ) ⟩
|
|
47
|
310 δ l a · l *
|
|
46
|
311 ∎ where open EqR (Bis _)
|
|
|
312
|
|
47
|
313 postulate
|
|
|
314 star-rec : ∀{i} (l : Lang ∞) → l * ≅⟨ i ⟩≅ ε ∪ (l · l *)
|
|
46
|
315
|
|
|
316 star-from-rec : ∀{i} (k {l m} : Lang ∞)
|
|
|
317 → ν k ≡ false
|
|
|
318 → l ≅⟨ i ⟩≅ k · l ∪ m
|
|
|
319 → l ≅⟨ i ⟩≅ k * · m
|
|
|
320 ≅ν (star-from-rec k n p) with ≅ν p
|
|
47
|
321 ... | b rewrite n = b
|
|
46
|
322 ≅δ (star-from-rec k {l} {m} n p) a with ≅δ p a
|
|
|
323 ... | q rewrite n = begin
|
|
|
324 (δ l a)
|
|
47
|
325 ≈⟨ q ⟩
|
|
|
326 δ k a · l ∪ δ m a
|
|
49
|
327 ≈⟨ union-congl (concat-congr (star-from-rec k {l} {m} n p)) ⟩
|
|
47
|
328 (δ k a · (k * · m) ∪ δ m a)
|
|
51
|
329 ≈⟨ union-congl (≅sym (concat-assoc _)) ⟩
|
|
47
|
330 (δ k a · (k *)) · m ∪ δ m a
|
|
46
|
331 ∎ where open EqR (Bis _)
|
|
|
332
|
|
|
333
|
|
|
334 open List
|
|
|
335
|
|
|
336 record DA (S : Set) : Set where
|
|
|
337 field ν : (s : S) → Bool
|
|
|
338 δ : (s : S)(a : A) → S
|
|
|
339 νs : ∀{i} (ss : List.List i S) → Bool
|
|
|
340 νs ss = List.any ν ss
|
|
|
341 δs : ∀{i} (ss : List.List i S) (a : A) → List.List i S
|
|
|
342 δs ss a = List.map (λ s → δ s a) ss
|
|
|
343
|
|
|
344 open Lang
|
|
|
345
|
|
|
346 lang : ∀{i} {S} (da : DA S) (s : S) → Lang i
|
|
|
347 Lang.ν (lang da s) = DA.ν da s
|
|
|
348 Lang.δ (lang da s) a = lang da (DA.δ da s a)
|
|
|
349
|
|
|
350 open import Data.Unit hiding ( _≟_ )
|
|
|
351
|
|
|
352 open DA
|
|
|
353
|
|
|
354 ∅A : DA ⊤
|
|
|
355 ν ∅A s = false
|
|
|
356 δ ∅A s a = s
|
|
|
357
|
|
|
358 εA : DA Bool
|
|
|
359 ν εA b = b
|
|
|
360 δ εA b a = false
|
|
|
361
|
|
|
362 open import Relation.Nullary.Decidable
|
|
|
363
|
|
|
364 data 3States : Set where
|
|
|
365 init acc err : 3States
|
|
|
366
|
|
|
367 charA : (a : A) → DA 3States
|
|
|
368 ν (charA a) init = false
|
|
|
369 ν (charA a) acc = true
|
|
|
370 ν (charA a) err = false
|
|
|
371 δ (charA a) init x =
|
|
|
372 if ⌊ a ≟ x ⌋ then acc else err
|
|
|
373 δ (charA a) acc x = err
|
|
|
374 δ (charA a) err x = err
|
|
|
375
|
|
|
376
|
|
|
377 complA : ∀{S} (da : DA S) → DA S
|
|
|
378 ν (complA da) s = not (ν da s)
|
|
|
379 δ (complA da) s a = δ da s a
|
|
|
380
|
|
|
381 open import Data.Product
|
|
|
382
|
|
|
383 _⊕_ : ∀{S1 S2} (da1 : DA S1) (da2 : DA S2) → DA (S1 × S2)
|
|
|
384 ν (da1 ⊕ da2) (s1 , s2) = ν da1 s1 ∨ ν da2 s2
|
|
|
385 δ (da1 ⊕ da2) (s1 , s2) a = δ da1 s1 a , δ da2 s2 a
|
|
|
386
|
|
|
387 powA : ∀{S} (da : DA S) → DA (List ∞ S)
|
|
|
388 ν (powA da) ss = νs da ss
|
|
|
389 δ (powA da) ss a = δs da ss a
|
|
|
390
|
|
|
391 open _≅⟨_⟩≅_
|
|
|
392
|
|
|
393 powA-nil : ∀{i S} (da : DA S) → lang (powA da) [] ≅⟨ i ⟩≅ ∅
|
|
|
394 ≅ν (powA-nil da) = refl
|
|
|
395 ≅δ (powA-nil da) a = powA-nil da
|
|
|
396
|
|
|
397 powA-cons : ∀{i S} (da : DA S) {s : S} {ss : List ∞ S} →
|
|
|
398 lang (powA da) (s ∷ ss) ≅⟨ i ⟩≅ lang da s ∪ lang (powA da) ss
|
|
|
399 ≅ν (powA-cons da) = refl
|
|
|
400 ≅δ (powA-cons da) a = powA-cons da
|
|
|
401
|
|
|
402 composeA : ∀{S1 S2} (da1 : DA S1)(s2 : S2)(da2 : DA S2) → DA (S1 × List ∞ S2)
|
|
47
|
403 ν (composeA da1 s2 da2) (s1 , ss2) = (ν da1 s1 ∧ ν da2 s2) ∨ νs da2 ss2
|
|
46
|
404 δ (composeA da1 s2 da2) (s1 , ss2) a =
|
|
47
|
405 δ da1 s1 a , δs da2 (if ν da1 s1 then s2 ∷ ss2 else ss2) a
|
|
46
|
406
|
|
266
|
407 -- import Relation.Binary.EqReasoning as EqR
|
|
|
408 import Relation.Binary.Reasoning.Setoid as EqR
|
|
46
|
409
|
|
|
410 composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : List ∞ S2) →
|
|
|
411 lang (composeA da1 s2 da2) (s1 , ss) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 ∪ lang (powA da2) ss
|
|
47
|
412 ≅ν (composeA-gen da1 da2 s1 s2 ss) = refl
|
|
46
|
413 ≅δ (composeA-gen da1 da2 s1 s2 ss) a with ν da1 s1
|
|
47
|
414 ... | false = composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 ss a)
|
|
46
|
415 ... | true = begin
|
|
47
|
416 lang (composeA da1 s2 da2) (δ da1 s1 a , δ da2 s2 a ∷ δs da2 ss a)
|
|
|
417 ≈⟨ composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 (s2 ∷ ss) a) ⟩
|
|
|
418 lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang (powA da2) (δs da2 (s2 ∷ ss) a)
|
|
49
|
419 ≈⟨ union-congr (powA-cons da2) ⟩
|
|
48
|
420 lang da1 (δ da1 s1 a) · lang da2 s2 ∪
|
|
|
421 (lang da2 (δ da2 s2 a) ∪ lang (powA da2) (δs da2 ss a))
|
|
|
422 ≈⟨ ≅sym (union-assoc _) ⟩
|
|
47
|
423 (lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang da2 (δ da2 s2 a)) ∪ lang (powA da2) (δs da2 ss a)
|
|
46
|
424 ∎ where open EqR (Bis _)
|
|
|
425
|
|
47
|
426 postulate
|
|
|
427 composeA-correct : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) s1 s2 →
|
|
46
|
428 lang (composeA da1 s2 da2) (s1 , []) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2
|
|
|
429
|
|
|
430
|
|
|
431 open import Data.Maybe
|
|
|
432
|
|
|
433 acceptingInitial : ∀{S} (s0 : S) (da : DA S) → DA (Maybe S)
|
|
|
434 ν (acceptingInitial s0 da) (just s) = ν da s
|
|
|
435 δ (acceptingInitial s0 da) (just s) a = just (δ da s a)
|
|
|
436 ν (acceptingInitial s0 da) nothing = true
|
|
|
437 δ (acceptingInitial s0 da) nothing a = just (δ da s0 a)
|
|
|
438
|
|
|
439
|
|
|
440
|
|
|
441 finalToInitial : ∀{S} (da : DA (Maybe S)) → DA (List ∞ (Maybe S))
|
|
|
442 ν (finalToInitial da) ss = νs da ss
|
|
|
443 δ (finalToInitial da) ss a =
|
|
|
444 let ss′ = δs da ss a
|
|
|
445 in if νs da ss then δ da nothing a ∷ ss′ else ss′
|
|
|
446
|
|
|
447
|
|
|
448 starA : ∀{S}(s0 : S)(da : DA S) → DA (List ∞(Maybe S))
|
|
|
449 starA s0 da = finalToInitial (acceptingInitial s0 da)
|
|
|
450
|
|
|
451
|
|
47
|
452 postulate
|
|
|
453 acceptingInitial-just : ∀{i S} (s0 : S) (da : DA S) {s : S} →
|
|
46
|
454 lang (acceptingInitial s0 da) (just s) ≅⟨ i ⟩≅ lang da s
|
|
47
|
455 acceptingInitial-nothing : ∀{i S} (s0 : S) (da : DA S) →
|
|
46
|
456 lang (acceptingInitial s0 da) nothing ≅⟨ i ⟩≅ ε ∪ lang da s0
|
|
47
|
457 starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : List ∞ (Maybe S))→
|
|
46
|
458 lang (starA s0 da) ss ≅⟨ i ⟩≅
|
|
|
459 lang (powA (acceptingInitial s0 da)) ss · (lang da s0) *
|
|
47
|
460 starA-correct : ∀{i S} (da : DA S) (s0 : S) →
|
|
|
461 lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *
|
|
46
|
462
|
|
52
|
463 record NAutomaton ( Q : Set ) ( Σ : Set )
|
|
|
464 : Set where
|
|
|
465 field
|
|
|
466 Nδ : Q → Σ → Q → Bool
|
|
|
467 Nstart : Q → Bool
|
|
|
468 Nend : Q → Bool
|
|
|
469
|
|
|
470 postulate
|
|
|
471 exists : { S : Set} → ( S → Bool ) → Bool
|
|
|
472
|
|
|
473 nlang : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
|
|
|
474 Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x ))
|
|
|
475 Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x)
|
|
|
476
|
|
119
|
477 nlang1 : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
|
|
|
478 Lang.ν (nlang1 nfa s) = NAutomaton.Nend nfa {!!}
|
|
|
479 Lang.δ (nlang1 nfa s) a = nlang1 nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x)
|
|
|
480
|
|
52
|
481 -- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i
|
|
|
482 -- Lang.ν (nlang' nfa s) = DA.ν nfa s
|
|
|
483 -- Lang.δ (nlang' nfa s) a = nlang' nfa (DA.δ nfa s a)
|
|
|
484
|
