Library ATBR.DKA_DFA_Language

Require Import List.

Require Import Common.
Require Import Classes.
Require Import Graph.
Require Import Monoid.
Require Import SemiLattice.
Require Import SemiRing.
Require Import KleeneAlgebra.
Require Import MxGraph.
Require Import MxSemiLattice.
Require Import MxSemiRing.
Require Import MxKleeneAlgebra.
Require Import Functors.
Require Import MxFunctors.

Require Import DKA_Definitions.
Require Import Model_Languages.
        Import Model_Languages.Load.


Notation language := (LX label).
Notation LMX n m := (LMX label n m).
Notation Word := (list label).

Fixpoint regex_language (e: regex): language :=
  match e with
    | RegExp.plus e f => regex_language e + regex_language f
    | RegExp.dot e f => regex_language e * regex_language f
    | RegExp.star e => regex_language e #
    | RegExp.one => 1
    | RegExp.zero => 0
    | RegExp.var a => (fun w => w = a::nil)
  end.

Lemma functor_xif `{HF: graph_functor} :
  forall A B b (x y: X A B), F A B (xif b x y) == xif b (F A B x) (F A B y).

Definition regex_language_f :=
  @Build_functor RegExp.re_Graph (@lang_Graph label) (fun A => A) (fun A B e => regex_language e).

Section protect.

Opaque dot plus star one zero.

Instance regex_language_graph_functor: graph_functor regex_language_f.

Instance regex_language_kleene_functor: kleene_functor regex_language_f.

Ltac fold_regex_language := repeat match goal with |- context[regex_language ?e] => change (regex_language e) with (regex_language_f tt tt e) end.

Lemma dot_xifzero_left `{ISR: IdemSemiRing}: forall A B C b (x: X A B) (y: X B C), xif b x 0 * y == xif b (x*y) 0.
Lemma dot_boolxif_left `{ISR: IdemSemiRing}: forall A B b (x: X A B), xif b 1 0 * x == xif b x 0.
Lemma dot_xifzero_right `{ISR: IdemSemiRing}: forall A B C b (x: X B A) (y: X C B), y * xif b x 0 == xif b (y*x) 0.
Lemma dot_boolxif_right `{ISR: IdemSemiRing}: forall A B b (x: X A B), x * xif b 1 0 == xif b x 0.

Transparent dot plus star one zero.

Lemma lang_sum: forall (f: nat -> language) w n i, sum i n f w <-> exists2 j, j<n & f (i+j)%nat w.

Lemma mx_leq_pointwise `{SL: SemiLattice}: forall n m A (M N: MX_ A n m),
  M <== N <-> forall i j, i<n -> j<m -> !M i j <== !N i j.

Section s.
  Variable I: Type.
  Variable n m: nat.
  Variable M: I -> LMX n m.

  Definition mx_lang_Union: LMX n m :=
    box _ _ (fun i j => lang_Union (fun k => !(M k) i j): language).

  Lemma mx_lang_Union_spec: forall M', mx_lang_Union <== M' <-> forall i, M i <== M'.
    Opaque leq.
    Transparent leq.

  Lemma leq_mx_lang_Union: forall k, M k <== mx_lang_Union.
End s.

Lemma mx_star_charac: forall n (M: LMX n n), M# == mx_lang_Union (iter M).

Local Open Scope num_scope.

Section accept.

  Import DFA.
  Variable A : DFA.t.

  Fixpoint read (w: Word) i :=
    match w with
      | nil => i
      | a::w => read w (delta A a i)
    end.

  Definition bounded_word (w: Word) := forall a, List.In a w -> a < max_label A.

  Definition DFA_language : language :=
    fun w => StateSet.In (read w (initial A)) (finaux A) /\ bounded_word w.

  Lemma read_app: forall v w i, read (w++v) i = read v (read w i).

End accept.

Lemma simpl_regex_language : forall A,
  mxF regex_language_f tt (MAUT.size (DFA.to_MAUT A)) (MAUT.size (DFA.to_MAUT A)) (MAUT.delta (DFA.to_MAUT A))
  == box (DFA.size A) (DFA.size A)
  (fun s t => sum 0 (DFA.max_label A)
     (fun i => xif (eqb (state_of_nat t) (DFA.delta A (num_of_nat i) s)) (regex_language (RegExp.var (num_of_nat i))) 0)).
  Opaque regex_language_f. Transparent regex_language_f.

Theorem language_DFA_eval: forall A, DFA.bounded A -> regex_language (DFA.eval A) == DFA_language A.
  Opaque leq plus.
  Opaque eq_nat_bool regex_language_f.
  Transparent regex_language_f.
End protect.