(* Author: Christian Doczkal *)
(* Distributed under the terms of CeCILL-B. *)
From Coq Require Import Omega.
From mathcomp Require Import all_ssreflect.
From RegLang Require Import misc setoid_leq languages dfa myhill_nerode two_way.
Set Default Proof Using "Type".
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* Distributed under the terms of CeCILL-B. *)
From Coq Require Import Omega.
From mathcomp Require Import all_ssreflect.
From RegLang Require Import misc setoid_leq languages dfa myhill_nerode two_way.
Set Default Proof Using "Type".
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Lemma contraN (b : bool) (P : Prop) : b -> ~~ b -> P. Proof. by case b. Qed.
Lemma inord_inj n m : n <= m -> injective (@inord m \o @nat_of_ord n.+1).
Proof.
move => Hnm k k' /= /(f_equal (@nat_of_ord _)) E. apply/ord_inj.
rewrite !inordK // in E; exact: leq_trans (ltn_ord _) _.
Qed.
Lemmas for character lookups on composite words
Lemma tnthL (T:eqType) (x z : seq T) (i : 'I_(size x)) (j : 'I_(size (x++z))) :
i = j :> nat -> tnth (in_tuple x) i = tnth (in_tuple (x++z)) j.
Proof.
move => e. pose a := tnth (in_tuple x) i.
by rewrite !(tnth_nth a) /= -e nth_cat ltn_ord.
Qed.
Lemma tnthR (T:eqType) (x z : seq T) (i : 'I_(size z)) (j : 'I_(size (x++z))) :
size x + i = j -> tnth (in_tuple z) i = tnth (in_tuple (x++z)) j.
Proof.
move => e. pose a := tnth (in_tuple z) i.
by rewrite !(tnth_nth a) /= -e nth_cat ltnNge leq_addr /= addKn.
Qed.
Wrapper for omega that uses ssreflects operators on nat
Ltac norm := rewrite ?(size_cat,cats0); simpl in *.
Ltac normH := match goal with [ H : is_true (_ <= _) |- _] => move/leP : H end.
Ltac somega :=
try (try (apply/andP; split); apply/leP; repeat normH; norm ; rewrite ?addnE /addn_rec ; intros; omega).
Section NFA2toAFA.
Variables (char : finType) (M : nfa2 char).
Implicit Types (x y z w v : word char).
We fix some 2NFA M. Instead of directly defining a DFA for M, we
instantiate the construction of DFAs from classifiers. This means that we have
to give a finite type Q and define a function T : word char -> Q which is
right congruent and refines the language of M. We take Q to be the type of
tables or black-box results for M.
We define the mapping from word char to table using a restriction of the
step relation. The stop relation srel k x behaves like step x except that
it does not continue if the head is at position k.
Definition srel (k:nat) x (c d : nfa2_config M x) := (step M x c d) && (k != c.2).
Arguments srel : clear implicits.
Lemma srel_step k w : subrel (srel k w) (step M w).
Proof. by move => c d /= => /andP[->]. Qed.
Lemma srel_step_max x : srel (size x).+2 x =2 step M x.
Proof. move => c d /=. by rewrite /srel neq_ltn ltn_ord orbT andbT. Qed.
Definition Tab x : table :=
([set q | connect (srel (size x).+1 x) (nfa2_s M, ord1) (q,ord_max)],
[set pq | connect (srel (size x).+1 x) (pq.1,inord (size x)) (pq.2,ord_max)]).
To show that Tab is right-congruent and refines the language of M, we
need to make use of the fact that M moves its head only one step at a
time. In particular, this allows us to split runs starting with head position
i and ending at head position j at any position k in beteen.
Lemma srelLR k x p i q j : srel k x (p,i) (q,j) ->
j.+1 = i :> nat \/ j = i.+1 :> nat.
Proof. move/srel_step. case/orP => /andP [_ /eqP ->]; tauto. Qed.
Lemma srel1 k x c d : srel k x c d -> d.2 <= c.2.+1.
Proof. move: c d => [p i] [q j] /srelLR [<-|->] //=. by somega. Qed.
Lemma srelSr k' k x (c d : nfa2_config M x) : c.2 < k ->
srel k x c d = srel (k+k') x c d.
Proof. move => lt_k. by rewrite /srel !neq_ltn ltn_addr lt_k ?orbT. Qed.
Lemma srelS k x p q (i j : pos x) m : i <= k ->
connect (srel k x) (p,i) (q,j) -> connect (srel (k+m) x) (p,i) (q,j).
Proof.
move => H /connectP [cs].
elim: cs p i H => [/= p i H _ [-> ->] //|[p' i'] cs IH p i H /= /andP [s pth] l].
have Hk: i < k. case/andP : s => _ /= s. by rewrite ltn_neqAle H eq_sym s.
apply: (connect_trans (y := (p',i'))) (connect1 _) _; first by rewrite -srelSr.
apply: IH => //. move/srel1 : s Hk => /= s. exact: leq_trans.
Qed.
Lemma srel_mid_path (k k' : nat) x (i j : pos x) (p q : M) cs :
i <= k <= j -> path (srel k' x) (p,i) cs -> (q,j) = last (p,i) cs ->
exists p' cl cr, [/\ cs = cl ++ cr, (p',inord k) = last (p,i) cl & path (srel k x) (p,i) cl].
Proof.
move: cs p i. apply: (size_induction (measure := size)) => cs IH p i /andP [H1 H2].
case: (boolP (i == k :> nat)) => Ei.
- exists p. exists [::]. exists cs. by rewrite -[i]inord_val (eqP Ei).
- destruct cs as [|c cs] => [_ /= [_ E]|/= /andP [s p1] p2]; subst.
+ by rewrite eqn_leq H1 H2 in Ei.
+ have Hi: i < k by rewrite ltn_neqAle Ei H1.
have mid: c.2 <= k <= j by rewrite (leq_trans (srel1 s)).
case: (IH cs _ c.1 _ mid) ; rewrite -?surjective_pairing //.
move => p' [cl] [cr] [C1 C2 C3]. exists p'. exists (c::cl). exists cr.
rewrite /= -C1 C3 andbT. split => //. rewrite /srel /= eq_sym Ei andbT.
exact: srel_step s.
Qed.
Lemma srel_mid (k k' : nat) x (i j : pos x) (p q : M) : i <= k <= j -> k <= k' ->
reflect (exists2 p', connect (srel k x) (p,i) (p',inord k) & connect (srel k' x) (p',inord k) (q,j))
(connect (srel k' x) (p,i) (q,j)).
Proof.
move => H X. apply: (iffP idP).
- case/connectP => cs c1 c2. case: (srel_mid_path H c1 c2) => [p'] [cl] [cr] [Ecs L C].
subst cs. rewrite cat_path last_cat -L in c1 c2. case/andP : c1 => ? c1. exists p'.
+ apply/connectP. by exists cl.
+ apply/connectP. by exists cr.
- case/andP: H => H1 H2 [p']. move/(srelS (k'-k) H1). rewrite subnKC //. exact: connect_trans.
Qed.
Lemma readL x z (p:M) (k : pos x) : k != (size x).+1 :> nat ->
read p (inord k : pos (x++z)) = read p k.
Proof.
move => Hk. rewrite /read. case: (ord2P k) => [/eqP->|E|i Hi].
- by rewrite /= -inord0 ord2P0.
- apply: contraN Hk. by rewrite (eqP E).
- have oi : i < size (x++z) by rewrite size_cat ltn_addr.
have H_eq: (Ordinal oi).+1 = (inord k : pos (x++z)). by rewrite -Hi inordK // ; somega.
by rewrite (ord2PC H_eq) -(tnthL (i := i)).
Qed.
Section CompositeWord.
Variables (x z : word char).
We first show that runs on x that do not cross the boundary between
x and z do not depend on z.
Lemma srelL (i j : pos x) p q :
srel (size x).+1 x (p,i) (q,j) = srel (size x).+1 (x++z) (p,inord i) (q,inord j).
Proof.
case: (boolP (i == (size x).+1 :> nat)) => Hi.
- rewrite /srel (eqP Hi) /= inordK ?eqxx //= ?andbF //; somega.
- have Hi' : i < (size x).+1. by rewrite ltn_neqAle Hi -ltnS ltn_ord.
rewrite /srel /step readL // !inordK //; somega.
move: (ltn_ord j) => ?. somega.
Qed.
Lemma runL (i j : pos x) p q :
connect (srel (size x).+1 x) (p,i) (q,j) =
connect (srel (size x).+1 (x++z)) (p,inord i) (q,inord j).
Proof.
pose f (c : nfa2_config M x) : nfa2_config M (x ++ z) := (c.1, inord c.2).
rewrite -[(p,inord i)]/(f (p,i)) -[(q,inord j)]/(f (q,j)).
apply: connect_transfer => //.
- move => {p q i j} [p i] [q j] /= [->] /inord_inj.
case/(_ _)/Wrap => [|->//]. somega.
- move => [? ?] [? ?]. rewrite /f /=. exact: srelL.
- move => {p q i j} [p i] [q j] step. exists (q,inord j).
rewrite /f /= inordK ?inord_val //. move: (srel1 step) => /= Hs.
case/andP : step => /= _ Hi. rewrite (leqRW Hs) ltn_neqAle eq_sym Hi /=.
by rewrite inordK ltnS ?leq_ord // (leqRW (leq_ord i)) ltnS size_cat leq_addr.
Qed.
This entails, that the behaviour of M starting from the endpoints of
x is also independent of z. Note that the direction from right to left
makes use of lemma term_uniq
Lemma Tab1P q : q \in (Tab x).1
<-> connect (srel (size x).+1 (x++z)) (nfa2_s M,ord1) (q,inord (size x).+1).
Proof. by rewrite /Tab inE runL /= -[ord1]inord_val. Qed.
Lemma Tab2P p q : (p,q) \in (Tab x).2
<-> connect (srel (size x).+1 (x++z)) (p,inord (size x)) (q,inord (size x).+1).
Proof. by rewrite inE runL /= inordK. Qed.
Dually, steps on the right of x++z do not depend on x, if they do not
cross the boundary between x and z.
Lemma readR (q:M) k : k != 0 -> k < (size z).+2 ->
read q (inord k : pos z) = read q (inord (size x + k) : pos (x++z)).
Proof.
move => Hk0 Hk. rewrite /read. case: (ord2P _) => [H|H|i Hi].
- apply: contraN Hk0.
move/eqP/(f_equal (@nat_of_ord _)) : H => /=. by rewrite inordK // => ->.
- by rewrite -[k](@inordK (size z).+1) ?(eqP H) //= addnS -size_cat -inord_max ord2PM.
- have Hi' : size x + i < size (x ++ z) by rewrite size_cat ltn_add2l.
have X: (Ordinal Hi').+1 = (inord (size x + k) : pos (x ++ z)).
by rewrite /= -addnS Hi !inordK //; somega.
by rewrite (ord2PC X) -(tnthR (i := i)).
Qed.
Lemma srelR (m k k' : nat) p p' : k != 0 -> k < (size z).+2 -> k' < (size z).+2 ->
srel ((size x).+1 + m) (x++z) (p,inord (size x + k)) (p',inord (size x + k'))
= srel m.+1 z (p,inord k) (p',inord k').
Proof.
move => Hk0 Hk Hk'. rewrite /srel /= !inordK ?addSnnS ?eqn_add2l //; somega.
case: (_ != _); rewrite ?andbT ?andbF // /step -?readR //.
rewrite !inordK //; somega. by rewrite -!addnS !eqn_add2l.
Qed.
Lemma srelRE m k p c : k < (size z).+2 -> k != 0 ->
srel m (x++z) (p,inord (size x + k)) c ->
exists q k', k' < (size z).+2 /\ c = (q,inord (size x + k')).
Proof.
move: k c => [//|k] [q j] Hk _ /srelLR [/eqP C|/eqP C];
exists q; rewrite inordK addnS ?eqSS in C; somega.
- exists k. by rewrite ltnW // -[j]inord_val (eqP C).
- exists k.+2. rewrite !addnS -[j]inord_val (eqP C). split => //.
rewrite eqn_leq in C. case/andP : C => _ C.
move: (leq_ltn_trans C (ltn_ord j)).
by rewrite size_cat -!addnS leq_add2l.
Qed.
End CompositeWord.
The main lemma used both in the proof of right-congruence and language
refinement states that as long as the black-box results for x and y
agreee, runs starting and ending on the right of composite words x++z and
y++z behave the same even if they cross the boundaries.
Lemma runR x y z p q (i j: nat) k :
Tab x = Tab y -> i <= (size z).+1 -> 0 < j <= (size z).+1 ->
connect (srel ((size x).+1 + k) (x++z)) (p,inord (size x + i)) (q,inord (size x + j)) ->
connect (srel ((size y).+1 + k) (y++z)) (p,inord (size y + i)) (q,inord (size y + j)).
Proof.
move => Tab_eq Hi /andP [Hj0 Hj]. case/connectP => cs. move: cs i Hi p.
apply: (size_induction (measure := size)) => /= cs IH i Hi p.
case: (boolP (i == 0)) => Hi0.
- rewrite (eqP Hi0) !addn0 => p1 p2.
case: (srel_mid_path (k := (size x).+1) _ p1 p2); try solve [rewrite inordI; somega].
apply/andP; split; rewrite !inordK; somega. move => p' [cl] [cr] [Ecs Lcl Pcl].
apply/(@srel_mid (size y).+1) ; try solve [rewrite !inordK; somega|rewrite -addn1; somega].
+ exists p'. apply/Tab2P. rewrite -Tab_eq. apply/Tab2P. by apply/connectP; exists cl.
+ subst cs. rewrite -[_.+1 as X in inord X]addn1.
apply: (IH cr) => {IH} //; somega.
* destruct cl as [|c cs]; simpl in *. case: Lcl => _.
-- move/(f_equal (@nat_of_ord _)); rewrite ?inordK; intros; somega.
-- by rewrite[size (cs ++ cr)]size_cat -addnS leq_addl.
* rewrite cat_path -Lcl addn1 in p1 *. by case/andP : p1.
* by rewrite p2 last_cat -Lcl addn1.
- destruct cs as [|c cs]; simpl in *.
+ move => _ [-> /(f_equal (@nat_of_ord _))/eqP].
rewrite !inordK ?eqn_add2l ?size_cat -?addnS ?leq_add2l // => /eqP ->.
exact: connect0.
+ case/andP => P1 P2 L. case/srelRE: (P1) => // p' [ip] [Hip ?]; subst.
rewrite srelR // -(@srelR y z) // in P1. apply: connect_trans (connect1 P1) _.
exact: (IH cs).
Qed.
Variant of the lemma above, that generales equality subgoals
Lemma runR_eq x y z p q (i j: nat) k xk xi xj yk yi yj :
Tab x = Tab y -> i <= (size z).+1 -> 0 < j <= (size z).+1 ->
xk = (size x).+1 + k -> xi = size x + i -> xj = size x + j ->
yk = (size y).+1 + k -> yi = size y + i -> yj = size y + j ->
connect (srel xk (x++z)) (p,inord xi) (q,inord xj) ->
connect (srel yk (y++z)) (p,inord yi) (q,inord yj).
Proof. move => ? ? ? ? ? ? ? ? ?. subst. exact: runR. Qed.
Lemma Tab_refines : refines (nfa2_lang M) Tab.
Proof.
move => x y E.
wlog suff W: x y E / (x \in nfa2_lang M) -> (y \in nfa2_lang M).
{ by apply/idP/idP; exact: W. }
case/exists_inP => f Hq1 Hq2. apply/exists_inP; exists f => //. move: Hq2.
rewrite -[x]cats0 -[y]cats0 -!(eq_connect (@srel_step_max _)).
case/(@srel_mid (size x).+1); somega => q /Tab1P q1 q2.
apply/(@srel_mid (size y).+1); somega.
- exists q. apply/Tab1P. by rewrite -E.
- move: q2 => {q1}. rewrite !inord_max.
apply: (runR_eq (i := 1) (j := 1) (k := 1)); rewrite ?addn1 ?cats0 //=.
Qed.
Lemma Tab_rc : right_congruent Tab.
Proof.
move => x y a E.
have Tab2 : (Tab (x ++ [:: a])).2 = (Tab (y ++ [:: a])).2.
{ apply/setP => [[p q]]. rewrite /Tab !inE /= !inord_max.
apply/idP/idP; apply: (runR_eq (i := 1) (j := 2) (k := 1)); by rewrite ?size_cat ?addn1 ?addn2. }
suff ?: (Tab (x ++ [:: a])).1 = (Tab (y ++ [:: a])).1 by congr pair.
apply/setP => q /=. rewrite !inE.
pose C x := connect (srel (size (x ++ [:: a])).+1 (x ++ [:: a])) (nfa2_s M, ord1) (q, ord_max).
wlog suff W: x y E Tab2 / C x -> C y; [by apply/idP/idP; exact: W|].
case/(@srel_mid (size x).+1); somega => p /Tab1P p1 p2.
apply/(@srel_mid (size y).+1); somega.
exists p; first by apply/Tab1P; rewrite -E. move: p2.
rewrite -![_.+1 as X in inord X]addn1 -[1]/(size [:: a]) -!size_cat.
rewrite !(@runL _ [::]) !inordK; somega. move/Tab2P => p2. by apply/Tab2P; rewrite -Tab2.
Qed.
Definition nfa2_to_classifier : classifier_for (nfa2_lang M) :=
{| cf_classifier := Classifier Tab; cf_congruent := Tab_rc; cf_refines := Tab_refines |}.
Theorem nfa2_to_dfa :
{ A : dfa char | dfa_lang A =i nfa2_lang M & #|A| <= 2 ^ (#|M| ^ 2 + #|M|) }.
Proof.
exists (classifier_to_dfa (nfa2_to_classifier)); first exact: classifier_to_dfa_correct.
rewrite card_sub (leqRW (max_card _)) [#|_|]/=.
by rewrite card_prod expnD mulnC leq_mul //= card_set // card_prod -mulnn.
Qed.
End NFA2toAFA.
Tab x = Tab y -> i <= (size z).+1 -> 0 < j <= (size z).+1 ->
xk = (size x).+1 + k -> xi = size x + i -> xj = size x + j ->
yk = (size y).+1 + k -> yi = size y + i -> yj = size y + j ->
connect (srel xk (x++z)) (p,inord xi) (q,inord xj) ->
connect (srel yk (y++z)) (p,inord yi) (q,inord yj).
Proof. move => ? ? ? ? ? ? ? ? ?. subst. exact: runR. Qed.
Lemma Tab_refines : refines (nfa2_lang M) Tab.
Proof.
move => x y E.
wlog suff W: x y E / (x \in nfa2_lang M) -> (y \in nfa2_lang M).
{ by apply/idP/idP; exact: W. }
case/exists_inP => f Hq1 Hq2. apply/exists_inP; exists f => //. move: Hq2.
rewrite -[x]cats0 -[y]cats0 -!(eq_connect (@srel_step_max _)).
case/(@srel_mid (size x).+1); somega => q /Tab1P q1 q2.
apply/(@srel_mid (size y).+1); somega.
- exists q. apply/Tab1P. by rewrite -E.
- move: q2 => {q1}. rewrite !inord_max.
apply: (runR_eq (i := 1) (j := 1) (k := 1)); rewrite ?addn1 ?cats0 //=.
Qed.
Lemma Tab_rc : right_congruent Tab.
Proof.
move => x y a E.
have Tab2 : (Tab (x ++ [:: a])).2 = (Tab (y ++ [:: a])).2.
{ apply/setP => [[p q]]. rewrite /Tab !inE /= !inord_max.
apply/idP/idP; apply: (runR_eq (i := 1) (j := 2) (k := 1)); by rewrite ?size_cat ?addn1 ?addn2. }
suff ?: (Tab (x ++ [:: a])).1 = (Tab (y ++ [:: a])).1 by congr pair.
apply/setP => q /=. rewrite !inE.
pose C x := connect (srel (size (x ++ [:: a])).+1 (x ++ [:: a])) (nfa2_s M, ord1) (q, ord_max).
wlog suff W: x y E Tab2 / C x -> C y; [by apply/idP/idP; exact: W|].
case/(@srel_mid (size x).+1); somega => p /Tab1P p1 p2.
apply/(@srel_mid (size y).+1); somega.
exists p; first by apply/Tab1P; rewrite -E. move: p2.
rewrite -![_.+1 as X in inord X]addn1 -[1]/(size [:: a]) -!size_cat.
rewrite !(@runL _ [::]) !inordK; somega. move/Tab2P => p2. by apply/Tab2P; rewrite -Tab2.
Qed.
Definition nfa2_to_classifier : classifier_for (nfa2_lang M) :=
{| cf_classifier := Classifier Tab; cf_congruent := Tab_rc; cf_refines := Tab_refines |}.
Theorem nfa2_to_dfa :
{ A : dfa char | dfa_lang A =i nfa2_lang M & #|A| <= 2 ^ (#|M| ^ 2 + #|M|) }.
Proof.
exists (classifier_to_dfa (nfa2_to_classifier)); first exact: classifier_to_dfa_correct.
rewrite card_sub (leqRW (max_card _)) [#|_|]/=.
by rewrite card_prod expnD mulnC leq_mul //= card_set // card_prod -mulnn.
Qed.
End NFA2toAFA.
If M is determinististic, the size bound on the constructed 2DFA improves
to (#|M|.+1)^(#|M|.+1)
Section DFA2toAFA.
Variables (char : finType) (M : dfa2 char).
Lemma functional_srel k w : functional (srel M k w).
Proof. apply: functional_sub (@srel_step _ _ k w). exact: step_fun. Qed.
Lemma term_srel k x q (H: k < (size x).+2) : terminal (srel M k x) (q,inord k).
Proof. move => c /=. by rewrite /srel inordK // ?eqxx /= andbF. Qed.
Lemma Tab1_uniq x p q : p \in (Tab M x).1 -> q \in (Tab M x).1 -> p = q.
Proof.
rewrite !inE => H1 H2. suff: (p,@ord_max (size x).+1) = (q,ord_max) by case.
apply: term_uniq H1 H2; rewrite ?inord_max; auto using term_srel, functional_srel.
Qed.
Lemma Tab2_functional x p q r : (p,q) \in (Tab M x).2 -> (p,r) \in (Tab M x).2 -> q = r.
Proof.
rewrite !inE => /= H1 H2. suff: (q,@ord_max (size x).+1) = (r,ord_max) by case.
apply: term_uniq H1 H2; rewrite ?inord_max; auto using term_srel, functional_srel.
Qed.
Definition Tab' := image_fun (@Tab_rc _ M).
Lemma image_rc : right_congruent Tab'.
Proof. move => x y a /Sub_eq E. apply/Sub_eq. exact: Tab_rc. Qed.
Lemma image_refines : refines (nfa2_lang M) Tab'.
Proof. move => x y /Sub_eq E. exact: Tab_refines. Qed.
Definition dfa2_to_myhill :=
{| cf_classifier := Classifier Tab';
cf_congruent := image_rc;
cf_refines := image_refines |}.
Lemma det_range : #|{:image_type (@Tab_rc _ M)}| <= (#|M|.+1)^(#|M|.+1).
Proof.
pose table' := (option M * {ffun M -> option M})%type.
apply: (@leq_trans #|{: table'}|); last by rewrite card_prod card_ffun !card_option expnS.
pose f (x : image_type (@Tab_rc _ M)) : table' :=
let (b,_) := x in ([pick q | q \in b.1],[ffun p => [pick q | (p,q) \in b.2]]).
suff : injective f by apply: card_leq_inj.
move => [[a1 a2] Ha] [[b1 b2] Hb] [E1 /ffunP E2]. apply/Sub_eq.
move: Ha Hb => /dec_eq /= [x Hx] /dec_eq [y Hy].
rewrite [Tab M x]surjective_pairing [Tab M y]surjective_pairing !xpair_eqE in Hx Hy.
case/andP : Hx => /eqP ? /eqP ?. case/andP : Hy => /eqP ? /eqP ?. subst. f_equal.
- apply/setP => p. case: (pickP _) E1 => q1; case: (pickP _) => q2 //; last by rewrite q1 q2.
move => {E2} H1 H2 [?]; subst.
wlog suff S : p x y H1 H2 / (p \in (Tab M x).1) -> (p \in (Tab M y).1).
{ apply/idP/idP; exact: S. }
move => H. by rewrite (@Tab1_uniq x p q2).
- apply/setP => [[p q]]. move: E2 {E1} => /(_ p). rewrite !ffunE.
case: (pickP _) => r1; case: (pickP _) => r2 //; last by rewrite r1 r2.
move => H1 H2 [?]; subst. apply/idP/idP => ?.
+ by rewrite (@Tab2_functional x p q r2).
+ by rewrite (@Tab2_functional y p q r2).
Qed.
Theorem dfa2_to_dfa :
{ A : dfa char | dfa_lang A =i dfa2_lang M & #|A| <= (#|M|.+1)^(#|M|.+1) }.
Proof.
exists (classifier_to_dfa (dfa2_to_myhill)); first exact: classifier_to_dfa_correct.
rewrite card_sub (leqRW (max_card _)). exact: det_range.
Qed.
End DFA2toAFA.