# nfa: Non-deterministic Finite Automata

Require Import positives comparisons.
Require Import kleene regex rmx sums matrix_ext prop normalisation.
Require dfa.
Set Implicit Arguments.
Unset Printing Implicit Defensive.

# Matricial (non deterministic) finite automata

transitions are labelled with regular expressions
Record t := mk {
n: nat;
u: rmx 1 n;
M: rmx n n;
v: rmx n 1
}.
Notation "x ^u" := (u x) (at level 2, left associativity, format "x ^u").
Notation "x ^M" := (M x) (at level 2, left associativity, format "x ^M").
Notation "x ^v" := (v x) (at level 2, left associativity, format "x ^v").

formal evaluation of matricial automata into regular expressions
Definition eval A := mx_scal (A^u A^M^* A^v).
Arguments eval !_ /.

two important classes of automata:
• NFA, for which transitions are labelled by sums of letters, and
• NFA with epsilon-transitions, where the sums may also include 1
characterisation of epsilon for automata with a pure transition matrix
Lemma epsilon_eval n u (M: rmx n n) v: is_pure_mx M
(epsilon (mx_scal (uM^*v)) epsilon (mx_scal (uv))).
Proof.
intro HM. rewrite 2epsilon_iff_reflexive_eps.
rewrite 2(scal_mx_map (fun eeps e)).
rewrite 3epsilon_mx_dot, epsilon_mx_str, (epsilon_mx_pure HM).
now rewrite str0, dotx1.
Qed.

characterisation of derivatives for NFA
Lemma deriv_eval a n u (M: rmx n n) v: is_01_mx u is_pure_mx M is_01_mx v
deriv a (mx_scal (uM^*v)) mx_scal (uepsilon_mx (deriv_mx a M)M^*v).
Proof.
intros Hu HM Hv.
rewrite (scal_mx_map (deriv a)). apply mx_scal_weq.
rewrite 2deriv_mx_dot, deriv_mx_str_strict. 2: apply epsilon_mx_pure; assumption.
rewrite <-expand_01_mx by assumption.
rewrite (deriv_01_mx _ Hu), (deriv_01_mx _ Hv), epsilon_deriv_pure_mx by assumption.
ra.
Qed.

# Language of a NFA

(operationally, not through evaluation into regular expressions)
Fixpoint lang n (M: rmx n n) v u w: Prop :=
match w with
| nilepsilon (mx_scal (u v))
| cons a wlang M v (u epsilon_mx (deriv_mx a M)) w
end.

the language of the NFA is that obtained by evaluation into regular expressions
Theorem eval_lang n u M v (H: is_nfa (@mk n u M v)):
regex.lang (mx_scal (u M^* v)) lang M v u.
Proof.
unfold regex.lang. intro w. revert u H. induction w; intros u H.
unfold derivs. now rewrite epsilon_eval by apply H.
unfold derivs. setoid_rewrite <- IHw.
clear IHw. revert w. apply lang_weq, deriv_eval; apply H.
split. 2: apply H. apply is_01_mx_dot. apply H. apply is_01_mx_epsilon.
Qed.

#[export] Instance lang_leq n (M: rmx n n) v: Proper (leq ==> leq) (lang M v).
Proof.
intros u u' H w. revert u u' H; induction w; intros u u' H; unfold lang; fold lang.
apply epsilon_leq.   now rewrite H.
apply IHw. now rewrite H.
Qed.

#[export] Instance lang_weq n (M: rmx n n) v: Proper (weq ==> weq) (lang M v) := op_leq_weq_1.

#[export] Instance lang_weq' n (M: rmx n n) v: Proper (weq ==> eq ==> iff) (lang M v).
Proof. intros ? ? H ? ? <-. now apply lang_weq. Qed.

Lemma lang_empty n (u: rmx 1 n) M v: u 0 lang M v u bot.
Proof.
intros Hu w. revert Hu. induction w; intro Hu. simpl; fold_regex.
rewrite Hu, dot0x. intuition.
simpl. rewrite <-IHw by assumption. now rewrite Hu, dot0x.
Qed.

# Injection of DFA into NFA

Module dfa.

injection into NFA
Definition to_nfa (A: dfa.t): t := mk
(mx_fun (fun _dfa.u A) 1)
(\sum_(a\in dfa.vars A) mx_fun (fun xdfa.M A x a) (var a))
(fun i _ofbool (dfa.v A i)).

injected DFA are indeed NFA
Lemma is_nfa_nfa A: is_nfa (to_nfa A).
Proof.
split. intros ? ?. simpl. unfold mx_fun. case eqb_ord; constructor.
split. intros ? ?. simpl. rewrite mx_sup. apply is_pure_sup.
intros. unfold mx_fun. case eqb_ord; constructor.
intros ? ?. apply is_01_ofbool.
Qed.

evaluation at a given state, into regular expressions
Notation "A @ i" := (eval (to_nfa (dfa.reroot A i))) (at level 1).

the language of a DFA coincides with that of the underlying NFA
Theorem nfa_lang A i: dfa.lang A i
lang ((to_nfa A)^M) ((to_nfa A)^v) (mx_fun (fun _i) 1).
Proof.
intro w. revert i. induction w; intro i; simpl.
- rewrite epsilon_iff_reflexive_eps. rewrite (scal_mx_map (fun eeps e)).
change (mx_dot regex_ops regex_tt) with (@dot (mx_ops regex_ops regex_tt)).
rewrite (mx_dot_kfun1 (X:=regex_ops)).
unfold mx_map, mx_scal. rewrite <-epsilon_iff_reflexive_eps. case dfa.v; reflexivity.
- rewrite IHw. clear IHw.
change (mx_dot regex_ops regex_tt) with (@dot (mx_ops regex_ops regex_tt)).
rewrite (mx_dot_kfun1 (X:=regex_ops)). unfold mx_fun, epsilon_mx, mx_map.
setoid_rewrite mx_sup. setoid_rewrite deriv_sup. setoid_rewrite epsilon_sup. split.
+ intros [Ha H]. eapply lang_leq. 2: apply H. clear w H.
intros _ j. rewrite <-(leq_xsup _ _ a Ha).
case eqb_ord. 2: apply leq_bx.
simpl. now rewrite eqb_refl.
+ intros H. split. case (List.in_dec (cmp_dec _) a (dfa.vars A)) as [Ha|Ha]. assumption.
apply lang_empty in H. elim H. clear H.
intros o j. apply sup_b. intros b Hb. case eqb_ord. 2: reflexivity.
simpl. case eqb_spec; simpl. 2: reflexivity.
intros <-. elim (Ha Hb).
eapply lang_leq. 2: apply H. clear w H.
intros _ j. apply leq_supx. intros b _.
case eqb_spec. 2: intros; ra.
intros →. simpl. case eqb_spec; simpl. 2: intro; lattice.
intros <-. now rewrite eqb_refl.
Qed.

the language of the DFA is that obtained by evaluation into regular expressions
Corollary eval_lang A i: regex.lang A@i dfa.lang A i.
Proof. setoid_rewrite eval_lang. 2: apply is_nfa_nfa. now rewrite nfa_lang. Qed.

End dfa.

Coercion dfa.to_nfa: dfa.t >-> t.