Library theories.re_automata

Require Import alphabet pdrvs.

Module ReAutomata(a:Alphabet).

Module Pdrvs := PDrvs(a).
Import Pdrvs.

Definition of NFA whose states are identified by regular expressions

  Record reAut : Type := {
    sts : Sre ;
    ini : re ;
    fin : Sre ;
    tr : re → A → Sre ;

    ini_in_sts : ini ? sts ;
    fin_in_sts : fin [≤] sts ;
    tr_wdef : ∀ r, r ? sts → ∀ x,
      tr r x [≤] sts
  }.

Extension of the transition function for sets of regular expressions as input

  Definition dlt (rA:reAut) :=
    fun s a ⇒ reset.fold (fun x ⇒ reset.union (rA.(tr) x a)) s [{}].
  Notation "/dlt[ r ]( s ; a )" := (dlt r s a)(at level 35,right associativity).

  Section dltTools.

    Lemma compat_dlt : ∀ rA a,
      compat_op Logic.eq reset.Equal (fun x : reset.elt ⇒ reset.union (tr rA x a)).

    Lemma transpose_dlt : ∀ rA a,
      transpose reset.Equal (fun x : reset.elt ⇒ reset.union (tr rA x a)).

  End dltTools.

Bootstrap axioms for the extended transition function

  Lemma In_tr_dlt : ∀ rA s a y x,
    y ? rA.(tr) x a → x ? s → (y ? /dlt[rA](s;a)).

  Lemma In_dlt_tr_ex : ∀ rA s a x, x ? /dlt[rA](s;a) →
    ∃ y, y ? s ∧ x ? rA.(tr) y a.

Standard properties of the extended transition function

  Lemma dlt_wdef : ∀ s rA a,
    s[≤]rA.(sts) → /dlt[rA](s;a)[≤]rA.(sts).

  Lemma dlt_grow : ∀ s1 s2 rA a,
    s1[≤]s2 → (/dlt[rA](s1;a))[≤](/dlt[rA](s2;a)).

  Lemma dlt_eq :
    ∀ (y : reAut) (x y0 : Sre) y1,
      x[=]y0 → /dlt[y](x;y1)[=]/dlt[y](y0;y1).

Inversion principle for the extended transition function

