Authors: Christian Doczkal and Jan-Oliver Kaiser
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype path fingraph tuple finfun finset.
Require Import misc regexp automata dfa_to_re.
Require Import misc regexp automata dfa_to_re.
Set Implicit Arguments.
Import Prenex Implicits.
For the closure under images of homomorpisms, we need regular expressions for strings.
Definition String (char : finType) (w : word char) :=
foldr Conc Eps [seq Atom a | a <- w].
Lemma StringE (char : finType) (w : word char) : String w =i pred1 w.
Section HomDef.
Variables (char char' : finType).
Variable (h : seq char -> seq char').
Definition homomorphism := forall w1 w2, h (w1 ++ w2) = h w1 ++ h w2.
Hypothesis h_hom : homomorphism.
Lemma h0 : h [::] = [::].
Lemma h_seq w : h w = flatten [seq h [:: a] | a <- w].
Lemma h_flatten vv : h (flatten vv) = flatten (map h vv).
End HomDef.
Implicit Arguments homomorphism [char char'].
Section Homomorphism.
Variables (char char' : finType).
Definition image (h : word char -> word char') (L : word char -> Prop) v :=
exists w, L w /\ h w = v.
Definition preimage (h : word char -> word char') (L : word char' -> Prop) v :=
L (h v).
Lemma image_ext L1 L2 h w :
(forall v, L1 v <-> L2 v) -> (image h L1 w <-> image h L2 w).
Variable (h : seq char -> seq char').
Hypothesis h_hom : homomorphism h.
Definition dfa_preim (A : dfa char') : dfa char :=
{| dfa_s := dfa_s A;
dfa_fin := dfa_fin A;
dfa_trans x a := delta x (h [:: a]) |}.
Lemma dfa_preim_aux A w: delta_s (dfa_preim A) w = delta_s A (h w).
Lemma dfa_preimP A : dfa_lang (dfa_preim A) =i preim h (dfa_lang A).
Fixpoint re_image (e : regexp char) : regexp char' :=
match e with
| Void => Void
| Eps => Eps
| Atom a => String (h [:: a])
| Star e => Star (re_image e)
| Plus e1 e2 => Plus (re_image e1) (re_image e2)
| Conc e1 e2 => Conc (re_image e1) (re_image e2)
end.
Lemma re_imageP e v : reflect (image h (re_lang e) v) (v \in re_image e).
End Homomorphism.
Implicit Arguments dfa_preim [char char'].
Lemma im_regular (char char' : finType) (h : word char -> word char') L :
homomorphism h -> regular L -> regular (image h L).
Lemma preim_regular (char char' : finType) (h : word char -> word char') L :
homomorphism h -> regular L -> regular (preimage h L).