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