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