Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype path fingraph tuple finfun finset.
Require Import misc regexp automata dfa_to_re.

Set Implicit Arguments.
Import Prenex Implicits.

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).