RIS.automata: finite state automata.
Set Implicit Arguments.
This module contains the definitions of deterministic and
non-deterministic automata, as well as a proof of Kleene's theorem.
Require Import tools algebra language regexp.
Require Import Bool.
Section automata.
Section def.
Context {Q : Set}{decQ: decidable_set Q }.
Context {X : Set}{decX: decidable_set X }.
Definition NFA Q X := ((list Q) × list (Q × X × Q))%type.
Fixpoint pathNFA (A : NFA Q X) p w q :=
match w with
| [] ⇒ p = q
| a::w ⇒ ∃ q', (p,a,q') ∈ snd A ∧ pathNFA A q' w q
end.
Definition langNFA A p : language :=
fun w ⇒ ∃ q, pathNFA A p w q ∧ q ∈ fst A.
Definition DFA Q X := Q → bool × (X → Q).
Fixpoint iter_auto (A : DFA Q X) q u :=
match u with
| [] ⇒ q
| a::u ⇒ iter_auto A (snd (A q) a) u
end.
Definition langDFA A q : language := fun u ⇒ fst (A (iter_auto A q u)) = true.
Definition Reachables (A : DFA Q X) R := ∀ q a, q ∈ R → snd (A q) a ∈ R.
Lemma Reachables_spec A R : Reachables A R ↔ ∀ q u, q ∈ R → iter_auto A q u ∈ R.
Definition determinise (A : NFA Q X) : DFA (list Q) X :=
fun l ⇒ ((existsb (fun q ⇒ inb q (fst A)) l),
(fun x ⇒ {{flat_map (fun tr ⇒ match tr with
| (p,y,q)⇒ if inb p l && x=?=y then [q] else []
end) (snd A)}})).
Definition statesNFA (A : NFA Q X) := {{fst A ++ flat_map (fun tr ⇒ [fst (fst tr);snd tr]) (snd A)}}.
Lemma statesNFA_spec A q :
q ∈ statesNFA A ↔ q ∈ fst A ∨ ∃ tr, tr ∈ snd A ∧ (q = fst(fst tr) ∨ q = snd tr).
Lemma statesNFA_path A p w q : pathNFA A p w q → w = [] ∨ (p ∈ statesNFA A ∧ q ∈ statesNFA A).
Lemma pathNFA_app A p u v q : pathNFA A p (u++v) q ↔ ∃ r, pathNFA A p u r ∧ pathNFA A r v q.
Lemma pathNFA_last A p u x q : pathNFA A p (u++[x]) q ↔ ∃ r, pathNFA A p u r ∧ (r,x,q)∈(snd A).
End def.
Context {Q : Set}{decQ: decidable_set Q }.
Context {X : Set}{decX: decidable_set X }.
Lemma determinise_lang A (q : Q) : langNFA A q ≃ langDFA (determinise A) [q].
Lemma determinise_Reachables (A : NFA Q X) :
Reachables (determinise A) (flat_map shuffles (subsets (statesNFA A))).
Definition NFA_of_regexp (e : @regexp X) : NFA regexp X :=
((filter (fun e ⇒ ϵ e =?= e_un) (stateSpace e)),
flat_map (fun f ⇒
flat_map
(fun a ⇒
map (fun g ⇒ (f,a,g))
(δA a f)
)
(Var e)
)
(stateSpace e)).
Lemma stateSpace_statesNFA e : statesNFA (NFA_of_regexp e) ⊆ stateSpace e.
Lemma NFA_of_regexp_langNFA e f :
f ∈ (stateSpace e) → ⟦f⟧ ≃ langNFA (NFA_of_regexp e) f.
Lemma NFA_of_regexp_spec e : ⟦e⟧ ≃ langNFA (NFA_of_regexp e) e.
Lemma pathNFA_stateSpace e e' f g u :
e' ∈ stateSpace e → pathNFA (NFA_of_regexp e') f u g → pathNFA (NFA_of_regexp e) f u g.
Fixpoint pathRestr (A : NFA Q X) states p w q :=
match w with
| [] ⇒ p=q
| a::w ⇒ ∃ q', (w = [] ∨ q' ∈ states) ∧ (p,a,q') ∈ snd A ∧ pathRestr A states q' w q
end.
Lemma pathRestr_pathNFA A p q w : pathNFA A p w q ↔ pathRestr A (statesNFA A) p w q.
Lemma pathRestr_app A S p q r u v :
q ∈ S → pathRestr A S p u q → pathRestr A S q v r → pathRestr A S p (u++v) r.
Lemma pathRestr_incl A S1 S2 p q w : S1 ⊆ S2 → pathRestr A S1 p w q → pathRestr A S2 p w q.
Lemma pathRestr_split A S p q r u :
pathRestr A S p u q →
(pathRestr A (S∖r) p u q)
\/(∃ w1 w2 w3, u = w1 ++ w2 ++ w3
∧ pathRestr A (S∖r) p w1 r
∧ pathRestr A S r w2 r
∧ pathRestr A (S∖r) r w3 q).
Lemma regexpPath (A : NFA Q X) p q : ∃ e, ∀ w, ⟦e⟧ w ↔ pathNFA A p w q.
CoInductive bissim (A: DFA Q X) : relation Q :=
| transition p q : fst (A p) = fst (A q) → (∀ a, bissim A (snd (A p) a) (snd (A q) a)) →
bissim A p q.
Lemma bissim_lang A p q :
bissim A p q ↔ langDFA A p ≃ langDFA A q.
Global Instance bissim_equiv A : Equivalence (bissim A).
End automata.
Section kleeneTheorem.
Context {X : Set}{decX: decidable_set X }.
Definition regular (L : @language X) := ∃ e, ⟦e⟧ ≃ L.
Definition rational (L : @language X) :=
∃ Q : Set, ∃ d : decidable_set Q, (∃ A (q : Q), langNFA A q ≃ L).
Theorem KleeneTheorem (L : @language X) : regular L ↔ rational L.
End kleeneTheorem.
Require Import Bool.
Section automata.
Section def.
Context {Q : Set}{decQ: decidable_set Q }.
Context {X : Set}{decX: decidable_set X }.
Definition NFA Q X := ((list Q) × list (Q × X × Q))%type.
Fixpoint pathNFA (A : NFA Q X) p w q :=
match w with
| [] ⇒ p = q
| a::w ⇒ ∃ q', (p,a,q') ∈ snd A ∧ pathNFA A q' w q
end.
Definition langNFA A p : language :=
fun w ⇒ ∃ q, pathNFA A p w q ∧ q ∈ fst A.
Definition DFA Q X := Q → bool × (X → Q).
Fixpoint iter_auto (A : DFA Q X) q u :=
match u with
| [] ⇒ q
| a::u ⇒ iter_auto A (snd (A q) a) u
end.
Definition langDFA A q : language := fun u ⇒ fst (A (iter_auto A q u)) = true.
Definition Reachables (A : DFA Q X) R := ∀ q a, q ∈ R → snd (A q) a ∈ R.
Lemma Reachables_spec A R : Reachables A R ↔ ∀ q u, q ∈ R → iter_auto A q u ∈ R.
Definition determinise (A : NFA Q X) : DFA (list Q) X :=
fun l ⇒ ((existsb (fun q ⇒ inb q (fst A)) l),
(fun x ⇒ {{flat_map (fun tr ⇒ match tr with
| (p,y,q)⇒ if inb p l && x=?=y then [q] else []
end) (snd A)}})).
Definition statesNFA (A : NFA Q X) := {{fst A ++ flat_map (fun tr ⇒ [fst (fst tr);snd tr]) (snd A)}}.
Lemma statesNFA_spec A q :
q ∈ statesNFA A ↔ q ∈ fst A ∨ ∃ tr, tr ∈ snd A ∧ (q = fst(fst tr) ∨ q = snd tr).
Lemma statesNFA_path A p w q : pathNFA A p w q → w = [] ∨ (p ∈ statesNFA A ∧ q ∈ statesNFA A).
Lemma pathNFA_app A p u v q : pathNFA A p (u++v) q ↔ ∃ r, pathNFA A p u r ∧ pathNFA A r v q.
Lemma pathNFA_last A p u x q : pathNFA A p (u++[x]) q ↔ ∃ r, pathNFA A p u r ∧ (r,x,q)∈(snd A).
End def.
Context {Q : Set}{decQ: decidable_set Q }.
Context {X : Set}{decX: decidable_set X }.
Lemma determinise_lang A (q : Q) : langNFA A q ≃ langDFA (determinise A) [q].
Lemma determinise_Reachables (A : NFA Q X) :
Reachables (determinise A) (flat_map shuffles (subsets (statesNFA A))).
Definition NFA_of_regexp (e : @regexp X) : NFA regexp X :=
((filter (fun e ⇒ ϵ e =?= e_un) (stateSpace e)),
flat_map (fun f ⇒
flat_map
(fun a ⇒
map (fun g ⇒ (f,a,g))
(δA a f)
)
(Var e)
)
(stateSpace e)).
Lemma stateSpace_statesNFA e : statesNFA (NFA_of_regexp e) ⊆ stateSpace e.
Lemma NFA_of_regexp_langNFA e f :
f ∈ (stateSpace e) → ⟦f⟧ ≃ langNFA (NFA_of_regexp e) f.
Lemma NFA_of_regexp_spec e : ⟦e⟧ ≃ langNFA (NFA_of_regexp e) e.
Lemma pathNFA_stateSpace e e' f g u :
e' ∈ stateSpace e → pathNFA (NFA_of_regexp e') f u g → pathNFA (NFA_of_regexp e) f u g.
Fixpoint pathRestr (A : NFA Q X) states p w q :=
match w with
| [] ⇒ p=q
| a::w ⇒ ∃ q', (w = [] ∨ q' ∈ states) ∧ (p,a,q') ∈ snd A ∧ pathRestr A states q' w q
end.
Lemma pathRestr_pathNFA A p q w : pathNFA A p w q ↔ pathRestr A (statesNFA A) p w q.
Lemma pathRestr_app A S p q r u v :
q ∈ S → pathRestr A S p u q → pathRestr A S q v r → pathRestr A S p (u++v) r.
Lemma pathRestr_incl A S1 S2 p q w : S1 ⊆ S2 → pathRestr A S1 p w q → pathRestr A S2 p w q.
Lemma pathRestr_split A S p q r u :
pathRestr A S p u q →
(pathRestr A (S∖r) p u q)
\/(∃ w1 w2 w3, u = w1 ++ w2 ++ w3
∧ pathRestr A (S∖r) p w1 r
∧ pathRestr A S r w2 r
∧ pathRestr A (S∖r) r w3 q).
Lemma regexpPath (A : NFA Q X) p q : ∃ e, ∀ w, ⟦e⟧ w ↔ pathNFA A p w q.
CoInductive bissim (A: DFA Q X) : relation Q :=
| transition p q : fst (A p) = fst (A q) → (∀ a, bissim A (snd (A p) a) (snd (A q) a)) →
bissim A p q.
Lemma bissim_lang A p q :
bissim A p q ↔ langDFA A p ≃ langDFA A q.
Global Instance bissim_equiv A : Equivalence (bissim A).
End automata.
Section kleeneTheorem.
Context {X : Set}{decX: decidable_set X }.
Definition regular (L : @language X) := ∃ e, ⟦e⟧ ≃ L.
Definition rational (L : @language X) :=
∃ Q : Set, ∃ d : decidable_set Q, (∃ A (q : Q), langNFA A q ≃ L).
Theorem KleeneTheorem (L : @language X) : regular L ↔ rational L.
End kleeneTheorem.