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.

Prenex Implicits Conc.
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.
Proof.
  elim: w => [|a v IHv] w //=. rewrite inE /String /=. apply/concP/eqP.
  - move => [w1] [w2] [e []]. set r := foldr _ _ _.
    rewrite -/(re_lang r) inE e => /eqP -> H /=.
    rewrite IHv inE in H. by rewrite (eqP H).
  - move => e. exists [:: a]; exists v; split => //; split.
    by rewrite inE. by rewrite IHv inE eqxx.
Qed.

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 [::] = [::].
  Proof.
    apply: size0nil. apply/eqP.
    by rewrite -(eqn_add2r (size (h [::]))) -size_cat -h_hom /=.
  Qed.

  Lemma h_seq w : h w = flatten [seq h [:: a] | a <- w].
  Proof. elim: w => [|a w IHw] /= ; by rewrite ?h0 // -cat1s h_hom IHw. Qed.

  Lemma h_flatten vv : h (flatten vv) = flatten (map h vv).
  Proof.
    elim: vv => //= [|v vv IHvv]; first exact: h0.
    by rewrite h_hom IHvv.
  Qed.
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).
  Proof. by move => H; split; move => [v] [] /H; exists v. Qed.

  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).
  Proof.
    rewrite /= /delta_s {2}/dfa_preim /=.
    elim: w (dfa_s A) => [|a w IHw] x; first by rewrite h0.
    by rewrite -cat1s h_hom !delta_cat -!IHw IHw.
  Qed.

  Lemma dfa_preimP A : dfa_lang (dfa_preim A) =i preim h (dfa_lang A).
  Proof.
    move => w. rewrite [_ \in preim _ _]inE topredE !delta_accept.
    by rewrite -/(delta_s _ (h w)) -dfa_preim_aux.
  Qed.

  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).
  Proof.
    elim: e v => [||a|e IHe|e1 IHe1 e2 IHe2|e1 IHe1 e2 IHe2] v /=.
    - rewrite inE; constructor. move => [u]. by case.
    - rewrite inE; apply: (iffP eqP) => [-> |[w] [] /eqP -> <-]; last exact: h0.
      exists [::]; by rewrite ?h0.
    - rewrite StringE. apply: (iffP eqP) => [->|[w /=]].
      + exists [::a] => //. by rewrite /atom inE.
      + by rewrite /atom inE => [[]] /eqP -> <-.
    - apply: (iffP idP) => [/starP [vv] /allP Hvv dev_v|].
        have {Hvv IHe} Hvv : forall v', v' \in vv -> image h (re_lang e) v'.
          by move => v' /Hvv /= /andP [_ /IHe].
        subst v. elim: vv Hvv => [|v vv IHvv] Hvv /=; first by exists [::]; rewrite ?h0.
        case: (Hvv v (mem_head _ _)) => w [Hw1 Hw2].
        case: (all1s Hvv) => Hv /IHvv [ww [Hww1 Hww2]].
        exists (w++ww); split; by [exact: star_cat | rewrite h_hom Hw2 Hww2].
      + case => w [] /starP [ww] /allP Hww1 -> <-. rewrite h_flatten //.
        apply: starI => v' /mapP [w' /Hww1 /= /andP [_ Hw' ->]].
        apply/IHe. by exists w'.
    - rewrite inE -/(re_lang (re_image e1)) -/(re_lang (re_image e2)).
       apply: (iffP orP).
       + case => [/IHe1 | /IHe2] [w] [] H <-.
           exists w => //. by rewrite /plus inE (_ : w \in re_lang e1).
         exists w => //. by rewrite /plus inE (_ : w \in re_lang e2) ?orbT.
       + case => w []. case/orP => H <-; [left; apply/IHe1 |right; apply/IHe2]; by exists w.
    - apply: (iffP idP).
      + case/concP => v1 [v2] [e] [/IHe1 [w [Hw1 Hw2]] /IHe2 [w' [Hw1' Hw2']]].
        exists (w++w'); split; first exact: conc_cat.
        by rewrite h_hom e Hw2 Hw2'.
      + case => w [] /concP [w1] [w2] [-> [H1 H2 <-]]. rewrite h_hom.
        apply: conc_cat; [apply/IHe1|apply/IHe2]. by exists w1. by exists w2.
  Qed.

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).
Proof.
  move => hom_h [e He]. exists (@re_image _ _ h e) => w.
  transitivity (image h (re_lang e) w); first exact: image_ext.
  exact: rwP (re_imageP _ _ _).
Qed.

Lemma preim_regular (char char' : finType) (h : word char -> word char') L :
  homomorphism h -> regular L -> regular (preimage h L).
Proof.
  move => hom_h [e He]. exists (dfa_to_re (dfa_preim h (re_to_dfa e))) => w.
  by rewrite -dfa_to_re_correct dfa_preimP // inE topredE re_to_dfa_correct -He.
Qed.