Library fl.aut.myhill_nerode
Require Import automata misc regexp.
Require Import base.
Set Implicit Arguments.
Import Prenex Implicits.
Import Automata.
Lemma nand3P (b1 b2 b3: bool):
reflect (¬[\/ b1, b2 | b3]) [&& ~~ b1, ~~ b2 & ~~ b3].
Section MyhillNerode.
Variable char: finType.
Definition word:= word char.
Section Relations.
Variable L: language char.
(* We model finiteness of equivalence classes
by functions to some finType. *)
Definition surjective {X: finType} {Y} (f: Y → X) := ∀ x, ∃ w, f w == x.
Record Fin_Eq_Cls :=
{
fin_type : finType;
fin_func :> word → fin_type;
fin_surjective : surjective fin_func
}.
Section Inversion.
Variable f: Fin_Eq_Cls.
Definition cr (f: Fin_Eq_Cls) x := xchoose (fin_surjective f x).
Lemma crK: cancel (cr f) f.
(* Needed? *)
Lemma eq_cr x: x = (f (cr f x)).
End Inversion.
Section Myhill.
Definition right_congruent {X} (f: word → X) :=
∀ u v a, f u = f v → f (rcons u a) = f (rcons v a).
Definition refines {X} (f: word → X) :=
∀ u v, f u = f v → u \in L = (v \in L).
Record Myhill_Rel :=
{
myhill_func :> Fin_Eq_Cls;
myhill_congruent: right_congruent myhill_func;
myhill_refines: refines myhill_func
}.
End Myhill.
Definition suffix_equal u v :=
∀ w, u++w \in L = (v++w \in L).
Definition equiv_suffix {X} (f: word → X) :=
∀ u v, f u = f v ↔ suffix_equal u v.
Record Nerode_Rel :=
{
nerode_func :> Fin_Eq_Cls;
nerode_equiv: equiv_suffix nerode_func
}.
Lemma cr_rcons (f: Nerode_Rel) w a: f (rcons (cr f (f w)) a) = f (rcons w a).
Section Weak_Nerode.
Definition imply_suffix {X} (f: word → X) :=
∀ u v, f u = f v → suffix_equal u v.
Record Weak_Nerode_Rel :=
{
weak_nerode_func :> Fin_Eq_Cls;
weak_nerode_imply: imply_suffix weak_nerode_func
}.
End Weak_Nerode.
Section Weak_Nerode_Facts.
Variable f: Weak_Nerode_Rel.
Lemma cr_mem_L_cat u v: cr f (f u) ++ v \in L = (u ++ v \in L).
Lemma cr_mem_L w: cr f (f w) \in L = (w \in L).
End Weak_Nerode_Facts.
Definition nerode_weak_nerode (f: Nerode_Rel): Weak_Nerode_Rel :=
{| weak_nerode_imply := fun u v H ⇒ match nerode_equiv f u v with conj H0 H1 ⇒ H0 H end |}.
Coercion nerode_weak_nerode : Nerode_Rel >-> Weak_Nerode_Rel.
End Relations.
Section DFA_To_Myhill.
Variable A: dfa char.
Definition A_c := dfa_connected A.
Definition f_M := fun w ⇒ last (dfa_s A_c) (dfa_run A_c w).
Lemma f_M_surjective: surjective f_M.
Definition f_fin : Fin_Eq_Cls :=
{|
fin_func := f_M;
fin_surjective := f_M_surjective
|}.
Lemma f_M_right_congruent: right_congruent f_M.
Lemma f_M_refines: refines (dfa_lang A_c) f_M.
Definition dfa_to_myhill' : Myhill_Rel (dfa_lang A_c) :=
{|
myhill_func := f_fin;
myhill_congruent := f_M_right_congruent;
myhill_refines := f_M_refines
|}.
Lemma myhill_lang_eq L1 L2: L1 =i L2 → Myhill_Rel L1 → Myhill_Rel L2.
Lemma dfa_to_myhill : Myhill_Rel (dfa_lang A).
End DFA_To_Myhill.
Section Myhill_Weak_Nerode.
Variable L: language char.
Variable f: Myhill_Rel L.
Lemma myhill_suffix: imply_suffix L f.
Lemma myhill_to_weak_nerode: Weak_Nerode_Rel L.
End Myhill_Weak_Nerode.
Section Nerode_To_DFA.
Variable L: language char.
Variable f: Nerode_Rel L.
Definition nerode_to_dfa :=
{|
dfa_s := f [::];
dfa_fin := [pred x | cr f x \in L ];
dfa_step := [fun x a ⇒ f (rcons (cr f x) a)]
|}.
Lemma nerode_to_dfa_run w: last (f[::]) (dfa_run' nerode_to_dfa (f [::]) w) = f w.
Lemma nerode_to_dfa_correct: L =i dfa_lang nerode_to_dfa.
End Nerode_To_DFA.
Section Minimalization.
Variable L: language char.
Variable f_0: Weak_Nerode_Rel L.
Definition X := f_0.(fin_type).
Definition succ := [ fun x a ⇒ f_0 ((cr f_0 x) ++ [::a]) ].
Definition psucc := [ fun x y ⇒ [ fun a ⇒ (succ x a, succ y a) ] ].
Definition distinguishable := [ fun x y ⇒ (cr f_0 x) \in L != ((cr f_0 y) \in L) ].
Definition dist0 := [set x | distinguishable x.1 x.2 ].
Lemma dist0P x:
reflect (cr f_0 x.1 \in L ≠ (cr f_0 x.2 \in L))
(x \in dist0).
Lemma dist0NP x:
reflect (cr f_0 x.1 \in L = (cr f_0 x.2 \in L))
(x \notin dist0).
Definition distS (dist: {set X×X}) :=
[set (x,y) | x in X, y in X & [ ∃ a, psucc x y a \in dist ] ].
Lemma distSP (dist: {set X×X}) x y:
reflect (∃ a, psucc x y a \in dist)
((x,y) \in distS dist).
Lemma distSNP (dist: {set X×X}) x y:
reflect (∀ a, psucc x y a \notin dist)
((x,y) \notin distS dist).
Definition one_step_dist dist := dist0 :|: dist :|: (distS dist).
Lemma one_step_distP (dist: {set X×X}) x:
reflect ([\/ x \in dist0, x \in dist | x \in distS dist])
(x \in one_step_dist dist).
Lemma one_step_distNP (dist: {set X×X}) x:
reflect ([/\ x \notin dist0, x \notin dist & x \notin distS dist])
(x \notin one_step_dist dist).
Definition distinct := lfp one_step_dist.
Notation "x ~!= y" := ((x,y) \in distinct) (at level 70, no associativity).
Notation "u ~!=_f_0 v" := (f_0(u) ~!= f_0(v)) (at level 70, no associativity).
Notation "x ~= y" := ((x,y) \notin distinct) (at level 70, no associativity).
Notation "u ~=_f_0 v" := (f_0(u) ~= f_0(v)) (at level 70, no associativity).
Lemma distS_mono: mono distS.
Lemma one_step_dist_mono: mono one_step_dist.
Lemma equiv0_refl x:
(x,x) \notin dist0.
Lemma equiv_refl x: x ~= x.
Lemma dist_sym x y: distinguishable x y → distinguishable y x.
Lemma not_dist_sym x y: ~~ distinguishable x y → ~~ distinguishable y x.
Lemma equiv0_sym x y: (x,y) \notin dist0 → (y,x) \notin dist0.
Lemma dist0_sym x y: (x,y) \in dist0 → (y,x) \in dist0.
Lemma equiv_sym x y: x ~= y → y ~= x.
Lemma equiv_trans x y z: x ~= y → y ~= z → x ~= z.
Lemma equiv_suffix_equal u v: u ~=_f_0 v → suffix_equal L u v.
Lemma distinct_not_suffix_equal u v:
u ~!=_f_0 v →
∃ w, u ++ w \in L != (v ++ w \in L).
Lemma equivP u v:
reflect (suffix_equal L u v)
(u ~=_f_0 v).
Definition equiv_repr x := [set y | x ~= y].
Lemma equiv_repr_refl x : x \in equiv_repr x.
Definition X_min := map equiv_repr (enum (fin_type f_0)).
Lemma equiv_repr_mem x: equiv_repr x \in X_min.
Definition f_min w := SeqSub (equiv_repr_mem (f_0 w)).
Lemma f_minP u v:
reflect (f_min u = f_min v)
(u ~=_f_0 v).
Lemma f_min_correct: equiv_suffix L f_min.
Lemma f_min_surjective: surjective f_min.
Definition f_min_fin: Fin_Eq_Cls :=
{| fin_surjective := f_min_surjective |}.
Lemma weak_nerode_to_nerode: Nerode_Rel L.
End Minimalization.
End MyhillNerode.
Require Import base.
Set Implicit Arguments.
Import Prenex Implicits.
Import Automata.
Lemma nand3P (b1 b2 b3: bool):
reflect (¬[\/ b1, b2 | b3]) [&& ~~ b1, ~~ b2 & ~~ b3].
Section MyhillNerode.
Variable char: finType.
Definition word:= word char.
Section Relations.
Variable L: language char.
(* We model finiteness of equivalence classes
by functions to some finType. *)
Definition surjective {X: finType} {Y} (f: Y → X) := ∀ x, ∃ w, f w == x.
Record Fin_Eq_Cls :=
{
fin_type : finType;
fin_func :> word → fin_type;
fin_surjective : surjective fin_func
}.
Section Inversion.
Variable f: Fin_Eq_Cls.
Definition cr (f: Fin_Eq_Cls) x := xchoose (fin_surjective f x).
Lemma crK: cancel (cr f) f.
(* Needed? *)
Lemma eq_cr x: x = (f (cr f x)).
End Inversion.
Section Myhill.
Definition right_congruent {X} (f: word → X) :=
∀ u v a, f u = f v → f (rcons u a) = f (rcons v a).
Definition refines {X} (f: word → X) :=
∀ u v, f u = f v → u \in L = (v \in L).
Record Myhill_Rel :=
{
myhill_func :> Fin_Eq_Cls;
myhill_congruent: right_congruent myhill_func;
myhill_refines: refines myhill_func
}.
End Myhill.
Definition suffix_equal u v :=
∀ w, u++w \in L = (v++w \in L).
Definition equiv_suffix {X} (f: word → X) :=
∀ u v, f u = f v ↔ suffix_equal u v.
Record Nerode_Rel :=
{
nerode_func :> Fin_Eq_Cls;
nerode_equiv: equiv_suffix nerode_func
}.
Lemma cr_rcons (f: Nerode_Rel) w a: f (rcons (cr f (f w)) a) = f (rcons w a).
Section Weak_Nerode.
Definition imply_suffix {X} (f: word → X) :=
∀ u v, f u = f v → suffix_equal u v.
Record Weak_Nerode_Rel :=
{
weak_nerode_func :> Fin_Eq_Cls;
weak_nerode_imply: imply_suffix weak_nerode_func
}.
End Weak_Nerode.
Section Weak_Nerode_Facts.
Variable f: Weak_Nerode_Rel.
Lemma cr_mem_L_cat u v: cr f (f u) ++ v \in L = (u ++ v \in L).
Lemma cr_mem_L w: cr f (f w) \in L = (w \in L).
End Weak_Nerode_Facts.
Definition nerode_weak_nerode (f: Nerode_Rel): Weak_Nerode_Rel :=
{| weak_nerode_imply := fun u v H ⇒ match nerode_equiv f u v with conj H0 H1 ⇒ H0 H end |}.
Coercion nerode_weak_nerode : Nerode_Rel >-> Weak_Nerode_Rel.
End Relations.
Section DFA_To_Myhill.
Variable A: dfa char.
Definition A_c := dfa_connected A.
Definition f_M := fun w ⇒ last (dfa_s A_c) (dfa_run A_c w).
Lemma f_M_surjective: surjective f_M.
Definition f_fin : Fin_Eq_Cls :=
{|
fin_func := f_M;
fin_surjective := f_M_surjective
|}.
Lemma f_M_right_congruent: right_congruent f_M.
Lemma f_M_refines: refines (dfa_lang A_c) f_M.
Definition dfa_to_myhill' : Myhill_Rel (dfa_lang A_c) :=
{|
myhill_func := f_fin;
myhill_congruent := f_M_right_congruent;
myhill_refines := f_M_refines
|}.
Lemma myhill_lang_eq L1 L2: L1 =i L2 → Myhill_Rel L1 → Myhill_Rel L2.
Lemma dfa_to_myhill : Myhill_Rel (dfa_lang A).
End DFA_To_Myhill.
Section Myhill_Weak_Nerode.
Variable L: language char.
Variable f: Myhill_Rel L.
Lemma myhill_suffix: imply_suffix L f.
Lemma myhill_to_weak_nerode: Weak_Nerode_Rel L.
End Myhill_Weak_Nerode.
Section Nerode_To_DFA.
Variable L: language char.
Variable f: Nerode_Rel L.
Definition nerode_to_dfa :=
{|
dfa_s := f [::];
dfa_fin := [pred x | cr f x \in L ];
dfa_step := [fun x a ⇒ f (rcons (cr f x) a)]
|}.
Lemma nerode_to_dfa_run w: last (f[::]) (dfa_run' nerode_to_dfa (f [::]) w) = f w.
Lemma nerode_to_dfa_correct: L =i dfa_lang nerode_to_dfa.
End Nerode_To_DFA.
Section Minimalization.
Variable L: language char.
Variable f_0: Weak_Nerode_Rel L.
Definition X := f_0.(fin_type).
Definition succ := [ fun x a ⇒ f_0 ((cr f_0 x) ++ [::a]) ].
Definition psucc := [ fun x y ⇒ [ fun a ⇒ (succ x a, succ y a) ] ].
Definition distinguishable := [ fun x y ⇒ (cr f_0 x) \in L != ((cr f_0 y) \in L) ].
Definition dist0 := [set x | distinguishable x.1 x.2 ].
Lemma dist0P x:
reflect (cr f_0 x.1 \in L ≠ (cr f_0 x.2 \in L))
(x \in dist0).
Lemma dist0NP x:
reflect (cr f_0 x.1 \in L = (cr f_0 x.2 \in L))
(x \notin dist0).
Definition distS (dist: {set X×X}) :=
[set (x,y) | x in X, y in X & [ ∃ a, psucc x y a \in dist ] ].
Lemma distSP (dist: {set X×X}) x y:
reflect (∃ a, psucc x y a \in dist)
((x,y) \in distS dist).
Lemma distSNP (dist: {set X×X}) x y:
reflect (∀ a, psucc x y a \notin dist)
((x,y) \notin distS dist).
Definition one_step_dist dist := dist0 :|: dist :|: (distS dist).
Lemma one_step_distP (dist: {set X×X}) x:
reflect ([\/ x \in dist0, x \in dist | x \in distS dist])
(x \in one_step_dist dist).
Lemma one_step_distNP (dist: {set X×X}) x:
reflect ([/\ x \notin dist0, x \notin dist & x \notin distS dist])
(x \notin one_step_dist dist).
Definition distinct := lfp one_step_dist.
Notation "x ~!= y" := ((x,y) \in distinct) (at level 70, no associativity).
Notation "u ~!=_f_0 v" := (f_0(u) ~!= f_0(v)) (at level 70, no associativity).
Notation "x ~= y" := ((x,y) \notin distinct) (at level 70, no associativity).
Notation "u ~=_f_0 v" := (f_0(u) ~= f_0(v)) (at level 70, no associativity).
Lemma distS_mono: mono distS.
Lemma one_step_dist_mono: mono one_step_dist.
Lemma equiv0_refl x:
(x,x) \notin dist0.
Lemma equiv_refl x: x ~= x.
Lemma dist_sym x y: distinguishable x y → distinguishable y x.
Lemma not_dist_sym x y: ~~ distinguishable x y → ~~ distinguishable y x.
Lemma equiv0_sym x y: (x,y) \notin dist0 → (y,x) \notin dist0.
Lemma dist0_sym x y: (x,y) \in dist0 → (y,x) \in dist0.
Lemma equiv_sym x y: x ~= y → y ~= x.
Lemma equiv_trans x y z: x ~= y → y ~= z → x ~= z.
Lemma equiv_suffix_equal u v: u ~=_f_0 v → suffix_equal L u v.
Lemma distinct_not_suffix_equal u v:
u ~!=_f_0 v →
∃ w, u ++ w \in L != (v ++ w \in L).
Lemma equivP u v:
reflect (suffix_equal L u v)
(u ~=_f_0 v).
Definition equiv_repr x := [set y | x ~= y].
Lemma equiv_repr_refl x : x \in equiv_repr x.
Definition X_min := map equiv_repr (enum (fin_type f_0)).
Lemma equiv_repr_mem x: equiv_repr x \in X_min.
Definition f_min w := SeqSub (equiv_repr_mem (f_0 w)).
Lemma f_minP u v:
reflect (f_min u = f_min v)
(u ~=_f_0 v).
Lemma f_min_correct: equiv_suffix L f_min.
Lemma f_min_surjective: surjective f_min.
Definition f_min_fin: Fin_Eq_Cls :=
{| fin_surjective := f_min_surjective |}.
Lemma weak_nerode_to_nerode: Nerode_Rel L.
End Minimalization.
End MyhillNerode.