Lemma In_dlt_inv : ∀ rA x s a,
x ? /dlt[rA](s;a) → ∃ x', x' ? s ∧ x ? /dlt[rA]([!x'];a).

General rewriting for the extended transition function

Add Morphism dlt : dlt_m.

Add Morphism dlt with signature Logic.eq ==> reset.Subset ==> Logic.eq ==> reset.Subset as dtl_subset_m.

Extension of the transition function w.r.t. word, that is, the word accepting function

  Fixpoint wtr (r:Sre)(rA:reAut)(w:word) : Sre :=
    match w with
      | nil ⇒ r
      | (x::xs) ⇒ wtr (/dlt[rA](r;x)) rA xs
    end.

  Notation "/dlt^[ r ]( s ; w )" := (wtr s r w)(at level 35,right associativity).

  Lemma wtr_wdef : ∀ rA w,
    ∀ s, s[≤]rA.(sts) → /dlt^[rA](s;w)[≤]rA.(sts).

  Lemma wtr_grow : ∀ rA w,
    ∀ s1 s2, s1[≤]s2 → /dlt^[rA](s1;w)[≤]/dlt^[rA](s2;w).

General rewriting for the word transition function

Add Morphism wtr : wtr_m.

Add Morphism wtr with signature reset.Subset ==> Logic.eq ==> Logic.eq ==> reset.Subset as wtr_subset_m.

Inversion principle for the word transition function

  Lemma wtr_inv : ∀ rA w,
    ∀ x s, x ? /dlt^[rA](s;w) → ∃ y, y ? s ∧ x ? /dlt^[rA]([!y];w).

  Lemma In_wtr : ∀ rA w,
    ∀ s x y, x ? /dlt^[rA]([!y];w) → y ? s → x ? /dlt^[rA](s;w).

  Lemma wtr_empty : ∀ rA w, /dlt^[rA]([{}];w) [=] [{}].

  Lemma wtr_app : ∀ rA s w1 w2, /dlt^[rA](s;w1++w2) [=] /dlt^[rA]((/dlt^[rA](s;w1));w2).

Logical specification of well-defined extended transition functions

  Inductive wtr_spec (rA:reAut) : re → word → re → Prop :=
  | in_nil : ∀ s, wtr_spec rA s nil s
  | in_symb : ∀ s w q q' a, q ? rA.(tr) s a →
    wtr_spec rA q w q' → wtr_spec rA s (a::w) q'.

  Notation "/dlt@^[ r ]( s ; w ; t )" := (wtr_spec r s w t)(at level 35,right associativity).

Correctness of the word transition relation w.r.t the logical specification wtr_spec

  Lemma wtr_wtr_spec : ∀ w rA r1 r2,
    /dlt@^[rA](r1;w;r2) ↔ r2 ? /dlt^[rA]([!r1];w).

  Hint Resolve wtr_wtr_spec : lbase.

Inductive definitions of the language accepted by a state of an NFA

  Section StateLanguages.

    Inductive SreL_reAut_st (rA:reAut) : re → language :=
    | in_sre_reaut_st : ∀ w r,
      (∃ w', w' ? ((wtr [!r] rA w)[&](rA.(fin)))) → w ?? SreL_reAut_st rA r.

    Inductive SreL_reAut_stemp (rA:reAut) : re → language :=
    | in_sre_reaut_stemp : ∀ w r,
      ((wtr ([!r]) rA w)[&](rA.(fin)))[!=][{}] → w ?? (SreL_reAut_stemp rA r).

    Inductive SreL_reAut_stspec (rA:reAut) : re → language :=
    | in_stre_reaut_spec : ∀ w r,
      (∃ f, f ? rA.(fin) ∧ wtr_spec rA r w f) → w ?? SreL_reAut_stspec rA r.

Properties of languages accepted by the NFA's states

    Lemma SreL_reAut_st_stemp : ∀ rA r, SreL_reAut_st rA r == SreL_reAut_stemp rA r.

    Lemma SreL_reAut_stemp_stspec : ∀ rA r, SreL_reAut_stemp rA r == SreL_reAut_stspec rA r.

    Lemma SreL_reAut_stspec_st : ∀ rA r, SreL_reAut_stspec rA r == SreL_reAut_st rA r.

  End StateLanguages.

  Notation "/Lgs| a <== r |" := (SreL_reAut_st a r)(at level 35,right associativity).
  Notation "/Lgs{ a <== r }" := (SreL_reAut_stemp a r)(at level 35,right associativity).
  Notation "/Lgs[ a <== r ]" := (SreL_reAut_stspec a r)(at level 35,right associativity).

Logical specification of the language accepted by an NFA

  Section AutomataLanguage.

    Inductive reAutL (rA:reAut) : language :=
    | in_reautl : ∀ w, w ?? /Lgs|rA <== rA.(ini)| → w ?? (reAutL rA).

    Inductive reAutLstemp (rA:reAut) : language :=
    | in_reautl_stemp : ∀ w, w ?? /Lgs{rA <== rA.(ini)} → w ?? (reAutLstemp rA).

    Inductive reAutLspec (rA:reAut) : language :=
    | in_reaut_spec : ∀ w, w ?? /Lgs[rA <== rA.(ini)] → w ?? (reAutLspec rA).

Equivalence of logical definitions of languages accepted by automata

    Lemma reAutL_AutL_stemp_eq : ∀ rA, reAutL rA == reAutLstemp rA.

    Lemma reAutL_AutL_stemp_spec_eq : ∀ rA, reAutLstemp rA == reAutLspec rA.

    Lemma reAutL_AutL_spec_eq : ∀ rA, reAutL rA == reAutLspec rA.

  End AutomataLanguage.

  Hint Resolve reAutL_AutL_spec_eq : lbase.

  Notation "/Lg| r |" := (reAutL r)(at level 35,right associativity).
  Notation "/Lg{ r }" := (reAutLstemp r)(at level 35,right associativity).
  Notation "/Lg[ r ]" := (reAutLspec r)(at level 35,right associativity).

  Add Morphism reAutL : reAutL_m.

Formalization of partial derivative automata (PDNFA)

Formal definition of the PDNFA

  Record pdAut (r:re) : Type := {

    aut :> reAut ;

    ini_r : r = aut.(ini) ;
    tr_pdrv : ∀ x a, x ? aut.(sts) ∧ IsSy a → aut.(tr) x a [=] pdrv x a;
    fin_eps : ∀ x, x ? aut.(sts) ∧ c_of_re x = true → x ? aut.(fin)
  }.

Construction of the NFA underlying a PDNFA

Definition mk_am_reAut(r:re) : reAut.

Notation "<reA>[ r ]" := (mk_am_reAut r)(at level 35,right associativity).

Build the PDNFA for a given regular expression

Definition mk_pdAut_of_re (r:re) : pdAut r.

Notation "<pdA>[ r ]" := (mk_pdAut_of_re r)(at level 0).

Extraction of the simple NFA from an PDNFA

Definition mk_reAut_of_pdAut (r:re)(rA:pdAut r) : reAut.

Notation "<EreA>[ r ]" := (mk_reAut_of_pdAut r)(at level 35,right associativity).

Extended one-step delta function of a PDNFA

  Definition dlt_am(r:re)(mA:pdAut r) :=
    fun s a ⇒ /dlt[mA](s;a).

  Notation "//dlt[ x ]( z ; t )" := (dlt_am x (<pdA>[x]) z t)(at level 35,right associativity).

  Lemma dlt_am_eq_dlt : ∀ r s a, //dlt[r](s;a) [=] /dlt[(<pdA>[r])](s;a).

Extension of the transition relation of a PDNFA w.r.t. word

  Definition wtr_am (rs:Sre)(r:re)(w:word) : Sre :=
    let rA := <pdA>[r] in /dlt^[rA](rs;w).

  Notation "//dlt^[ r ]( s , w )" := (wtr_am s r w)(at level 35,right associativity).

Logical specification of the word transition function of the derivative automata

Definition wtr_spec_am (rA r1:re)(w:word)(r2:re) := wtr_spec (<pdA>[rA]) r1 w r2.
Notation "//dlt@^[ t <== s ]( w , r )" := (wtr_spec_am t s w r)(at level 35,right associativity).

Correctness of word transition function w.r.t. its logical specification

Lemma wtr_wtr_am_spec : ∀ w rA r1 r2,
wtr_spec_am rA r1 w r2 ↔ r2 ? (wtr_am [!r1] rA w).

Language accepted in a particular PDNFA state

  Definition SreL_pdAut_st (r:re)(r':re) := /Lgs|(<pdA>[r]) <== r'|.
  Definition reAutLam (rA:re) : language := /Lg|<pdA>[rA]|.

  Definition SreL_pdAut_stemp (r:re)(r':re) := /Lgs{<pdA>[r] <== r'}.
  Definition reAutLam_stemp (r:re) : language := /Lg{<pdA>[r]}.

  Definition SreL_pdAut_stspec (r:re)(r':re) := /Lgs[(<pdA>[r]) <== r'].
  Definition reAutLam_stspec (rA:re) : language := /Lg[<pdA>[rA]].

  Notation "//Lgs| r <== s |" := (SreL_pdAut_st r s)(at level 35,right associativity).
  Notation "//Lg| r |" := (reAutLam r)(at level 35,right associativity).

  Notation "//Lgs{ r <== s }" := (SreL_pdAut_stemp r s)(at level 35,right associativity).
  Notation "//Lg{ r }" := (reAutLam_stemp r)(at level 35,right associativity).

  Notation "//Lgs[ r <== s ]" := (SreL_pdAut_stspec r s)(at level 35,right associativity).
  Notation "//Lg[ r ]" := (reAutLam_stspec r)(at level 35,right associativity).

  Lemma reAutL_stateL_st_stemp : ∀ rA r, //Lgs| rA <== r | == //Lgs{ rA <== r }.

  Lemma reAutL_state_stemp_spec : ∀ rA r, //Lgs{ rA <== r } == //Lgs[ rA <== r ].

  Lemma reAutL_state_spec_st : ∀ rA r, //Lgs[ rA <== r ] == //Lgs| rA <== r |.

  Lemma reAutL_AutL_spec_eq_am : ∀ rA, //Lg|rA| == //Lg[rA].

  Lemma reAutL_AutL_am_eq_stemp : ∀ rA, //Lg|rA| == //Lg{rA}.

  Lemma reAutL_AutL_am_eq_stemp_spec : ∀ rA, //Lg[rA] == //Lg{rA}.

Relating word derivatives and word acceptance by the PDAUT

Lemma wtr_to_wtr_am : ∀ s r w, wtr_am [!s] r w [=] wtr [!s] (mk_pdAut_of_re r) (w).

Word acceptance function wtr_am is equivalent to the syntactical partial derivative w.r.t. words

  Lemma wtr_am_eq_wpdrv : ∀ w r s, pdrv_iw s w [=] wtr s (mk_pdAut_of_re r) (@>w).

  Lemma wpdrv_eq_wtr_am : ∀ w r s, wpdrv s w [=] wtr_am [!s] r w.

  Lemma wpdrv_in_final : ∀ w r s,
    wtr_am [!s] r w [&] (<pdA>[r]).(fin) [!=] [{}] → $$% (wtr_am [!s] r w) = true.

  Lemma final_in_wpdrv : ∀ w s r, s ? (<pdA>[r].(sts)) →
    $$% (wtr_am [!s] r w) = true → ∃ x, x ? (wtr_am [!s] r w [&] (<pdA>[r]).(fin)).

  Lemma lang_of_pdAut_state : ∀ (r:re) rA, r ? (<pdA>[rA].(sts)) → //Lgs|rA <== r | == r.

  Lemma lang_of_pdAut : ∀ r, //Lg|r| == r.

From PDNFA to PDDFA

Definition of deterministic finite automata (DFA) whose states are indexed

by finite sets of regular expressions

  Record reDFA : Type := {
    dsts : SSre ;
    dini :> Sre ;
    dfin : SSre ;
    dtr : Sre → A → Sre ;

    dini_in_dsts : dini ??? dsts ;
    dfin_in_dsts : dfin [{<=}] dsts ;
    dtr_wdef : ∀ r, r ??? dsts → ∀ x,
      dtr r x ??? dsts;
    dtr_compat : ∀ q q', q[=]q'→ ∀ a, (dtr q a)[=](dtr q' a)
  }.

  Add Morphism dtr : dtr_m.

  Section PdDFAConstructions.

    Lemma elem_in_powerset : ∀ r, [!r] ??? powerset(PD(r)).

    Lemma eq_c_of_re_set_compat_bool :
      compat_bool reset.Equal (fun x : resets.elt ⇒ $$% x).

  End PdDFAConstructions.

  Hint Resolve elem_in_powerset eq_c_of_re_set_compat_bool : lbase.

  Reserved Notation "/$dlt^[ r ]( s ; w )" (at level 45,right associativity).
  Fixpoint dwtr (rD:reDFA) (s:Sre) (w:word) : Sre :=
    match w with
      | nil ⇒ s
      | x::xs ⇒ /$dlt^[ rD ]( (rD.(dtr) s x) ; xs)
    end
    where "/$dlt^[ r ]( s ; w )" := (dwtr r s w).

  Lemma dwtr_wdef : ∀ w rD s,
    s ??? rD.(dsts) → (/$dlt^[rD](s;w)) ??? rD.(dsts).

  Add Morphism dwtr : dwtr_m.

Logical specification of the word acceptance function

  Reserved Notation "/$dlt@^[ r ]( s ; w ; t )" (at level 45,right associativity).
  Inductive dwtr_spec(rD:reDFA) : Sre → word → Sre → Prop :=
  | dwtr_spec_c1 : ∀ s s', s[=]s' → /$dlt@^[rD](s; nil ;s')
  | dwtr_spec_c2 : ∀ x w s s' s'', (rD.(dtr) s x)[=]s'' → /$dlt@^[rD](s''; w ;s') → /$dlt@^[rD](s; x::w ;s')
    where "/$dlt@^[ r ]( s ; w ; t )" := (dwtr_spec r s w t).

  Lemma dwtr_spec_app : ∀ rD w s1 s2,
    /$dlt@^[rD](s1;w;s2) → ∀ v s3, /$dlt@^[rD](s2;v;s3) →
      /$dlt@^[rD](s1;w++v;s3).

  Lemma dwtr_spec_iff : ∀ rD w s1 s2,
    /$dlt^[rD](s1;w) [=] s2 ↔ /$dlt@^[rD](s1;w;s2).

  Section reDFAStateLanguages.

    Inductive SreL_reDFA_stemp (rA:reDFA) : Sre → language :=
    | in_sre_redfa_stemp : ∀ w s, /$dlt^[rA](s;w) ??? rA.(dfin) → w ?? (SreL_reDFA_stemp rA s).

    Inductive SreL_reDFA_stspec (rA:reDFA) : Sre → language :=
    | in_stre_redfa_spec : ∀ w s,
      (∃ f, f ??? rA.(dfin) ∧ /$dlt@^[rA](s;w;f)) → w ?? SreL_reDFA_stspec rA s.

Properties of languages accepted by the NFA's states

    Lemma SreL_reDFA_stemp_stspec : ∀ rA r, SreL_reDFA_stemp rA r == SreL_reDFA_stspec rA r.

  End reDFAStateLanguages.

  Notation "/$Lgs{ a <== r }" := (SreL_reDFA_stemp a r)(at level 35,right associativity).
  Notation "/$Lgs[ a <== r ]" := (SreL_reDFA_stspec a r)(at level 35,right associativity).

Logical specification of the language accepted by an NFA

  Section reDFAAutomataLanguage.

    Inductive reDFALstemp (rA:reDFA) : language :=
    | in_redfal_stemp : ∀ w, w ?? /$Lgs{rA <== rA.(dini)} → w ?? (reDFALstemp rA).

    Inductive reDFALspec (rA:reDFA) : language :=
    | in_redfa_spec : ∀ w, w ?? /$Lgs[rA <== rA.(dini)] → w ?? (reDFALspec rA).

Equivalence of logical definitions of languages accepted by automata

    Lemma reDFAL_DFAL_stemp_spec_eq : ∀ rA, reDFALstemp rA == reDFALspec rA.

  End reDFAAutomataLanguage.

  Notation "/$Lg{ r }" := (reDFALstemp r)(at level 35,right associativity).
  Notation "/$Lg[ r ]" := (reDFALspec r)(at level 35,right associativity).

Construction of the partial derivative DFA

Definition of partial derivative DFA (pdDFA)

  Record pdDFA (r:re) : Type := {
    daut :> reDFA ;

    dini_r : [!r] [=] daut.(dini) ;
    dtr_pdrv : ∀ x a, x ??? daut.(dsts) ∧ IsSy a → daut.(dtr) x a [=] pdrv_set x a;
    dfin_eps : ∀ x, x ??? daut.(dsts) ∧ c_of_re_set x = true → x ??? daut.(dfin)
  }.

Construction of DFA partial derivative automata, using sets of regular expressions as states

  Definition mk_reDFA (r:re): reDFA.

  Notation "<reDA>[ r ]" := (mk_reDFA r)(at level 0).

  Definition mk_pdDFA_of_re (r:re) : pdDFA r.

  Notation "<pdDA>[ r ]" := (mk_pdDFA_of_re r)(at level 0).

Extended one-step delta function of a PDNFA

  Definition dlt_amD(r:re)(dA:pdDFA r) :=
    fun s a ⇒ dtr dA s a.

  Notation "//$tr[ x ]( s ; a )" := (dlt_amD x (<pdDA>[x]) s a)(at level 35,right associativity).

Relation to derivatives in PDNFA - relating the basic transition function of the automatas

  Lemma in_st_pdDFA_in_st_amNFA : ∀ s r a x,
    x ? //$tr[r](s;a) → ∃ y, y ? s ∧ x ? //dlt[r]([!y];a).

  Lemma all_in_st_pdDFA_in_st_amNFA : ∀ s r a x y,
    y ? s → x ? //dlt[r]([!y];a) → x ? //$tr[r](s;a).

Extension of the transition relation of a PDNFA w.r.t. word

  Definition dwtr_am (r:re)(rs:Sre)(w:word) : Sre :=
    let rA := <pdDA>[r] in dwtr rA rs w.

  Notation "//$dlt^[ r ]( s ; w )" := (dwtr_am r s w)(at level 35,right associativity).

  Definition dwtr_am_spec (r:re)(r1:Sre)(w:word)(r2:Sre) :=
    let rA := <pdDA>[r] in dwtr_spec rA r1 w r2.

  Notation "//$dlt@^[ r ]( s ; w ; t )" := (dwtr_am_spec r s w t)(at level 35,right associativity).

  Add Morphism dwtr_am_spec : dwtr_am_spec_m.

  Lemma dwtr_am_dwtr_am_spec_eq : ∀ r w r1 r2,
    //$dlt^[r](r1;w) [=] r2 ↔ //$dlt@^[r](r1;w;r2).

Relating pdDFA with pdNFA

  Lemma in_wtr_am_in_dwtr_am : ∀ w r s x y,
    y ? s → x ? //dlt^[r]([!y],w) → x ? //$dlt^[r](s;w).

  Lemma in_dwtr_am_in_wtr_am : ∀ w r s x,
    x ? //$dlt^[r](s;w) → ∃ y, y ? s ∧ x ? //dlt^[r]([!y],w).

  Lemma dwtr_am_wdef : ∀ w (r:re) s,
    s ??? <pdDA>[r].(dsts) → //$dlt^[r](s;w) ??? <pdDA>[r].(dsts).

  Add Morphism dwtr_am : dwtr_am_m.

  Section pdDFAStateLanguages.

    Inductive SreL_pdDFA_stemp (r:re) : Sre → language :=
    | in_sre_pddfa_stemp : ∀ w s, //$dlt^[r](s;w) ??? <pdDA>[r].(dfin) → w ?? (SreL_pdDFA_stemp r s).

    Inductive SreL_pdDFA_stspec (r:re) : Sre → language :=
    | in_stre_pddfa_spec : ∀ w s,
      (∃ f, f ??? <pdDA>[r].(dfin) ∧ //$dlt@^[r](s;w;f)) → w ?? (SreL_pdDFA_stspec r s).

Properties of languages accepted by the NFA's states

    Lemma SreL_pdDFA_stemp_stspec : ∀ rA r, SreL_pdDFA_stemp rA r == SreL_pdDFA_stspec rA r.

  End pdDFAStateLanguages.

  Notation "//$Lgs{ a <== r }" := (SreL_pdDFA_stemp a r)(at level 35,right associativity).
  Notation "//$Lgs[ a <== r ]" := (SreL_pdDFA_stspec a r)(at level 35,right associativity).

Logical specification of the language accepted by an NFA

  Section pdDFAAutomataLanguage.

    Inductive pdDFALstemp (r:re) : language :=
    | in_pddfal_stemp : ∀ w, w ?? //$Lgs{r <== <pdDA>[r].(dini)} → w ?? (pdDFALstemp r).

    Inductive pdDFALspec (r:re) : language :=
    | in_pddfa_spec : ∀ w, w ?? //$Lgs[r <== <pdDA>[r].(dini)] → w ?? (pdDFALspec r).

Equivalence of logical definitions of languages accepted by automata

    Lemma pdDFAL_DFAL_stemp_spec_eq : ∀ rA, pdDFALstemp rA == pdDFALspec rA.

  End pdDFAAutomataLanguage.

  Notation "//$Lg{ r }" := (pdDFALstemp r)(at level 35,right associativity).
  Notation "//$Lg[ r ]" := (pdDFALspec r)(at level 35,right associativity).

Language equivalence between DFA and NFA derivativa automatons

  Lemma fin_NFA_in_dfin_DFA : ∀ r x, x ? <pdA>[r].(fin) → ∃ y, y ??? <pdDA>[r].(dfin) ∧ x ? y.

  Lemma dwtr_eq_wtr : ∀ w r s, wtr s (<reA>[r]) w [=] dwtr (<reDA>[r]) s w.

  Lemma dwtr_am_eq_wtr_am : ∀ w r s, wtr_am s r w [=] dwtr_am r s w.

  Lemma pdNFA_in_pdDFA_word : ∀ r, //Lg{r} == //$Lg{r}.

  Lemma lang_of_pdDFA : ∀ r, //$Lg{r} == r.

End ReAutomata.