(* Authors: Christian Doczkal and Jan-Oliver Kaiser *)
(* Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import all_ssreflect.
From RegLang Require Import setoid_leq misc languages dfa nfa.

Set Default Proof Using "Type".

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Regular Expressions

This file contains the definition of regular expressions and the proof that regular expressions have the same expressive power as finite automata.

Section RegExp.
Variable char : eqType.

Inductive regexp :=
 | Void
 | Eps
 | Atom of char
 | Star of regexp
 | Plus of regexp & regexp
 | Conc of regexp & regexp.

Lemma eq_regexp_dec (e1 e2 : regexp) : {e1 = e2} + {e1 <> e2}.
Proof. decide equality; apply: eq_comparable. Qed.

Definition regexp_eqMixin := EqMixin (compareP eq_regexp_dec).
Canonical Structure form_eqType := EqType _ regexp_eqMixin.
End RegExp.

Arguments void : clear implicits.
Arguments eps : clear implicits.
Prenex Implicits Plus.
Arguments plusP {char r s w}.

Notation "'Void'" := (@Void _).
Notation "'Eps'" := (@Eps _).

We assign a decidable language to every regular expression

Fixpoint re_lang (char: eqType) (e : regexp char) : dlang char :=
  match e with
  | Void => void char
  | Eps => eps char
  | Atom x => atom x
  | Star e1 => star (re_lang e1)
  | Plus e1 e2 => plus (re_lang e1) (re_lang e2)
  | Conc e1 e2 => conc (re_lang e1) (re_lang e2)
  end.

Canonical Structure regexp_predType (char: eqType) := PredType (@re_lang char).

We instantiate Ssreflects Canonical Big Operators
Notation "\sigma_( i <- r ) F" := (\big[Plus/Void]_(i <- r) F) (at level 50).
Notation "\sigma_( i | P ) F" := (\big[Plus/Void]_(i | P) F) (at level 50).

Lemma big_plus_seqP (T char : eqType) (r : seq T) w (F : T -> regexp char) :
  reflect (exists2 x, x \in r & w \in F x) (w \in \sigma_(i <- r) F i).
Proof.
  elim: r w => [|r rs IHrs] w. rewrite big_nil; by constructor => [[x]].
  rewrite big_cons; apply: (iffP plusP) => [[H|H]|[x]].
  - exists r => //; by rewrite mem_head.
  - case/IHrs : H => x Hx ?. exists x => //. by rewrite in_cons Hx orbT.
  - rewrite in_cons; case/orP => [/eqP -> |]; auto => ? ?.
    right. apply/IHrs. by exists x.
Qed.

Lemma big_plusP (T char: finType) (P:pred T) w (F : T -> regexp char) :
  reflect (exists2 i, P i & w \in F i) (w \in \sigma_(i | P i) F i).
Proof.
  rewrite -big_filter. apply: (iffP (big_plus_seqP _ _ _)) => [[x]|[x] H1 H2].
  - rewrite mem_filter => /andP [? ?]; by exists x.
  - by exists x; rewrite // mem_filter H1 mem_index_enum.
Qed.

Fixpoint re_size (char: eqType) (e : regexp char) :=
  match e with
  | Star s => (re_size s).+1
  | Plus s t => ((re_size s)+(re_size t)).+1
  | Conc s t => ((re_size s)+(re_size t)).+1
  | _ => 1
  end.

Lemma big_plus_size (T char : eqType) (r : seq T) (F : T -> regexp char) m :
  (forall i, i \in r -> re_size (F i) <= m) -> re_size (\sigma_(i <- r) F i) <= (size r * m.+1).+1.
Proof.
  elim: r => [|e r IH /all1s [A B]]; first by rewrite big_nil.
  rewrite big_cons /= ltnS mulSn addSn -addnS leq_add //. exact: IH.
Qed.

Regular Expressions to Finite Automata

Section DFAofRE.
Variable (char : finType).

Fixpoint re_to_nfa (r : regexp char): nfa char :=
  match r with
  | Void => dfa_to_nfa (dfa_void _)
  | Eps => nfa_eps _
  | Atom a => nfa_char a
  | Star s => nfa_star (re_to_nfa s)
  | Plus s t => nfa_plus (re_to_nfa s) (re_to_nfa t)
  | Conc s t => nfa_conc (re_to_nfa s) (re_to_nfa t)
  end.

Lemma re_to_nfa_correct (r : regexp char) : nfa_lang (re_to_nfa r) =i r.
Proof.
  elim: r => [||a|s IHs |s IHs t IHt |s IHs t IHt] w //=.
  - by rewrite -dfa_to_nfa_correct inE /dfa_accept inE.
  - exact: nfa_eps_correct.
  - exact: nfa_char_correct.
  - rewrite nfa_star_correct. exact: star_eq.
  - by rewrite nfa_plus_correct /plus inE IHs IHt.
  - rewrite nfa_conc_correct. exact: conc_eq.
Qed.

Lemma re_to_nfa_size e : #|re_to_nfa e| <= 2 * re_size e.
Proof.
  elim: e; rewrite /= ?card_unit ?card_bool => //.
  - move => e IH. by rewrite card_option (leqRW IH) mulnS add2n.
  - move => e1 IH1 e2 IH2.
    by rewrite card_sum (leqRW IH1) (leqRW IH2) mulnS mulnDr add2n ltnW.
  - move => e1 IH1 e2 IH2.
    by rewrite card_sum (leqRW IH1) (leqRW IH2) mulnS mulnDr add2n ltnW.
Qed.

Definition re_to_dfa := @nfa_to_dfa _ \o re_to_nfa.

Lemma re_to_dfa_correct (r : regexp char) : dfa_lang (re_to_dfa r) =i r.
Proof. move => w. by rewrite -nfa_to_dfa_correct re_to_nfa_correct. Qed.

Lemma re_to_dfa_size e : #|re_to_dfa e| <= 2^(2 * re_size e).
Proof. by rewrite card_set leq_pexp2l // re_to_nfa_size. Qed.

Decidability of regular expression equivalence

Definition re_equiv r s := dfa_equiv (re_to_dfa r) (re_to_dfa s).

Lemma re_equiv_correct r s : reflect (r =i s) (re_equiv r s).
Proof.
  apply: (iffP (dfa_equiv_correct _ _)) => H w;
    move/(_ w) : H; by rewrite !re_to_dfa_correct.
Qed.

End DFAofRE.

Finite Automata to Regular Expressions (Kleene Construction)


Section KleeneAlgorithm.
  Variable char : finType.
  Variable A : dfa char.

We first define the transition languages between states. The trasition languages are defined such that w \in L^X q p iff for all nonempty strict prefixes v of w, delta q v \in X.

  Definition L (X : {set A}) (p q : A) x :=
    (delta p x == q) && [forall (i : 'I_(size x) | 0 < i), delta p (take i x) \in X].
  Notation "'L^' X" := (L X) (at level 8,format "'L^' X").

  Lemma dfa_L x y w : w \in L^setT x y = (delta x w == y).
  Proof.
    rewrite unfold_in. case: (_ == _) => //=.
    apply/forall_inP => ? ?. by rewrite inE.
  Qed.

  Lemma LP {X : {set A}} {p q : A} {x} :
    reflect (delta p x = q /\ forall i, (0 < i) -> (i < size x) -> delta p (take i x) \in X)
            (x \in L^X p q).
  Proof.
    apply: (iffP andP); case => /eqP ? H; split => //.
    - move => i I1 I2. exact: (forall_inP H (Ordinal I2)).
    - apply/forall_inP => [[i I1 /= I2]]; auto.
  Qed.

  Lemma L_monotone (X : {set A}) (x y z : A): {subset L^X x y <= L^(z |: X) x y}.
  Proof.
    move => w. rewrite !unfold_in. case: (_ == _) => //. apply: sub_forall => i /=.
    case: (_ < _) => //= H. by rewrite inE H orbT.
  Qed.

  Lemma L_nil X x y : reflect (x = y) ([::] \in L^X x y).
  Proof. apply: (iffP LP) => //=. by case. Qed.

  Lemma L_set0 p q w :
    L^set0 q p w -> p = q /\ w = [::] \/ exists2 a, w = [::a] & p = dfa_trans q a.
  Proof.
    case/LP => <-. case: w => [|a [|b w]] H ; [by left|by right;exists a|].
    move: (H 1). do 2 case/(_ _)/Wrap => //. by rewrite inE.
  Qed.

  Lemma L_split X p q z w : w \in L (z |: X) p q ->
    w \in L^X p q \/
    exists w1 w2, [/\ w = w1 ++ w2, size w2 < size w, w1 \in L^X p z & w2 \in L^(z |: X) z q].
  Proof.
    case/LP => H1 H2.
    case: (find_minn_bound (fun i => (0 < i) && (delta p (take i w) == z)) (size w)).
    - case => i [lt_w /andP [i_gt0 /eqP delta_z] min_i]; right.
      exists (take i w); exists (drop i w).
      have ? : 0 < size w by exact: ltn_trans lt_w.
      rewrite cat_take_drop size_drop -{2}[size w]subn0 ltn_sub2l //; split => //.
      + apply/LP. split => // j J1 J2.
        have lt_i_j : j < i. apply: leq_trans J2 _. by rewrite size_take lt_w.
        have/(H2 _ J1) : j < size w. exact: ltn_trans lt_w.
        case/setU1P => [H|]; last by rewrite take_take.
        move: (min_i _ lt_i_j). by rewrite negb_and J1 H eqxx.
      + apply/LP. rewrite -H1 -{2}[w](cat_take_drop i) delta_cat delta_z.
        split => // j J1 J2. rewrite -{1}delta_z -delta_cat -take_addn.
        apply: H2; first by rewrite addn_gt0 J1 orbT.
        by rewrite -[w](cat_take_drop i) size_cat size_take lt_w ltn_add2l.
    - move => H; left. apply/LP. split => // i I1 I2. apply: contraTT (H2 _ I1 I2) => C.
      rewrite inE negb_or C inE andbT. apply: contraNN (H _ I2) => ->. by rewrite I1.
  Qed.

  Lemma L_cat (X : {set A}) x y z w1 w2 :
    z \in X -> w1 \in L^X x z -> w2 \in L^X z y -> w1++w2 \in L^X x y.
  Proof.
    move => Hz /LP [H11 H12] /LP [H21 H22]. apply/LP.
    split; first by rewrite delta_cat H11 H21.
    move => i i_gt0 H. rewrite take_cat. case: (boolP (i < _)); first exact: H12.
    rewrite delta_cat H11 -leqNgt => le_w1.
    case: (posnP (i - size w1)) => [->|Hi]; first by rewrite take0.
    apply: H22 => //. by rewrite -(ltn_add2l (size w1)) subnKC // -size_cat.
  Qed.

  Lemma L_catL X x y z w1 w2 :
    w1 \in L^X x z -> w2 \in L^(z |: X) z y -> w1++w2 \in L^(z |: X) x y.
  Proof. move/(L_monotone z). apply: L_cat. exact: setU11. Qed.

  Lemma L_catR X x y z w1 w2 :
    w1 \in L^(z |: X) x z -> w2 \in L^X z y -> w1++w2 \in L^(z |: X) x y.
  Proof. move => H /(L_monotone z). apply: L_cat H. exact: setU11. Qed.

  Lemma L_star (X : {set A}) z w : w \in star (L^X z z) -> w \in L^(z |: X) z z.
  Proof.
    move/starP => [vv Hvv ->]. elim: vv Hvv => [_|r vv IHvv]; first exact/L_nil.
    move => /= /andP [/andP [_ H1] H2]. exact: L_catL H1 (IHvv H2).
  Qed.

Main Lemma - L satisfies a recursive equation that can be used to construct a regular expression

  Lemma L_rec (X : {set A}) x y z :
    L^(z |: X) x y =i plus (conc (L^X x z) (conc (star (L^X z z)) (L^X z y))) (L^X x y).
  Proof.
    move => w. apply/idP/idP.
    - move: w x y. apply: (size_induction (measure := size)) => w IHw x y.
      move/L_split => [|[w1 [w2 [Hw' H1 Hw1 Hw2]]]].
      + rewrite inE => ->. by rewrite orbT.
      + move: (IHw w2 H1 z y Hw2) Hw' => H4 -> {IHw H1}.
        rewrite inE (conc_cat Hw1 _) //.
        case/plusP : H4 => H; last by rewrite -[w2]cat0s conc_cat //.
        move/concP : H => [w21] [w22] [W1 [W2]] /concP [w221] [w222] [W3 [W4 W5]]; subst.
        by rewrite catA conc_cat // star_cat.
    - case/plusP ; last exact: L_monotone.
      move/concP => [w1] [w2] [-> [Hw1]] /concP [w3] [w4] [-> [Hw3 Hw4]].
      by rewrite (L_catL Hw1) // (L_catR _ Hw4) // L_star.
  Qed.

Construction of the regular expression

  Definition edges (x y : A) := \big[Plus/Void]_(a | dfa_trans x a == y) Atom a.

  Definition edgesP x y w :
    reflect (exists2 a, w = [::a] & dfa_trans x a = y) (w \in edges x y).
  Proof. apply: (iffP (big_plusP _ _ _)) => [|] [a] /eqP ? /eqP ?; by exists a. Qed.

  Definition R0 x y := Plus (if x == y then Eps else Void) (edges x y).

  Lemma mem_R0 w x y :
    reflect (w = [::] /\ x=y \/ exists2 a, w = [::a] & dfa_trans x a = y)
            (w \in R0 x y).
  Proof.
    apply: (iffP plusP).
    - case => [| /edgesP]; auto. case e : (x == y) => // /eqP.
      by rewrite (eqP e); auto.
    - case => [[-> ->]|/edgesP];auto. by rewrite eqxx; auto.
  Qed.

  Fixpoint R (X : seq A) (x y : A) :=
    if X isn't z :: X' then R0 x y else
      Plus (Conc (R X' x z) (Conc (Star (R X' z z)) (R X' z y))) (R X' x y).

  Notation "'R^' X" := (R X) (at level 8, format "'R^' X").

  Lemma L_R (X : seq A) x y : L^[set z in X] x y =i R^X x y.
  Proof.
    elim: X x y => [|z X' IH] x y w.
    - rewrite (_ : [set z in [::]] = set0) //=.
      apply/idP/mem_R0.
      + move/L_set0 => [[-> ->]|[a -> ->]]; by eauto.
      + move => [[-> ->]|[a -> <-]]; apply/LP => /=; split => // [[|i]] //.
    - rewrite set_cons /= (L_rec _ _) -2!topredE /= /plus /= IH.
      f_equal.
      apply: conc_eq; first exact: IH.
      apply: conc_eq; last exact: IH.
      apply: star_eq. exact: IH.
  Qed.

  Definition dfa_to_re : regexp char := \sigma_(x | x \in dfa_fin A) R^(enum A) (dfa_s A) x.

  Lemma dfa_to_re_correct : dfa_lang A =i dfa_to_re.
  Proof.
    move => w. apply/idP/big_plusP => [H|[x Hx]].
    - exists (delta_s A w) => //. by rewrite -L_R set_enum dfa_L.
    - by rewrite -L_R set_enum dfa_L inE /dfa_accept => /eqP ->.
  Qed.

Size Bound for Kleene Theorem


  Let c := (2 * #|char|).+3.

  Lemma R0_size x y : re_size (R0 x y) <= c.
  Proof.
    rewrite /= [X in X + _](_ : _ = 1); last by case (_ == _).
    rewrite add1n !ltnS. rewrite /edges -big_filter.
    apply: leq_trans (big_plus_size (m := 1) _) _ => [//|].
    rewrite size_filter ltnS mulnC leq_mul2l /=.
    apply: leq_trans (count_size _ _) _. by rewrite /index_enum -enumT cardE.
  Qed.

  Fixpoint R_size_rec (n : nat) := if n is n'.+1 then 4 * R_size_rec n' + 4 else c.

  Lemma R_size x : re_size (R^(enum A) (dfa_s A) x) <= R_size_rec #|A| .
  Proof.
    rewrite cardE. elim: (enum A) (dfa_s A) x => [|r s IH] p q.
    - exact: R0_size.
    - rewrite /= 6!(addSn,addnS) addn4 !ltnS !(leqRW (IH _ _)).
      by rewrite !mulSn mul0n addn0 !addnA.
  Qed.

  Lemma R_size_low (n : nat) : 3 <= R_size_rec n.
  Proof. elim: n => // n IH. by rewrite (leqRW IH) /= -(leqRW (leq_addr _ _)) leq_pmull. Qed.

  Lemma R_size_high n : R_size_rec n <= c * 4^(2 * n).
  Proof.
    elim: n => //= [|n IH].
    - by rewrite mulnS muln0 addn0.
    - rewrite [in X in _^X]mulnS expnD mulnA [c * _]mulnC -mulnA.
      rewrite -(leqRW IH) -[4^2]/((1+3) * 4) -mulnA mulnDl mul1n leq_add //.
      by rewrite -(leqRW (R_size_low _)).
  Qed.

  Lemma dfa_to_re_size : re_size dfa_to_re <= (#|A| * (c * 4 ^ (2 * #|A|)).+1).+1.
  Proof.
    rewrite /dfa_to_re -big_filter (leqRW (big_plus_size (m := R_size_rec #|A|)_)).
    - rewrite -(leqRW (R_size_high _)) size_filter (leqRW (count_size _ _)).
      by rewrite ltnS /index_enum -enumT cardE.
    - move => q _. exact: R_size.
  Qed.

End KleeneAlgorithm.

Lemma regularP (char : finType) (L : lang char) :
  regular L <-T-> { e : regexp char | forall x, L x <-> x \in e}.
Proof.
  split => [[A HA]|[e He]].
  - exists (dfa_to_re A) => x. by rewrite -dfa_to_re_correct.
  - exists (re_to_dfa e) => x. by rewrite re_to_dfa_correct.
Qed.

Closure of Regular Expressions under intersection and complement

Regular expression for images of homomorphimsms


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 Image.
  Variables (char char' : finType) (h : seq char -> seq char').
  Hypothesis h_hom : homomorphism h.

  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 using h_hom.
    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 v' : v' \in vv -> image h (re_lang e) v'.
          by move => /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'.
    - 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 Image.

Lemma im_regular (char char' : finType) (h : word char -> word char') L :
  homomorphism h -> regular L -> regular (image h L).
Proof.
  move => hom_h /regularP [e He]. apply/regularP. exists (@re_image _ _ h e) => w.
  transitivity (image h (re_lang e) w); first exact: image_ext.
  exact: rwP (re_imageP _ _ _).
Qed.

Regular Expression for word reversal


Fixpoint Rev (char : finType) (e : regexp char) :=
  match e with
  | Star e => Star (Rev e)
  | Plus e1 e2 => Plus (Rev e1) (Rev e2)
  | Conc e1 e2 => Conc (Rev e2) (Rev e1)
  | _ => e
  end.

Lemma Rev_correct (char : finType) (e : regexp char) w :
  w \in Rev e = (rev w \in e).
Proof.
  elim: e w => [||a|e IH|e1 IH1 e2 IH2|e1 IH1 e2 IH2] w //.
  - rewrite !inE. apply/eqP/idP; first by move->.
    elim/last_ind: w => //= s a _. by rewrite rev_rcons.
  - rewrite !inE. apply/eqP/eqP; first by move->.
    do 2 elim/last_ind: w => //= w ? _. by rewrite !rev_rcons.
  - rewrite /=; apply/idP/idP; case/starP => vv /allP /= H.
    + move->. rewrite rev_flatten. apply: starI => v'.
      rewrite mem_rev => /mapP [v V1 ->]. rewrite -IH. by case/andP: (H _ V1).
    + rewrite -{2}[w]revK => ->. rewrite rev_flatten. apply: starI => v'.
      rewrite mem_rev => /mapP [v V1 ->]. rewrite IH revK. by case/andP: (H _ V1).
  - by rewrite /= !inE -!/(re_lang _) IH1 IH2.
  - rewrite /=. apply/concP/concP => [] [w1] [w2]; rewrite -!/(re_lang _).
    + move => [-> [A B]]. exists (rev w2); exists (rev w1). by rewrite rev_cat -IH1 -IH2.
    + rewrite -{2}[w]revK. move => [-> [A B]]. exists (rev w2); exists (rev w1).
      by rewrite rev_cat IH1 IH2 !revK.
Qed.

Lemma regular_rev (char : finType) (L : lang char) :
  regular L -> regular (fun x => L (rev x)).
Proof. case/regularP => e H. apply/regularP. exists (Rev e) => x. by rewrite Rev_correct. Qed.