Authors: Christian Doczkal and Jan-Oliver Kaiser
Require Import ssreflect ssrbool ssrnat fintype eqtype seq ssrfun ssrbool finset choice finfun.
Require Import automata misc regexp.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Import automata misc regexp.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Record finPar := {
finpar_classes : finType;
finpar_fun :> word -> finpar_classes;
finpar_surj : surjective finpar_fun
}.
We register an additional coercion. So we can write
- x:E => x is a class of E
- E w => the class of w
- #|E| => the cardinality of the index type
Coercion finpar_classes : finPar >-> finType.
Coercion finpar_surj : finPar >-> surjective.
Definition right_congruent (X : eqType) (E : word -> X) :=
forall u v a, E u = E v -> E (u ++ [::a]) = E (v ++ [::a]).
Definition refines (X: eqType) (L : dlang char) (E : word -> X) :=
forall u v, E u = E v -> (u \in L) = (v \in L).
Record myhillPar L := {
myhill_rel :> finPar;
myhill_congruent : right_congruent myhill_rel;
myhill_refines : refines L myhill_rel
}.
Lemma myhill_lang_eq_proof L1 L2 (M1 : myhillPar L1) : L1 =i L2 -> refines L2 M1.
Proof. move => H0 u v /myhill_refines. by rewrite -!H0. Qed.
Definition myhill_lang_eq L1 L2 M1 (H : L1 =i L2) := {|
myhill_congruent := @myhill_congruent L1 M1;
myhill_refines := myhill_lang_eq_proof H
|}.
Definition nerode_spec (L : dlang char) u v :=
forall w, u++w \in L = (v++w \in L).
Definition nerode (X : eqType) (L : dlang char) (E : word -> X) :=
forall u v, E u = E v <-> forall w, (u++w \in L) = (v++w \in L).
Record nerodePar L := {
nerode_par :> finPar;
nerodeP : nerode L nerode_par
}.
Nerode partitions can be seen as a special case of Myhill partitions.
We make this explicit by defining a coercion from Nerode partitions
to Myhill partitons. This way we only need one set of lemmas for
cr (see below).
Lemma nerode_right_congruent L (N : nerodePar L) : right_congruent N.
Proof. move => u v a /nerodeP H. apply/nerodeP => w. by rewrite -!catA. Qed.
Lemma nerode_refines L (N : nerodePar L) : refines L N.
Proof. move => u v /nerodeP H. by rewrite -[u]cats0 -[v]cats0. Qed.
Definition nerode_to_myhill L (N : nerodePar L) := {|
myhill_congruent := @nerode_right_congruent L N;
myhill_refines := @nerode_refines L N |}.
Arguments myhill_congruent [L M u v a] H: rename.
Arguments myhill_refines [L M u v] H: rename.
Arguments nerodeP [L] N u v: rename.
Lemma myhill_nerode_spec L (M : myhillPar L) u v :
M u = M v -> forall w, (u++w \in L) = (v ++ w \in L).
Proof. move => H w.
elim: w v u H => [|a w IHw] v u H.
rewrite !cats0. exact: (myhill_refines H).
rewrite -cat1s !catA. apply IHw. exact: (myhill_congruent H).
Qed.
Lemma delta_s_right_congruent A : right_congruent (@delta_s _ A).
Proof. move => u v a H. rewrite /= /delta_s !delta_cat. by f_equal. Qed.
Lemma delta_s_refines A : refines (dfa_lang A) (@delta_s _ A).
Proof. move => u v H. rewrite !delta_accept. by f_equal. Qed.
Definition delta_s_finPar A (CA : connected A) :=
{| finpar_surj := CA |}.
We define two translations from DFAs to Myhill-Partitions.
The first translation only works for connected DFAs.
The advantage of dfac_to_myhill is that the index type
is convertible to the type of states of the input automaton.
The second conversion first prunes unreachable states and
therefore works an all DFAs.
Definition dfac_to_myhill (A : dfa char) (CA : connected A) := {|
myhill_congruent := @delta_s_right_congruent _;
myhill_refines := @delta_s_refines _;
myhill_rel := delta_s_finPar CA |}.
Definition dfa_to_myhill (A : dfa char) : myhillPar (dfa_lang A) :=
myhill_lang_eq (dfac_to_myhill (@dfa_prune_connected _ A))
(dfa_prune_correct A).
Lemma dfa_to_myhill_size A : #|A| >= #|dfa_to_myhill A|.
Proof. exact: dfa_prune_size. Qed.
Conversion from Myhill partitons to DFAS.
Definition fp_trans (E : finPar) (x : E) a := E (cr E x ++ [:: a]).
Definition myhill_to_dfa L (M : myhillPar L) :=
{| dfa_s := M [::]; dfa_fin x := cr M x \in L; dfa_trans := @fp_trans M |}.
Lemma myhill_to_dfa_delta L (M : myhillPar L) : @delta_s _ (myhill_to_dfa M) =1 M.
Proof.
apply: last_ind => [|w a IHw] //=.
rewrite /delta_s -cats1 delta_cat -!/(delta_s _ _) IHw.
by rewrite /delta /= /fp_trans (myhill_congruent (crK _)).
Qed.
Lemma myhill_to_dfa_correct L (M : myhillPar L) : dfa_lang (myhill_to_dfa M) =i L.
Proof. move => w.
rewrite delta_accept -!/(delta_s _ _) myhill_to_dfa_delta.
exact: (myhill_refines (crK _)).
Qed.
Lemma myhill_to_connected L (M : myhillPar L) : connected (myhill_to_dfa M).
Proof. apply/connectedP.
apply/forallP => x. apply/step_someP. exists (cr M x).
by rewrite -{2}[x](crK (Sf:=M)) -myhill_to_dfa_delta.
Qed.
Nerode partitions coerce to Myhill partitions and hence can be converted
the same way as Myhill partitions.
Definition nerode_to_dfa L (N : nerodePar L) := myhill_to_dfa (nerode_to_myhill N).
Lemma nerode_to_dfa_correct L (N : nerodePar L) : dfa_lang (nerode_to_dfa N) =i L.
Proof. exact: myhill_to_dfa_correct. Qed.
Lemma nerode_to_connected L (N : nerodePar L) : connected (nerode_to_dfa N).
Proof. exact: myhill_to_connected. Qed.
We can cast one Nerode partiton to a partiton for an equivalent language
Lemma nerode_eq_proof L1 L2 (N1 : nerodePar L1) : L1 =i L2 -> nerode L2 N1.
Proof. move => H0 u v. split => [/nerodeP H1 w|H1].
- by rewrite -!H0.
- apply/nerodeP => w. by rewrite !H0.
Qed.
Definition nerode_eq L1 L2 N1 (H : L1 =i L2) := {| nerodeP := nerode_eq_proof N1 H |}.
Minimal DFAs are connected and can therefore be cast to Nerode partitions.
Section mDFA_To_Nerode.
Variable A : dfa char.
Variable MA : minimal A.
Lemma minimal_nerode : nerode (dfa_lang A) (@delta_s _ A).
Proof.
move => u v. apply: iff_trans (iff_sym (minimal_idem MA _ _)) _.
by split => H w; move: (H w); rewrite -!delta_cat !delta_accept.
Qed.
Lemma minimal_surj : surjective (@delta_s _ A).
Proof.
move => x. exists (cr (minimal_connected MA) x).
by rewrite crK.
Qed.
Definition minimal_finPar := {| finpar_surj := minimal_surj |}.
End mDFA_To_Nerode.
Definition dfa_to_nerode A (MinA : minimal A) := {|
nerode_par := minimal_finPar MinA;
nerodeP := minimal_nerode MinA
|}.
End MyhillNerode.