Authors: Christian Doczkal and Jan-Oliver Kaiser
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype path fingraph finfun finset.
Require Import misc regexp.
Set Implicit Arguments.
Section FA.
Variable char : finType.
Definition word := regexp.word char.
Require Import misc regexp.
Set Implicit Arguments.
Section FA.
Variable char : finType.
Definition word := regexp.word char.
Record dfa : Type := {
dfa_state :> finType;
dfa_s : dfa_state;
dfa_fin : pred dfa_state;
dfa_trans : dfa_state -> char -> dfa_state
}.
For DFAs, we use the direct recursive defintion of acceptance
as well as a definition in terms of runs. The latter is used
in the translation of DFAs to regular expressions.
Fixpoint dfa_accept (A : dfa) (x : A) w :=
if w is a :: w' then dfa_accept A (dfa_trans A x a) w' else x \in dfa_fin A.
Arguments dfa_trans [d] x a.
Arguments dfa_accept [A] x w.
Section DFA_Acceptance.
Variable A : dfa.
Lemma dfa_accept_cons (x : A) a w :
a :: w \in dfa_accept x = (w \in dfa_accept (dfa_trans x a)).
Proof. by rewrite -simpl_predE /=. Qed.
We define a run of w on the automaton A
to be the list of states x_1 .. x|w|
traversed when following the edges labeled
w_1 .. w|w| starting in x.
So the run on x does not include x
Fixpoint dfa_run (x : A) (w : word) : seq A :=
if w is a :: w' then dfa_trans x a :: dfa_run (dfa_trans x a) w' else [::].
Lemma dfa_run_take x w n : take n (dfa_run x w) = dfa_run x (take n w).
Proof. elim: w x n => [|a w IHw] x n //. case: n => [|n] //=. by rewrite IHw. Qed.
Lemma dfa_run_cat x w1 w2 :
dfa_run x (w1 ++ w2) = dfa_run x w1 ++ dfa_run (last x (dfa_run x w1)) w2.
Proof. elim: w1 w2 x => [|a w1 IHw1] w2 x //. simpl. by rewrite IHw1. Qed.
Definition delta x w := last x (dfa_run x w).
Lemma delta_cons x a w : delta x (a :: w) = delta (dfa_trans x a) w.
Proof. by []. Qed.
Lemma delta_cat x w1 w2 : delta x (w1 ++ w2) = delta (delta x w1) w2.
Proof. by rewrite /delta dfa_run_cat last_cat. Qed.
Definition delta_s w := delta (dfa_s A) w.
Lemma delta_accept (x : A) w : (w \in dfa_accept x) = (delta x w \in dfa_fin A).
Proof. elim: w x => [|a w IHw] x //. by rewrite /= -IHw. Qed.
Lemma dfa_trans1 x w a :
dfa_trans (delta x w) a = delta x (w ++ [::a]).
Proof. elim: w x a => [|b w IHw] x a //=. by rewrite !delta_cons IHw. Qed.
End DFA_Acceptance.
Definition dfa_lang A := [pred w | dfa_accept (dfa_s A) w].
Arguments delta_s A w.
Arguments delta [A] x w.
Arguments dfa_accept A x w.
Record nfa : Type := {
nfa_state :> finType;
nfa_s : nfa_state;
nfa_fin : pred nfa_state;
nfa_trans : nfa_state -> char -> nfa_state -> bool
}.
nfa_state :> finType;
nfa_s : nfa_state;
nfa_fin : pred nfa_state;
nfa_trans : nfa_state -> char -> nfa_state -> bool
}.
Non-deterministic acceptance.
Fixpoint nfa_accept (A : nfa) (x : A) w :=
if w is a :: w' then [exists y, nfa_trans A x a y && nfa_accept A y w']
else x \in nfa_fin A.
Definition nfa_lang (A : nfa) := [pred w | nfa_accept A (nfa_s A) w].
Definition nfa_char a :=
{| nfa_s := false ;
nfa_fin := id ;
nfa_trans x b y := [&& (b == a), ~~ x & y] |}.
Lemma nfa_char_correct a : nfa_lang (nfa_char a) =1 pred1 [:: a].
Proof.
move => [|b w] => //.
apply/existsP/eqP => [[x] /andP [/and3P [/eqP -> _ Hx]] |[-> ->]].
- case: w => //= c w /existsP [y] /=. by rewrite Hx andbF.
- exists true. by rewrite /= eqxx.
Qed.
if w is a :: w' then [exists y, nfa_trans A x a y && nfa_accept A y w']
else x \in nfa_fin A.
Definition nfa_lang (A : nfa) := [pred w | nfa_accept A (nfa_s A) w].
Definition nfa_char a :=
{| nfa_s := false ;
nfa_fin := id ;
nfa_trans x b y := [&& (b == a), ~~ x & y] |}.
Lemma nfa_char_correct a : nfa_lang (nfa_char a) =1 pred1 [:: a].
Proof.
move => [|b w] => //.
apply/existsP/eqP => [[x] /andP [/and3P [/eqP -> _ Hx]] |[-> ->]].
- case: w => //= c w /existsP [y] /=. by rewrite Hx andbF.
- exists true. by rewrite /= eqxx.
Qed.
Equivalence of DFAs and NFAs
We use the powerset construction to obtain a deterministic automaton from a non-deterministic one.
Section PowersetConstruction.
Variable A : nfa.
Definition nfa_to_dfa := {|
dfa_s := [set nfa_s A];
dfa_fin X := [exists x: A, (x \in X) && nfa_fin A x];
dfa_trans X a := \bigcup_(x | x \in X) [set y | nfa_trans A x a y] |}.
Lemma nfa_to_dfa_aux2 (x : A) w (X : nfa_to_dfa) :
x \in X -> nfa_accept A x w -> dfa_accept X w.
Proof. move => H0.
elim: w X x H0 => [|a w IHw] X x H0 /=.
move => H1. apply/existsP. by eexists; erewrite H0.
move => /= /existsP [] y /andP [] H1 H2.
apply: (IHw _ y) => //.
apply/bigcupP. exists x => //=. by rewrite in_set.
Qed.
Lemma nfa_to_dfa_aux1 (X : nfa_to_dfa) w :
dfa_accept X w -> exists2 x, (x \in X) & nfa_accept A x w.
Proof. elim: w X => [|a w IHw] X => //=.
move/existsP => [x] /andP [] H0 H1. by eexists; eassumption.
move/IHw => [] y /bigcupP [x] H0. rewrite inE => H1 H2.
eexists. eassumption.
apply/existsP. exists y. by apply/andP.
Qed.
Lemma nfa_to_dfa_correct : nfa_lang A =i dfa_lang nfa_to_dfa.
Proof. move => w. apply/idP/idP => /=.
apply: nfa_to_dfa_aux2. by apply/set1P.
by move/nfa_to_dfa_aux1 => [x] /set1P ->.
Qed.
End PowersetConstruction.
Variable A : nfa.
Definition nfa_to_dfa := {|
dfa_s := [set nfa_s A];
dfa_fin X := [exists x: A, (x \in X) && nfa_fin A x];
dfa_trans X a := \bigcup_(x | x \in X) [set y | nfa_trans A x a y] |}.
Lemma nfa_to_dfa_aux2 (x : A) w (X : nfa_to_dfa) :
x \in X -> nfa_accept A x w -> dfa_accept X w.
Proof. move => H0.
elim: w X x H0 => [|a w IHw] X x H0 /=.
move => H1. apply/existsP. by eexists; erewrite H0.
move => /= /existsP [] y /andP [] H1 H2.
apply: (IHw _ y) => //.
apply/bigcupP. exists x => //=. by rewrite in_set.
Qed.
Lemma nfa_to_dfa_aux1 (X : nfa_to_dfa) w :
dfa_accept X w -> exists2 x, (x \in X) & nfa_accept A x w.
Proof. elim: w X => [|a w IHw] X => //=.
move/existsP => [x] /andP [] H0 H1. by eexists; eassumption.
move/IHw => [] y /bigcupP [x] H0. rewrite inE => H1 H2.
eexists. eassumption.
apply/existsP. exists y. by apply/andP.
Qed.
Lemma nfa_to_dfa_correct : nfa_lang A =i dfa_lang nfa_to_dfa.
Proof. move => w. apply/idP/idP => /=.
apply: nfa_to_dfa_aux2. by apply/set1P.
by move/nfa_to_dfa_aux1 => [x] /set1P ->.
Qed.
End PowersetConstruction.
Embedding deterministic automata in non-deterministic automata.
Section Embed.
Variable A : dfa.
Definition dfa_to_nfa : nfa := {|
nfa_s := dfa_s A;
nfa_fin := dfa_fin A;
nfa_trans x a y := y == dfa_trans x a |}.
Lemma dfa_to_nfa_correct : dfa_lang A =i nfa_lang dfa_to_nfa.
Proof.
move => w. rewrite /dfa_lang /nfa_lang /=. move: (dfa_s A) => x.
elim: w x => [|b w IHw] x //=.
rewrite dfa_accept_cons IHw !inE /=. apply/idP/existsP.
move => H0. exists (dfa_trans x b). by rewrite eq_refl.
by move => [] y /andP [] /eqP ->.
Qed.
End Embed.
Variable A : dfa.
Definition dfa_to_nfa : nfa := {|
nfa_s := dfa_s A;
nfa_fin := dfa_fin A;
nfa_trans x a y := y == dfa_trans x a |}.
Lemma dfa_to_nfa_correct : dfa_lang A =i nfa_lang dfa_to_nfa.
Proof.
move => w. rewrite /dfa_lang /nfa_lang /=. move: (dfa_s A) => x.
elim: w x => [|b w IHw] x //=.
rewrite dfa_accept_cons IHw !inE /=. apply/idP/existsP.
move => H0. exists (dfa_trans x b). by rewrite eq_refl.
by move => [] y /andP [] /eqP ->.
Qed.
End Embed.
Definition dfa_void :=
{| dfa_s := tt; dfa_fin x := false; dfa_trans x a := tt |}.
Lemma dfa_void_correct (x: dfa_void) w: ~~ dfa_accept x w.
Proof. by elim: w x => [|a w IHw] //=. Qed.
Definition dfa_eps :=
{| dfa_s := true; dfa_fin := id ; dfa_trans x a := false |}.
Lemma dfa_eps_correct : dfa_lang dfa_eps =i pred1 [::].
Proof.
have H: (forall w, ~~ @dfa_accept dfa_eps false w) by elim => [|a v IHv] //=.
elim => [|a w IHw] //. apply/idP/idP. exact: H.
Qed.
{| dfa_s := tt; dfa_fin x := false; dfa_trans x a := tt |}.
Lemma dfa_void_correct (x: dfa_void) w: ~~ dfa_accept x w.
Proof. by elim: w x => [|a w IHw] //=. Qed.
Definition dfa_eps :=
{| dfa_s := true; dfa_fin := id ; dfa_trans x a := false |}.
Lemma dfa_eps_correct : dfa_lang dfa_eps =i pred1 [::].
Proof.
have H: (forall w, ~~ @dfa_accept dfa_eps false w) by elim => [|a v IHv] //=.
elim => [|a w IHw] //. apply/idP/idP. exact: H.
Qed.
Operations on deterministic automata.
Complement automaton
Definition dfa_compl :=
{|
dfa_s := dfa_s A1;
dfa_fin := [predC (dfa_fin A1)];
dfa_trans := (@dfa_trans A1)
|}.
Lemma dfa_compl_correct w :
w \in dfa_lang dfa_compl = (w \notin dfa_lang A1).
Proof.
rewrite /dfa_lang !inE {2}/dfa_compl /=.
elim: w (dfa_s _) => [| a w IHw] x //=.
Qed.
{|
dfa_s := dfa_s A1;
dfa_fin := [predC (dfa_fin A1)];
dfa_trans := (@dfa_trans A1)
|}.
Lemma dfa_compl_correct w :
w \in dfa_lang dfa_compl = (w \notin dfa_lang A1).
Proof.
rewrite /dfa_lang !inE {2}/dfa_compl /=.
elim: w (dfa_s _) => [| a w IHw] x //=.
Qed.
BinOp Automaton
Definition dfa_op :=
{| dfa_s := (dfa_s A1, dfa_s A2);
dfa_fin q := let (x1,x2) := q in op (dfa_fin A1 x1) (dfa_fin A2 x2);
dfa_trans x a := (dfa_trans x.1 a, dfa_trans x.2 a) |}.
Lemma dfa_op_correct w :
w \in dfa_lang dfa_op = op (w \in dfa_lang A1) (w \in dfa_lang A2).
Proof.
rewrite /dfa_lang /=. move: (dfa_s A1) (dfa_s A2) => x y.
elim: w x y => [| a w IHw] //= x y. by rewrite dfa_accept_cons IHw.
Qed.
End DFAOps.
Operations on non-deterministic automata.
Concatenation of two non-deterministic automata.
This construction looks more complicated than the ususal construction with epsilon edges,
but the construction is essentially the same
Definition nfa_conc A1 A2 : nfa :=
{| nfa_s := inl _ (nfa_s A1);
nfa_fin := [pred x |
match x with
| inl x => (x \in nfa_fin A1) && (nfa_s A2 \in nfa_fin A2)
| inr x => x \in nfa_fin A2
end];
nfa_trans := fun x a y =>
match x,y with
| inl x, inl y => nfa_trans A1 x a y
| inl x, inr y => (x \in nfa_fin A1) && nfa_trans A2 (nfa_s A2) a y
| inr x, inr y => nfa_trans A2 x a y
| inr x, inl y => false
end
|}.
Lemma conc_inrP A1 A2 x w :
nfa_accept (nfa_conc A1 A2) (inr x) w = nfa_accept A2 x w.
Proof. elim: w x => [|a w IHw] x //=; apply/exists_inP/exists_inP.
move => [[y //|y Y1 Y2]]. exists y; by rewrite // -IHw.
case => y Y1 Y2. exists (inr y); by rewrite // IHw.
Qed.
Lemma conc_inlP A1 A2 x w : reflect
(exists w1 w2, [/\ w = w1 ++ w2 , nfa_accept A1 x w1 & w2 \in nfa_lang A2])
(nfa_accept (nfa_conc A1 A2) (inl x) w).
Proof. elim: w x => [x|a w IHw x] /=.
- rewrite inE. apply: (iffP andP) => [[H1 H2] | [[|a w1]] [[|b w2]] [] //].
do 2 exists [::]; by split.
- apply: (iffP exists_inP).
+ move => [[y Hy /IHw [w1 [w2 [e W1 W2]]] |y /andP [Y1 Y2 Y3] ]].
* exists (a::w1); exists w2 => //=. rewrite e; split => //.
apply/existsP; exists y. by rewrite Hy.
* exists [::]. exists (a::w). rewrite inE -(@conc_inrP A1 A2); split => //=.
apply/existsP; exists (inr y). by rewrite Y2 Y3.
+ move => [[|b w1] /= [w2 [e W1 W2]]].
* rewrite -e /= in W2. case/exists_inP : W2 => y Y1 Y2.
exists (inr y) ; by rewrite ?W1 ?conc_inrP.
* case : e => e1 e2. case/exists_inP : W1 => y Y1 Y2.
exists (inl y). by rewrite e1. apply/IHw. exists w1; exists w2. by split.
Qed.
Lemma nfa_conc_correct A1 A2 :
nfa_lang (nfa_conc A1 A2) =i conc (nfa_lang A1) (nfa_lang A2).
Proof. move => w.
apply/conc_inlP/concP => [[w1] [w2] [H1 [H2 H3]] | [v1] [v2] [E [H1 H2]]].
exists w1. exists w2. by split.
exists v1. by exists v2.
Qed.
For nfa_star we again have to duplicate some edges since we have no epsilon transitions.
Definition nfa_star A : nfa :=
{| nfa_s := None;
nfa_fin x := x == None;
nfa_trans x a y :=
match x,y with
| Some x, Some y => nfa_trans A x a y
| None, Some y => nfa_trans A (nfa_s A) a y
| Some x, None => [exists z, (nfa_trans A x a z) && (z \in nfa_fin A)]
| None, None => [exists z, (nfa_trans A (nfa_s A) a z) && (z \in nfa_fin A)]
end |}.
Since we need at least one step to get back to None,
acceptance in A can only be lifted to nfa_star A for nonempty words.
Lemma nfa_star_cont A x w :
~~ nilp w -> nfa_accept A x w -> nfa_accept (nfa_star A) (Some x) w.
Proof.
elim: w x => [|b [|c w] IHw] x //= _ H.
- apply/existsP; exists None. by rewrite H.
- case/exists_inP : H => y xy H. apply/exists_inP; exists (Some y) =>//.
exact: IHw.
Qed.
Lemma nfa_star_clone A w :
w \in nfa_lang A -> w \in nfa_lang (nfa_star A).
Proof. case: w => [|a w] //. rewrite !inE. exact: nfa_star_cont. Qed.
Lemma nfa_star_cat A x w1 w2 :
nfa_accept (nfa_star A) x w1 -> w2 \in nfa_lang (nfa_star A) ->
nfa_accept (nfa_star A) x (w1 ++ w2).
Proof.
elim: w1 x => [|a w1 IHw] x. by rewrite !inE /= => /eqP->.
case/exists_inP => y xy H1 H2. rewrite /=. apply/exists_inP; exists y => //.
exact: IHw.
Qed.
Lemma nfa_starE_aux {A x w} :
nfa_accept (nfa_star A) (Some x) w ->
(exists w1 w2, [/\ w = w1 ++ w2, nfa_accept A x w1 & nfa_accept (nfa_star A) None w2]).
Proof.
elim: w x => // a w IHw x /= /exists_inP [[y Hy|]].
- move/IHw => [w1] [w2] [H1 H2 H4].
exists (a::w1); exists w2.
split => // ; by [rewrite /= H1 | apply/existsP; exists y; rewrite Hy].
- move => E N. exists [::a]; exists w. by split.
Qed.
Lemma nfa_starE A a w: (a :: w) \in nfa_lang (nfa_star A) ->
exists w1 w2, [/\ w = w1 ++ w2, a::w1 \in nfa_lang A & w2 \in nfa_lang (nfa_star A)].
Proof.
rewrite inE /=. case/exists_inP => [] [y Y1 Y2|].
- case: (nfa_starE_aux Y2) => w1 [w2] [e acc1 acc2].
exists w1;exists w2; split => //.
by apply/exists_inP; exists y.
- case/exists_inP => y Y1 Y2 Hw. exists [::]; exists w; split => //.
rewrite inE /=. by apply/exists_inP; exists y.
Qed.
Lemma nfa_star_correct A : nfa_lang (nfa_star A) =i star (nfa_lang A).
Proof.
move => w. apply/idP/starP => [| [vv] H -> {w}].
+ move: {2}(size w) (leqnn (size w)) => n.
elim: n w => [[_ _|//]|n IHn [|a w] s]; try by exists [::].
case/nfa_starE => w1 [w2] [e H H'].
have w2_le_n : size w2 <= n.
apply: (@leq_trans (size w)) => //. by rewrite e size_cat leq_addl.
case (IHn _ w2_le_n H') => vv' Hvv e'.
exists [:: (a::w1) & vv'] => /=; by [rewrite H | subst].
+ elim: vv H => //= [] [|a w] // vv IHvv. (do 2 case/andP) => _ HA /IHvv.
apply: nfa_star_cat. by move/nfa_star_clone : HA.
Qed.
End NFAOps.
Fixpoint re_to_dfa (r : regexp char): dfa :=
match r with
| Void => dfa_void
| Eps => dfa_eps
| Atom a => nfa_to_dfa (nfa_char a)
| Star s => nfa_to_dfa (nfa_star (dfa_to_nfa (re_to_dfa s)))
| Plus s t => dfa_op orb (re_to_dfa s) (re_to_dfa t)
| Conc s t => nfa_to_dfa (nfa_conc (dfa_to_nfa (re_to_dfa s)) (dfa_to_nfa (re_to_dfa t)))
end.
Lemma re_to_dfa_correct r : dfa_lang (re_to_dfa r) =i r.
Proof with rewrite -?(nfa_to_dfa_correct,dfa_to_nfa_correct) //.
elim: r => [||a|s IHs |s IHs t IHt |s IHs t IHt] w //=...
- apply/negbTE; exact: dfa_void_correct.
- exact: dfa_eps_correct.
- exact: nfa_char_correct.
- rewrite nfa_star_correct. apply: star_eq => {w} w...
- by rewrite dfa_op_correct IHs IHt.
- rewrite nfa_conc_correct. apply: conc_eq => {w} w...
Qed.
Section Reachability.
Variable A : dfa.
Definition dfa_trans_some (x y : A) := [exists a, dfa_trans x a == y].
Lemma step_someP x y :
reflect (exists w, delta x w == y) (connect dfa_trans_some x y).
Proof.
apply: (iffP connectP) => [[p]|[w]].
- elim: p x y => [x y _ -> |z p IHp x y /= /andP[H1 H2 e]]; first by exists [::].
case: (IHp _ _ H2 e) => w e'.
case/existsP : H1 => [a /eqP Ha]. exists (a::w). by rewrite delta_cons Ha.
- elim: w x y => [x y /eqP e | a w IHw x y /IHw [p p1 p2]]; first by exists [::].
exists (dfa_trans x a::p) => //. rewrite /= p1 andbT. by apply/existsP; exists a.
Qed.
Definition reachable := connect dfa_trans_some (dfa_s A).
End Reachability.
Definition dfa_lang_empty A := [forall (x | reachable A x), x \notin dfa_fin A].
Lemma dfa_lang_emptyP A :
reflect (dfa_lang A =i pred0) (dfa_lang_empty A).
Proof.
apply: (iffP forall_inP) => [H w| H x R].
- apply/negbTE. rewrite /dfa_lang delta_accept H //.
apply/step_someP. by exists w.
- apply/negP => F. case/step_someP : R => w /eqP Hw.
suff: w \in dfa_lang A by rewrite H.
by rewrite delta_accept Hw.
Qed.
Section Equivalence.
Definition dfa_sym_diff A1 A2 := dfa_op addb A1 A2.
Definition dfa_equiv A1 A2 := dfa_lang_empty (dfa_sym_diff A1 A2).
Lemma dfa_equiv_correct A1 A2 :
reflect (dfa_lang A1 =i dfa_lang A2) (dfa_equiv A1 A2).
Proof.
apply: (iffP (dfa_lang_emptyP _)) => H w.
- move/negbT: (H w). rewrite !dfa_op_correct -addNb.
move/addbP. by rewrite negbK.
- apply/negbTE. by rewrite !dfa_op_correct H addbb.
Qed.
End Equivalence.
Decidability of regular expression equivalence
Definition re_equiv r s := dfa_equiv (re_to_dfa r) (re_to_dfa s).
Lemma re_equiv_correct r s : reflect (r =i s) (re_equiv r s).
Proof.
apply: (iffP (dfa_equiv_correct _ _)) => H w;
move/(_ w) : H; by rewrite !re_to_dfa_correct.
Qed.
Arguments reachable [dfa] x : rename.
Section Connected.
Variable A : dfa.
Definition reachable_type := { x:A | reachable x }.
Lemma reachable_trans_proof (x : reachable_type) a : reachable (dfa_trans (val x) a).
Proof.
apply: connect_trans (svalP x) _.
apply: connect1. by apply/existsP; eexists.
Qed.
Definition reachable_trans (x : reachable_type) a : reachable_type :=
Sub (dfa_trans (val x) a) (reachable_trans_proof x a).
Definition reachable_s : reachable_type := Sub (dfa_s A) (connect0 _ _).
Definition dfa_prune := {|
dfa_s := reachable_s;
dfa_fin x := val x \in dfa_fin A;
dfa_trans := reachable_trans
|}.
Lemma dfa_prune_correct : dfa_lang dfa_prune =i dfa_lang A.
Proof.
rewrite /dfa_lang /= (_: dfa_s A = val reachable_s) //.
move: (reachable_s) => x w. elim: w x => [|a w IHw] [x Hx] //.
by rewrite 2!dfa_accept_cons IHw.
Qed.
Definition connected (A : dfa) := surjective (delta_s A).
Definition connectedb (A : dfa) := [forall x: A, reachable x].
Lemma connectedP (B : dfa) : reflect (connected B) (connectedb B).
Proof.
apply: (iffP forallP) => [H x|H x]; last exact/step_someP.
by move/step_someP : (H x).
Qed.
Lemma dfa_prune_connectedb_aux x y :
connect (dfa_trans_some A) (val x) (val y) ->
connect (dfa_trans_some dfa_prune) x y.
Proof.
have H_step: forall x y : reachable_type,
dfa_trans_some A (val x) (val y) -> dfa_trans_some dfa_prune x y by [].
case/connectP => p.
elim: p x y => //= [x y _ /val_inj -> //|z p IHp x y /andP [H1 H2] e].
case/existsP : H1 => a Ha.
have/H_step H: dfa_trans_some A (val x) (val (reachable_trans x a)).
rewrite /= (eqP Ha). by apply/existsP; exists a.
apply: connect_trans (connect1 H) _. apply: IHp; by rewrite /= ?(eqP Ha) ?e.
Qed.
Lemma dfa_prune_connected : connected dfa_prune.
Proof.
apply/connectedP.
apply/forallP. move => /= [x Hx]. by apply: dfa_prune_connectedb_aux.
Qed.
Hint Resolve dfa_prune_connected.
For connected DFAs, we can use xchoose to obtain for every state
a word leading to that state. We use this in the Myhill-Nerode theorem
to obtain Myhill partitions from DFAs
Lemma dfa_prune_size : #|dfa_prune | <= #|A|.
Proof. by rewrite card_sig subset_leq_card // subset_predT. Qed.
A DFA is connected, if it has the same size as ist connected sub automaton
Lemma prune_eq_connected : #|A| = #|dfa_prune| -> connected A.
Proof.
move => H. apply/connectedP. apply/forallP => x.
by move: (cardT_eq (Logic.eq_sym H)) ->.
Qed.
End Connected.
Proof.
move => H. apply/connectedP. apply/forallP => x.
by move: (cardT_eq (Logic.eq_sym H)) ->.
Qed.
End Connected.
Section Minimize.
Variable A : dfa.
Definition coll x y := forall w, (delta x w \in dfa_fin A) = (delta y w \in dfa_fin A).
Definition dist0 : {set A*A} := [set x | (x.1 \in dfa_fin A) != (x.2 \in dfa_fin A)].
Definition distS (dist : {set A*A}) :=
[set x | [exists a, (dfa_trans x.1 a, dfa_trans x.2 a) \in dist]].
Lemma distSP (dist : {set A*A}) (x y : A) :
reflect (exists a, (dfa_trans x a, dfa_trans y a) \in dist)
((x,y) \in distS dist).
Proof. by apply: (iffP idP); rewrite !inE => /existsP. Qed.
Lemma distS_mono: mono distS.
Proof. move => s t /subsetP H.
apply/subsetP => [[x y]] /distSP [a H1]. apply/distSP. exists a. exact: H _ H1.
Qed.
Definition one_step_dist dist := dist0 :|: distS dist.
Lemma one_step_dist_mono : mono one_step_dist.
Proof.
move => D1 D2 H. apply/subsetP.
move => x. rewrite /one_step_dist ![_ \in _ :|: _]inE.
case (_ \in dist0) => //=. apply/subsetP : (distS_mono H) x.
Qed.
Definition dist := lfp one_step_dist.
Lemma distP x y :
reflect (exists w, (delta x w \in dfa_fin A) != (delta y w \in dfa_fin A))
((x,y) \in dist).
Proof.
rewrite /dist. apply: (iffP idP).
move: x y. apply lfp_ind => [x y | D IHD x y]; first by rewrite inE.
rewrite inE; case/orP => [H|/distSP [a]].
+ exists [::]. by rewrite inE in H.
+ case/IHD => w /= H. by exists (a::w).
- case => w. elim: w x y => [|a w IHw] u v.
+ by rewrite /delta /= (lfpE one_step_dist_mono) /dist0 !inE /= => ->.
+ rewrite -cat1s delta_cat => /IHw H.
rewrite (lfpE one_step_dist_mono) inE ( _ : _ \in distS _) ?orbT //.
apply/distSP. by exists a.
Qed.
Definition collb x y := (x,y) \notin dist.
Lemma collP x y : reflect (coll x y) (collb x y).
Proof.
rewrite /coll /collb. apply: (iffP idP) => [H w|H].
- apply/eqP. apply: negbNE. move: H. apply: contra => H.
apply/distP. by exists w.
- apply/distP => [[w]]. by rewrite H eqxx.
Qed.
Lemma collb_refl x : collb x x.
Proof. apply/collP. rewrite /coll. auto. Qed.
Lemma collb_sym : symmetric collb.
Proof. move => x y. by apply/collP/collP; move => H w; rewrite H. Qed.
Lemma collb_trans : transitive collb.
Proof. move => x y z /collP H1 /collP H2. apply/collP => w. by rewrite H1 H2. Qed.
Definition min_state := quot collb.
Definition class (x:A) : min_state :=
Repr (collb_refl) (collb_sym) (collb_trans) x.
Lemma collb_step a x y : collb x y -> collb (dfa_trans x a) (dfa_trans y a).
Proof. move => /collP H. apply/collP => w. by rewrite -!delta_cons H. Qed.
Lemma class_eq x y : reflect (class x = class y) (collb x y).
Proof. exact: Repr_id. Qed.
Definition minimize : dfa := {|
dfa_s := class (dfa_s A);
dfa_trans x a := class (dfa_trans (val x) a);
dfa_fin := [pred x | val x \in dfa_fin A ] |}.
Canonical fin_app_pred := ApplicativePred (dfa_fin minimize).
Lemma minimize_delta (x : A) w :
@delta minimize (class x) w = class (delta x w).
Proof.
elim: w x => //= a w IHw x. rewrite -cat1s !delta_cat /= -IHw.
f_equal. rewrite /delta /=. apply/class_eq. apply: collb_step.
by rewrite collb_sym (repr_rel collb_refl).
Qed.
Lemma minstate_exp (x : minimize) : x = class (val x).
Proof. case: x => x Hx /=. exact/eqP. Qed.
Lemma minimize_val (x : minimize) w : class (delta (val x) w) = (delta x w).
Proof. by rewrite {2}[x]minstate_exp minimize_delta. Qed.
Lemma minimal_fin (x : A) :
(class x \in dfa_fin minimize) = (x \in dfa_fin A).
Proof.
rewrite /class /minimize inE /=. symmetry.
by move/collP : (repr_rel collb_refl x) => /(_ [::]).
Qed.
End Minimize.
Arguments coll [A] x y.
Lemma minimize_correct A : dfa_lang (minimize A) =i dfa_lang A.
Proof.
move => w. rewrite !delta_accept {1}/dfa_s /=.
rewrite minimize_delta -topredE /=.
set x:= delta _ _. symmetry.
have:= (repr_rel (collb_refl A)) x. by move/collP => /(_ [::]).
Qed.
Lemma minimize_size A : #|minimize A| <= #|A|.
Proof. rewrite card_sig. exact: max_card. Qed.
Definition minimal (A : dfa) := forall B, dfa_lang A =i dfa_lang B -> #|A| <= #|B|.
Definition collapsed (A : dfa) := forall x y: A, coll x y <-> x = y.
Lemma minimize_collapsed (A : dfa) : collapsed (minimize A).
Proof.
split => [H|->]; last by apply/collP; exact: collb_refl.
rewrite [x]minstate_exp [y]minstate_exp. apply/class_eq. apply/collP => w.
by rewrite -!minimal_fin !minimize_val.
Qed.
Definition dfa_iso (A1 A2 : dfa) :=
exists i: A1 -> A2,
[/\ bijective i,
forall x a, i (dfa_trans x a) = dfa_trans (i x) a,
forall x, i (x) \in dfa_fin A2 = (x \in dfa_fin A1) &
i (dfa_s A1) = dfa_s A2 ].
Section Isomopism.
Variables (A B : dfa).
Hypothesis L_AB : dfa_lang A =i dfa_lang B.
Hypothesis (A_coll: collapsed A) (B_coll: collapsed B).
Hypothesis (A_conn : connected A) (B_conn : connected B).
Definition iso (x : A) : B := delta (dfa_s B) (cr A_conn x).
Definition iso_inv (x : B) : A := delta (dfa_s A) (cr B_conn x).
Lemma delta_iso w x : delta (iso x) w \in dfa_fin B = (delta x w \in dfa_fin A).
Proof.
rewrite -{2}[x](crK (Sf := A_conn)).
by rewrite /iso -!delta_cat -!delta_accept -!L_AB !delta_accept !delta_cat.
Qed.
Lemma delta_iso_inv w x : delta (iso_inv x) w \in dfa_fin A = (delta x w \in dfa_fin B).
Proof.
rewrite -{2}[x](crK (Sf:=B_conn)).
by rewrite /iso -!delta_cat -!delta_accept -!L_AB !delta_accept !delta_cat.
Qed.
Lemma can_iso : cancel iso_inv iso.
Proof. move => x. apply/B_coll => w. by rewrite delta_iso delta_iso_inv. Qed.
Lemma can_iso_inv : cancel iso iso_inv.
Proof. move => x. apply/A_coll => w. by rewrite delta_iso_inv delta_iso. Qed.
Lemma coll_iso : dfa_iso A B.
Proof.
exists iso. split.
- exact: Bijective can_iso_inv can_iso.
- move => x a. apply/B_coll => w. rewrite dfa_trans1 delta_cat -/(iso _).
by rewrite -delta_cat -!delta_iso_inv !can_iso_inv.
- move => x. by rewrite -[iso x]/(delta _ [::]) delta_iso.
- apply/B_coll => w. by rewrite delta_iso -!delta_accept.
Qed.
Lemma dfa_iso_size : dfa_iso A B -> #|A| = #|B|.
Proof. move => [iso [H _ _ _]]. exact (bij_card H). Qed.
End Isomopism.
Lemma minimize_connected A : connected A -> connected (minimize A).
Proof.
move => H [x Hx]. case: (H x) => w /eqP Hw. exists w.
rewrite /delta_s /minimize /= minimize_delta.
apply/eqP. apply/val_inj => //=. by rewrite (eqP Hx) -Hw.
Qed.
Lemma minimal_connected A : minimal A -> connected A.
Proof.
move => MA. apply: prune_eq_connected. apply: leq_eq _ (dfa_prune_size _).
exact: MA (psym (dfa_prune_correct _)).
Qed.
Lemma minimal_size_eq A B :
minimal A -> minimal B -> dfa_lang A =i dfa_lang B -> #|A| = #|B|.
Proof. move => MinA MinB H. by apply: leq_eq (MinA _ H) (MinB _ _) => w. Qed.
Lemma minimize_minimal A (CA : connected A) : minimal (minimize A).
Proof.
move => B L_AB. apply: leq_trans _ (dfa_prune_size _).
apply: leq_trans _ (minimize_size _). apply eq_leq.
apply: dfa_iso_size.
apply: coll_iso; auto using minimize_collapsed, dfa_prune_connected, minimize_connected.
move => w. by rewrite L_AB minimize_correct dfa_prune_correct.
Qed.
Lemma minimize_idem_size A : collapsed A -> #|A| = #|minimize A|.
Proof.
move => H. apply: leq_eq _ (minimize_size _).
apply: (card_leq_inj (_:injective (class A))).
move => x y. move: (H x y) => H1 H2. apply/H1.
apply/collP. by apply/class_eq.
Qed.
Lemma minimal_idem A : minimal A -> collapsed A.
Proof.
move => MA.
have S: surjective (class A).
- move => [x Hx]. exists x. apply/eqP. apply/val_inj.
rewrite /=. by rewrite -(eqP Hx).
have Bf: bijective (class A). apply: surj_card_bij => //.
- apply/eqP. rewrite eqn_leq minimize_size andbT.
exact: (MA (minimize A) (psym (minimize_correct _))).
move => x y. split.
- move/collP. move/class_eq.
by move/(bij_inj Bf).
- move => ->. apply/collP. exact: collb_refl.
Qed.
Lemma minimalP A : minimal A <-> (connected A /\ collapsed A).
Proof.
split.
- move => H. split. exact: minimal_connected. exact: minimal_idem.
- move => [H1 H2] B L_AB. rewrite minimize_idem_size //.
apply: minimize_minimal => // w. by rewrite minimize_correct.
Qed.
Lemma minimal_iso A B :
dfa_lang A =i dfa_lang B -> minimal A -> minimal B -> dfa_iso A B.
Proof. move => L_AB MA MB.
apply: coll_iso; auto using minimal_idem, minimal_connected.
Qed.
End FA.
Arguments delta [char] [A] x w.
Arguments dfa_run [char] [A] x w.