|
46
|
1 open import Relation.Nullary
|
|
|
2 open import Relation.Binary.PropositionalEquality
|
|
|
3 module flcagl
|
|
|
4 (A : Set)
|
|
|
5 ( _≟_ : (a b : A) → Dec ( a ≡ b ) ) where
|
|
|
6
|
|
|
7 open import Data.Bool hiding ( _≟_ )
|
|
|
8 -- open import Data.Maybe
|
|
|
9 open import Level renaming ( zero to Zero ; suc to succ )
|
|
|
10 open import Size
|
|
|
11
|
|
|
12 module List where
|
|
|
13
|
|
|
14 data List (i : Size) (A : Set) : Set where
|
|
|
15 [] : List i A
|
|
|
16 _∷_ : {j : Size< i} (x : A) (xs : List j A) → List i A
|
|
|
17
|
|
|
18
|
|
|
19 map : ∀{i A B} → (A → B) → List i A → List i B
|
|
|
20 map f [] = []
|
|
|
21 map f ( x ∷ xs)= f x ∷ map f xs
|
|
|
22
|
|
|
23 foldr : ∀{i} {A B : Set} → (A → B → B) → B → List i A → B
|
|
|
24 foldr c n [] = n
|
|
|
25 foldr c n (x ∷ xs) = c x (foldr c n xs)
|
|
|
26
|
|
|
27 any : ∀{i A} → (A → Bool) → List i A → Bool
|
|
|
28 any p xs = foldr _∨_ false (map p xs)
|
|
|
29
|
|
|
30 module Lang where
|
|
|
31
|
|
|
32 open List
|
|
|
33
|
|
|
34 record Lang (i : Size) : Set where
|
|
|
35 coinductive
|
|
|
36 field
|
|
|
37 ν : Bool
|
|
|
38 δ : ∀{j : Size< i} → A → Lang j
|
|
|
39
|
|
|
40 open Lang
|
|
|
41
|
|
|
42 _∋_ : ∀{i} → Lang i → List i A → Bool
|
|
|
43 l ∋ [] = ν l
|
|
|
44 l ∋ ( a ∷ as ) = δ l a ∋ as
|
|
|
45
|
|
|
46 trie : ∀{i} (f : List i A → Bool) → Lang i
|
|
|
47 ν (trie f) = f []
|
|
|
48 δ (trie f) a = trie (λ as → f (a ∷ as))
|
|
|
49
|
|
|
50 ∅ : ∀{i} → Lang i
|
|
|
51 ν ∅ = false
|
|
|
52 δ ∅ x = ∅
|
|
|
53
|
|
|
54 ε : ∀{i} → Lang i
|
|
|
55 ν ε = true
|
|
|
56 δ ε x = ∅
|
|
|
57
|
|
|
58 open import Relation.Nullary.Decidable
|
|
|
59
|
|
|
60 char : ∀{i} (a : A) → Lang i
|
|
|
61 ν (char a) = false
|
|
|
62 δ (char a) x = if ⌊ a ≟ x ⌋ then ε else ∅
|
|
|
63
|
|
|
64 compl : ∀{i} (l : Lang i) → Lang i
|
|
|
65 ν (compl l) = not (ν l)
|
|
|
66 δ (compl l) x = compl (δ l x)
|
|
|
67
|
|
|
68
|
|
|
69 _∪_ : ∀{i} (k l : Lang i) → Lang i
|
|
|
70 ν (k ∪ l) = ν k ∨ ν l
|
|
|
71 δ (k ∪ l) x = δ k x ∪ δ l x
|
|
|
72
|
|
|
73
|
|
|
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
|
|
|
80 δ (_·_ {i} k l) {j} x =
|
|
|
81 let
|
|
|
82 k′l : Lang j
|
|
|
83 k′l = _·_ {j} (δ k {j} x) l
|
|
|
84 in if ν k then _∪_ {j} k′l (δ l {j} x) else k′l
|
|
|
85
|
|
|
86 _* : ∀{i} (l : Lang i) → Lang i
|
|
|
87 ν (l *) = true
|
|
|
88 δ (l *) x = δ l x · (l *)
|
|
|
89
|
|
|
90 record _≅⟨_⟩≅_ (l : Lang ∞ ) i (k : Lang ∞) : Set where
|
|
|
91 coinductive
|
|
|
92 field ≅ν : ν l ≡ ν k
|
|
|
93 ≅δ : ∀ {j : Size< i } (a : A ) → δ l a ≅⟨ j ⟩≅ δ k a
|
|
|
94
|
|
|
95 open _≅⟨_⟩≅_
|
|
|
96
|
|
|
97 ≅refl : ∀{i} {l : Lang ∞} → l ≅⟨ i ⟩≅ l
|
|
|
98 ≅ν ≅refl = refl
|
|
|
99 ≅δ ≅refl a = ≅refl
|
|
|
100
|
|
|
101
|
|
|
102 ≅sym : ∀{i} {k l : Lang ∞} (p : l ≅⟨ i ⟩≅ k) → k ≅⟨ i ⟩≅ l
|
|
|
103 ≅ν (≅sym p) = sym (≅ν p)
|
|
|
104 ≅δ (≅sym p) a = ≅sym (≅δ p a)
|
|
|
105
|
|
|
106 ≅trans : ∀{i} {k l m : Lang ∞}
|
|
|
107 ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m
|
|
|
108 ≅ν (≅trans p q) = trans (≅ν p) (≅ν q)
|
|
|
109 ≅δ (≅trans p q) a = ≅trans (≅δ p a) (≅δ q a)
|
|
|
110
|
|
|
111 open import Relation.Binary
|
|
|
112
|
|
|
113 ≅isEquivalence : ∀(i : Size) → IsEquivalence _≅⟨ i ⟩≅_
|
|
|
114 ≅isEquivalence i = record { refl = ≅refl; sym = ≅sym; trans = ≅trans }
|
|
|
115
|
|
|
116 Bis : ∀(i : Size) → Setoid _ _
|
|
|
117 Setoid.Carrier (Bis i) = Lang ∞
|
|
|
118 Setoid._≈_ (Bis i) = _≅⟨ i ⟩≅_
|
|
|
119 Setoid.isEquivalence (Bis i) = ≅isEquivalence i
|
|
|
120
|
|
|
121 import Relation.Binary.EqReasoning as EqR
|
|
|
122
|
|
|
123 ≅trans′ : ∀ i (k l m : Lang ∞)
|
|
|
124 ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m
|
|
|
125 ≅trans′ i k l m p q = begin
|
|
|
126 k ≈⟨ p ⟩
|
|
|
127 l ≈⟨ q ⟩
|
|
|
128 m ∎ where open EqR (Bis i)
|
|
|
129
|
|
|
130 open import Data.Bool.Properties
|
|
|
131
|
|
|
132 union-assoc : ∀{i} (k {l m} : Lang ∞) → ((k ∪ l) ∪ m ) ≅⟨ i ⟩≅ ( k ∪ (l ∪ m) )
|
|
|
133 ≅ν (union-assoc k) = ∨-assoc (ν k) _ _
|
|
|
134 ≅δ (union-assoc k) a = union-assoc (δ k a)
|
|
|
135 union-comm : ∀{i} (l k : Lang ∞) → (l ∪ k ) ≅⟨ i ⟩≅ ( k ∪ l )
|
|
|
136 ≅ν (union-comm l k) = ∨-comm (ν l) _
|
|
|
137 ≅δ (union-comm l k) a = union-comm (δ l a) (δ k a)
|
|
|
138 union-idem : ∀{i} (l : Lang ∞) → (l ∪ l ) ≅⟨ i ⟩≅ l
|
|
|
139 ≅ν (union-idem l) = ∨-idem _
|
|
|
140 ≅δ (union-idem l) a = union-idem (δ l a)
|
|
|
141 union-emptyl : ∀{i}{l : Lang ∞} → (∅ ∪ l ) ≅⟨ i ⟩≅ l
|
|
|
142 ≅ν union-emptyl = refl
|
|
|
143 ≅δ union-emptyl a = union-emptyl
|
|
|
144
|
|
|
145 union-cong : ∀{i}{k k′ l l′ : Lang ∞}
|
|
|
146 (p : k ≅⟨ i ⟩≅ k′)(q : l ≅⟨ i ⟩≅ l′ ) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l′ )
|
|
|
147 ≅ν (union-cong p q) = cong₂ _∨_ (≅ν p) (≅ν q)
|
|
|
148 ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a)
|
|
|
149
|
|
|
150 -- union-union-distr : ∀{i} (k {l m} : Lang ∞) → ( ( k ∪ l ) ∪ m ) ≅⟨ i ⟩≅ ( ( k ∪ m ) ∪ ( l ∪ m ) )
|
|
|
151 -- ≅ν (union-union-distr k) = {!!}
|
|
|
152 -- ≅δ (union-union-distr k) a = {!!}
|
|
|
153
|
|
|
154
|
|
|
155 withExample : (P : Bool → Set) (p : P true) (q : P false) →
|
|
|
156 {A : Set} (g : A → Bool) (x : A) → P (g x)
|
|
|
157 withExample P p q g x with g x
|
|
|
158 ... | true = p
|
|
|
159 ... | false = q
|
|
|
160
|
|
|
161 rewriteExample : {A : Set} {P : A → Set} {x : A} (p : P x)
|
|
|
162 {g : A → A} (e : g x ≡ x) → P (g x)
|
|
|
163 rewriteExample p e rewrite e = p
|
|
|
164
|
|
47
|
165 infixr 6 _∪_
|
|
46
|
166 infixr 7 _·_
|
|
|
167 infix 5 _≅⟨_⟩≅_
|
|
47
|
168 postulate
|
|
|
169 concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m )
|
|
46
|
170
|
|
|
171 union-swap24 : {!!}
|
|
|
172 union-swap24 = {!!}
|
|
|
173
|
|
|
174 concat-union-distribr : ∀{i} (k {l m} : Lang ∞) → k · ( l ∪ m ) ≅⟨ i ⟩≅ ( k · l ) ∪ ( k · m )
|
|
47
|
175 ≅ν (concat-union-distribr k) = {!!} -- ∧-distribʳ-∨ (ν k) _ _
|
|
46
|
176 ≅δ (concat-union-distribr k) a with ν k
|
|
|
177 ≅δ (concat-union-distribr k {l} {m}) a | true = begin
|
|
47
|
178 δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a)
|
|
|
179 -- ≈⟨ union-cong (concat-union-distribr (δ k a)) ⟩
|
|
46
|
180 ≈⟨ {!!} ⟩
|
|
47
|
181 (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a)
|
|
|
182 ≈⟨ {!!} ⟩
|
|
|
183 (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a)
|
|
46
|
184 ∎
|
|
|
185 where open EqR (Bis _)
|
|
|
186 ≅δ (concat-union-distribr k) a | false = concat-union-distribr (δ k a)
|
|
|
187
|
|
47
|
188 postulate
|
|
|
189 concat-congl : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → l · m ≅⟨ i ⟩≅ k · m
|
|
|
190 concat-congr : ∀{i} {m l k : Lang ∞} → l ≅⟨ i ⟩≅ k → m · l ≅⟨ i ⟩≅ m · k
|
|
|
191 concat-assoc : ∀{i} (k {l m} : Lang ∞) → (k · l) · m ≅⟨ i ⟩≅ k · (l · m)
|
|
|
192 concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅
|
|
|
193 concat-emptyr : ∀{i} l → l · ∅ ≅⟨ i ⟩≅ ∅
|
|
|
194 concat-unitl : ∀{i} l → ε · l ≅⟨ i ⟩≅ l
|
|
|
195 concat-unitr : ∀{i} l → l · ε ≅⟨ i ⟩≅ l
|
|
|
196 star-empty : ∀{i} → ∅ * ≅⟨ i ⟩≅ ε
|
|
46
|
197
|
|
|
198 star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l *
|
|
|
199 ≅ν (star-concat-idem l) = refl
|
|
|
200 ≅δ (star-concat-idem l) a = begin
|
|
47
|
201 δ ((l *) · (l *)) a
|
|
|
202 ≈⟨ union-cong (concat-assoc _) ≅refl ⟩
|
|
|
203 δ l a · (l * · l *) ∪ δ l a · l *
|
|
|
204 ≈⟨ union-cong (concat-congr (star-concat-idem _)) ≅refl ⟩
|
|
|
205 δ l a · l * ∪ δ l a · l *
|
|
|
206 ≈⟨ union-idem _ ⟩
|
|
|
207 δ (l *) a
|
|
46
|
208 ∎ where open EqR (Bis _)
|
|
|
209
|
|
|
210 star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l *
|
|
|
211 ≅ν (star-idem l) = refl
|
|
|
212 ≅δ (star-idem l) a = begin
|
|
47
|
213 δ ((l *) *) a ≈⟨ concat-assoc (δ l a) ⟩
|
|
|
214 δ l a · (l *) · ((l *) *) ≈⟨ {!!} ⟩
|
|
|
215 δ l a · l * · l * ≈⟨ {!!} ⟩
|
|
|
216 δ l a · ((l *) *) ≈⟨ concat-congr (star-idem l) ⟩
|
|
|
217 δ l a · l *
|
|
46
|
218 ∎ where open EqR (Bis _)
|
|
|
219
|
|
47
|
220 postulate
|
|
|
221 star-rec : ∀{i} (l : Lang ∞) → l * ≅⟨ i ⟩≅ ε ∪ (l · l *)
|
|
46
|
222
|
|
|
223 star-from-rec : ∀{i} (k {l m} : Lang ∞)
|
|
|
224 → ν k ≡ false
|
|
|
225 → l ≅⟨ i ⟩≅ k · l ∪ m
|
|
|
226 → l ≅⟨ i ⟩≅ k * · m
|
|
|
227 ≅ν (star-from-rec k n p) with ≅ν p
|
|
47
|
228 ... | b rewrite n = b
|
|
46
|
229 ≅δ (star-from-rec k {l} {m} n p) a with ≅δ p a
|
|
|
230 ... | q rewrite n = begin
|
|
|
231 (δ l a)
|
|
47
|
232 ≈⟨ q ⟩
|
|
|
233 δ k a · l ∪ δ m a
|
|
|
234 ≈⟨ union-cong (concat-congr (star-from-rec k {l} {m} n p)) ≅refl ⟩
|
|
|
235 (δ k a · (k * · m) ∪ δ m a)
|
|
|
236 ≈⟨ union-cong (≅sym (concat-assoc (δ k a))) ≅refl ⟩
|
|
|
237 (δ k a · (k *)) · m ∪ δ m a
|
|
46
|
238 ∎ where open EqR (Bis _)
|
|
|
239
|
|
|
240
|
|
|
241 open List
|
|
|
242
|
|
|
243 record DA (S : Set) : Set where
|
|
|
244 field ν : (s : S) → Bool
|
|
|
245 δ : (s : S)(a : A) → S
|
|
|
246 νs : ∀{i} (ss : List.List i S) → Bool
|
|
|
247 νs ss = List.any ν ss
|
|
|
248 δs : ∀{i} (ss : List.List i S) (a : A) → List.List i S
|
|
|
249 δs ss a = List.map (λ s → δ s a) ss
|
|
|
250
|
|
|
251 open Lang
|
|
|
252
|
|
|
253 lang : ∀{i} {S} (da : DA S) (s : S) → Lang i
|
|
|
254 Lang.ν (lang da s) = DA.ν da s
|
|
|
255 Lang.δ (lang da s) a = lang da (DA.δ da s a)
|
|
|
256
|
|
|
257 open import Data.Unit hiding ( _≟_ )
|
|
|
258
|
|
|
259 open DA
|
|
|
260
|
|
|
261 ∅A : DA ⊤
|
|
|
262 ν ∅A s = false
|
|
|
263 δ ∅A s a = s
|
|
|
264
|
|
|
265 εA : DA Bool
|
|
|
266 ν εA b = b
|
|
|
267 δ εA b a = false
|
|
|
268
|
|
|
269 open import Relation.Nullary.Decidable
|
|
|
270
|
|
|
271 data 3States : Set where
|
|
|
272 init acc err : 3States
|
|
|
273
|
|
|
274 charA : (a : A) → DA 3States
|
|
|
275 ν (charA a) init = false
|
|
|
276 ν (charA a) acc = true
|
|
|
277 ν (charA a) err = false
|
|
|
278 δ (charA a) init x =
|
|
|
279 if ⌊ a ≟ x ⌋ then acc else err
|
|
|
280 δ (charA a) acc x = err
|
|
|
281 δ (charA a) err x = err
|
|
|
282
|
|
|
283
|
|
|
284 complA : ∀{S} (da : DA S) → DA S
|
|
|
285 ν (complA da) s = not (ν da s)
|
|
|
286 δ (complA da) s a = δ da s a
|
|
|
287
|
|
|
288 open import Data.Product
|
|
|
289
|
|
|
290 _⊕_ : ∀{S1 S2} (da1 : DA S1) (da2 : DA S2) → DA (S1 × S2)
|
|
|
291 ν (da1 ⊕ da2) (s1 , s2) = ν da1 s1 ∨ ν da2 s2
|
|
|
292 δ (da1 ⊕ da2) (s1 , s2) a = δ da1 s1 a , δ da2 s2 a
|
|
|
293
|
|
|
294 powA : ∀{S} (da : DA S) → DA (List ∞ S)
|
|
|
295 ν (powA da) ss = νs da ss
|
|
|
296 δ (powA da) ss a = δs da ss a
|
|
|
297
|
|
|
298 open _≅⟨_⟩≅_
|
|
|
299
|
|
|
300 powA-nil : ∀{i S} (da : DA S) → lang (powA da) [] ≅⟨ i ⟩≅ ∅
|
|
|
301 ≅ν (powA-nil da) = refl
|
|
|
302 ≅δ (powA-nil da) a = powA-nil da
|
|
|
303
|
|
|
304 powA-cons : ∀{i S} (da : DA S) {s : S} {ss : List ∞ S} →
|
|
|
305 lang (powA da) (s ∷ ss) ≅⟨ i ⟩≅ lang da s ∪ lang (powA da) ss
|
|
|
306 ≅ν (powA-cons da) = refl
|
|
|
307 ≅δ (powA-cons da) a = powA-cons da
|
|
|
308
|
|
|
309 composeA : ∀{S1 S2} (da1 : DA S1)(s2 : S2)(da2 : DA S2) → DA (S1 × List ∞ S2)
|
|
47
|
310 ν (composeA da1 s2 da2) (s1 , ss2) = (ν da1 s1 ∧ ν da2 s2) ∨ νs da2 ss2
|
|
46
|
311 δ (composeA da1 s2 da2) (s1 , ss2) a =
|
|
47
|
312 δ da1 s1 a , δs da2 (if ν da1 s1 then s2 ∷ ss2 else ss2) a
|
|
46
|
313
|
|
|
314 import Relation.Binary.EqReasoning as EqR
|
|
|
315
|
|
|
316 composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : List ∞ S2) →
|
|
|
317 lang (composeA da1 s2 da2) (s1 , ss) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 ∪ lang (powA da2) ss
|
|
47
|
318 ≅ν (composeA-gen da1 da2 s1 s2 ss) = refl
|
|
46
|
319 ≅δ (composeA-gen da1 da2 s1 s2 ss) a with ν da1 s1
|
|
47
|
320 ... | false = composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 ss a)
|
|
46
|
321 ... | true = begin
|
|
47
|
322 lang (composeA da1 s2 da2) (δ da1 s1 a , δ da2 s2 a ∷ δs da2 ss a)
|
|
|
323 ≈⟨ composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 (s2 ∷ ss) a) ⟩
|
|
|
324 lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang (powA da2) (δs da2 (s2 ∷ ss) a)
|
|
|
325 ≈⟨ {!!} ⟩
|
|
|
326 (lang da2 (δ da2 s2 a) ∪ lang (powA da2) (δs da2 ss a))
|
|
|
327 ≈⟨ ≅sym {!!} ⟩
|
|
|
328 (lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang da2 (δ da2 s2 a)) ∪ lang (powA da2) (δs da2 ss a)
|
|
46
|
329 ∎ where open EqR (Bis _)
|
|
|
330
|
|
47
|
331 postulate
|
|
|
332 composeA-correct : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) s1 s2 →
|
|
46
|
333 lang (composeA da1 s2 da2) (s1 , []) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2
|
|
|
334
|
|
|
335
|
|
|
336 open import Data.Maybe
|
|
|
337
|
|
|
338 acceptingInitial : ∀{S} (s0 : S) (da : DA S) → DA (Maybe S)
|
|
|
339 ν (acceptingInitial s0 da) (just s) = ν da s
|
|
|
340 δ (acceptingInitial s0 da) (just s) a = just (δ da s a)
|
|
|
341 ν (acceptingInitial s0 da) nothing = true
|
|
|
342 δ (acceptingInitial s0 da) nothing a = just (δ da s0 a)
|
|
|
343
|
|
|
344
|
|
|
345
|
|
|
346 finalToInitial : ∀{S} (da : DA (Maybe S)) → DA (List ∞ (Maybe S))
|
|
|
347 ν (finalToInitial da) ss = νs da ss
|
|
|
348 δ (finalToInitial da) ss a =
|
|
|
349 let ss′ = δs da ss a
|
|
|
350 in if νs da ss then δ da nothing a ∷ ss′ else ss′
|
|
|
351
|
|
|
352
|
|
|
353 starA : ∀{S}(s0 : S)(da : DA S) → DA (List ∞(Maybe S))
|
|
|
354 starA s0 da = finalToInitial (acceptingInitial s0 da)
|
|
|
355
|
|
|
356
|
|
47
|
357 postulate
|
|
|
358 acceptingInitial-just : ∀{i S} (s0 : S) (da : DA S) {s : S} →
|
|
46
|
359 lang (acceptingInitial s0 da) (just s) ≅⟨ i ⟩≅ lang da s
|
|
47
|
360 acceptingInitial-nothing : ∀{i S} (s0 : S) (da : DA S) →
|
|
46
|
361 lang (acceptingInitial s0 da) nothing ≅⟨ i ⟩≅ ε ∪ lang da s0
|
|
47
|
362 starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : List ∞ (Maybe S))→
|
|
46
|
363 lang (starA s0 da) ss ≅⟨ i ⟩≅
|
|
|
364 lang (powA (acceptingInitial s0 da)) ss · (lang da s0) *
|
|
47
|
365 starA-correct : ∀{i S} (da : DA S) (s0 : S) →
|
|
|
366 lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *
|
|
46
|
367
|
