Library theories.language

File with the formalization of the base constructions of regular languages:

alphabet ;
words and regular language ;
regular expression and regular language ;
sets of regular expressions, pairs of sets of regular expressions
partial derivatives of regular expressions, and left-quotient of languages

Require Import SetoidList.
Require Import Setoid.
Require Export FSets.
Require Export Ensembles Constructive_sets.
Require Import ProofIrrelevance ProofIrrelevanceFacts.
Require Import Program.
Require Import alphabet.
Require Import TheoryList.

Module where all the language theory is defined and its properties of interest are formaly specified and verified

Module Language(alph:Alphabet).

Definition of words

Export alph.

Definition IsSy (a:A) := List.In a sigma.

Word is defined as a list of symbols

Definition word := list A.

IWord are defined as right-to-left defined lists of symbols

  Inductive iword : Type :=
  | inil : iword
  | icons : iword → A → iword.

  Notation "<[]" := inil.
  Infix "<::" := icons (at level 60, right associativity).

Correctness of words/iwords

  Inductive IsWord : word → Prop :=
  | nil_IsWord : IsWord nil
  | cons_IsWord : ∀ a, IsSy a→
    ∀ u, IsWord u → IsWord (cons a u).

  Inductive IsIWord : iword → Prop :=
  | inil_IsIWord : IsIWord inil
  | icons_IsIWord : ∀ a, IsSy a →
    ∀ u, IsIWord u → IsIWord (icons u a).

  Hint Constructors iword IsWord IsIWord : lbase.

Correctness of list concatenation

  Lemma IsWord_app : ∀ u v, IsWord u →
    IsWord v → IsWord (u++v).

  Lemma IsWord_app_1 : ∀ u v, IsWord (u++v) →
    IsWord u.

  Lemma IsWord_app_2 : ∀ u v, IsWord (u++v) →
    IsWord v.

  Hint Resolve IsWord_app IsWord_app_1 IsWord_app_2 : lbase.
  Hint Immediate IsWord_app IsWord_app_1 IsWord_app_2 : lbase.

Concatenation correctness for iwords

  Reserved Notation "x <++ y" (at level 60,right associativity).
  Fixpoint iword_app (a b:iword){struct b} : iword :=
    match b with
      | <[] ⇒ a
      | x<::y ⇒ (a <++ x)<::y
    end
    where "x <++ y" := (iword_app x y).

  Lemma IsIWord_iword_app : ∀ u v, IsIWord u →
    IsIWord v → IsIWord (u <++ v).

  Lemma IsIWord_iword_app_1 : ∀ u v, IsIWord (u <++ v) →
    IsIWord u.

  Lemma IsIWord_iword_app_2 : ∀ u v, IsIWord (u <++ v) →
    IsIWord v.

  Hint Resolve IsIWord_iword_app IsIWord_iword_app_1 IsIWord_iword_app_2 : lbase.
  Hint Immediate IsIWord_iword_app IsIWord_iword_app_1 IsIWord_iword_app_2 : lbase.

Power of a word (n'th concatenation of a word with itself)

  Reserved Notation "x ^p n" (at level 60).
  Fixpoint WordPower (x:word)(n:nat) :=
    match n with
      | O ⇒ nil
      | S n ⇒ x ++ (x ^p n)
    end
    where "x ^p n" := (WordPower x n).

  Lemma IsWord_WordPower : ∀ u, IsWord u →
    ∀ n, IsWord (u ^p n).

  Lemma IsWord_rev : ∀ u, IsWord u → IsWord (rev u).

  Hint Resolve IsWord_WordPower IsWord_rev : lbase.
  Hint Immediate IsWord_WordPower IsWord_rev : lbase.

Power of an iword (n'th concatenation of a word with itself)

  Reserved Notation "x ^p< n" (at level 60).
  Fixpoint IWordPower (x:iword)(n:nat) :=
    match n with
      | O ⇒ <[]
      | S n ⇒ (x ^p< n) <++ x
    end
    where "x ^p< n" := (IWordPower x n).

  Lemma IsIWord_IWordPower : ∀ u, IsIWord u →
    ∀ n, IsIWord (u ^p< n).

  Hint Resolve IsIWord_IWordPower : lbase.
  Hint Immediate IsIWord_IWordPower : lbase.

Relation between words and iwords

  Lemma IWord_iword_app_nil : ∀ w', <[] <++ w' = w'.

  Lemma IWord_iword_app_assoc : ∀ w1 w2 w3,
    w1 <++ (w2 <++ w3) = (w1 <++ w2) <++ w3.

  Lemma IWord_icons_iword_app_2 : ∀ u u0 a,
    (u <++ u0)<::a = u <++ (u0 <::a).

  Lemma IWord_icons_iword_app : ∀ x y w,
    (x<::y) <++ w = x <++ ((<[]<::y) <++ w).

  Hint Resolve IWord_iword_app_nil IWord_iword_app_assoc IWord_icons_iword_app_2
    IWord_icons_iword_app : lbase.
  Hint Immediate IWord_iword_app_nil IWord_iword_app_assoc IWord_icons_iword_app_2
    IWord_icons_iword_app : lbase.

words to iwords conversion function

  Reserved Notation "<@ a" (at level 50).
  Fixpoint word_to_iword (a:word) : iword :=
    match a with
      | [] ⇒ <[]
      | a::xs ⇒ (<[]<::a) <++ (<@ xs)
    end
    where "<@ a" := (word_to_iword a).

iwords to words conversion function

  Reserved Notation "@> a" (at level 50).
  Fixpoint iword_to_word (a:iword) : word :=
    match a with
      | <[] ⇒ []
      | l<::x ⇒ (@> l) ++ (x::[])
    end
    where "@> a" := (iword_to_word a).

  Theorem exWordFromIWord : ∀ w, ∃ w', w' = <@ w.

  Theorem exIWordFromWord : ∀ w', ∃ w, w = @> w'.

  Lemma IWordFromWordConc : ∀ w w',
    <@ (w ++ w') = (<@ w) <++ (<@ w').

  Hint Resolve IWordFromWordConc exIWordFromWord exWordFromIWord : lbase.
  Hint Immediate IWordFromWordConc exIWordFromWord exWordFromIWord : lbase.

Correctness of conversion operations between words and iwords

  Lemma WordFromIWordConc : ∀ w' w'',
    @> (w' <++ w'') = @> w' ++ @> w''.

  Hint Resolve WordFromIWordConc : lbase.
  Hint Immediate WordFromIWordConc : lbase.

  Theorem IWordFromWord : ∀ w',
    <@ (@> w') = w'.

  Hint Resolve IWordFromWord : lbase.
  Hint Immediate IWordFromWord : lbase.

  Theorem WordFromIWord : ∀ w, @> (<@ w) = w.

  Hint Resolve WordFromIWord : lbase.
  Hint Immediate WordFromIWord : lbase.

  Lemma nil2inil : ∀ w, w = [] → <@ w = <[].

  Lemma inil2nil : ∀ w, w = <[] → @> w = [].

  Hint Resolve nil2inil inil2nil : lbase.
  Hint Immediate nil2inil inil2nil : lbase.

  Lemma not_nil2inil : ∀ w, w ≠ [] → <@ w ≠ <[].

  Hint Resolve not_nil2inil : lbase.
  Hint Immediate not_nil2inil : lbase.

  Lemma eq_app_iapp : ∀ w u v,
    w = u ++ v → <@ w = <@ u <++ <@ v.

  Hint Resolve eq_app_iapp : lbase.
  Hint Immediate eq_app_iapp : lbase.

  Lemma iword_destruct : ∀ w, {w = <[]}+{w ≠ <[]}.

A language is a set of words

Definition language := Ensemble word.

Notation "x '??' y" := (Ensembles.In word y x)(at level 60).

Language containing all words : sigma star

  Inductive SigmaStar : language :=
  | in_sigma_star : ∀ w, IsWord w → w ?? SigmaStar.

  Lemma ex_sy : {s: A | IsSy s }.

  Lemma ex_word : {w:word | w ?? SigmaStar}.

  Hint Constructors SigmaStar : lbase.

Well foundness of a language

  Definition language_wf (L:language) := Included word L SigmaStar.

  Definition EmptyL := (Empty_set word).
  Notation "{}" := EmptyL.

  Lemma EmptyL_wf : language_wf {}.

  Definition EpsL := (Singleton word nil).
  Notation "{e}" := EpsL.

  Hint Constructors Singleton : lbase.

  Lemma EpsL_wf : language_wf {e}.

  Inductive SymbL (s:A) : language :=
  | in_sing : IsSy s → (s::nil) ?? SymbL s.

  Notation "{! S }" := (SymbL S).

  Lemma SymbL_wf : ∀ s, language_wf ({!s}).

  Hint Resolve EmptyL_wf EpsL_wf SymbL_wf : lbase.
  Hint Immediate EmptyL_wf EpsL_wf SymbL_wf : lbase.

  Definition UnionL (l l':language) := Union word l l'.

  Hint Constructors Union : lbase.

  Infix "{+}" := UnionL(at level 59,left associativity).

  Lemma UnionL_wf : ∀ L1 L2,
    ∀ (H1:language_wf L1)(H2:language_wf L2),
      language_wf (L1{+}L2).

  Hint Resolve UnionL_wf : lbase.
  Hint Immediate UnionL_wf : lbase.

  Reserved Notation "x {.} y" (at level 58,left associativity).
  Inductive ConcL (L1 L2:language) : language :=
  | ConcL_app : ∀ w1 w2, w1 ?? L1 → w2 ?? L2 →
    (w1 ++ w2) ?? (L1 {.} L2)
    where "x {.} y" := (ConcL x y).

  Hint Constructors ConcL : lbase.

  Lemma ConcL_wf : ∀ L1 L2,
    ∀ (H1:language_wf L1)(H2:language_wf L2),
      language_wf (L1{.}L2).

  Hint Resolve ConcL_wf : lbase.
  Hint Immediate ConcL_wf : lbase.

  Reserved Notation "x {^} n" (at level 60).
  Fixpoint ConcLn (L:language)(n:nat) : language :=
    match n with
      | 0 ⇒ EpsL
      | (S m) ⇒ L{.}(L{^}m)
    end
    where "x {^} n" := (ConcLn x n).

  Lemma ConcLn_0 : ∀ l, l{^}0 = EpsL.

  Lemma ConcLn_n : ∀ l n, l{^}(n+1) = l{.}(l{^}n).

  Hint Resolve ConcLn_0 ConcLn_n : lbase.
  Hint Immediate ConcLn_0 ConcLn_n : lbase.

  Lemma ConcLn_wf : ∀ L n,forall (H:language_wf L),
    language_wf (L{^}n).

  Hint Resolve ConcLn_wf : lbase.
  Hint Immediate ConcLn_wf : lbase.

  Reserved Notation "x {*}" (at level 45).
  Inductive StarL (l:language) : language :=
  | starL_n : ∀ n w, w ?? (l{^}n) → w ?? (l{*})
    where "x {*}" := (StarL x).

  Reserved Notation "x {^+}" (at level 45).
  Inductive PlusL (l:language) : language :=
  | starPlusL_n : ∀ n w, w ?? (l{^}(S n)) → w ?? (l{^+})
    where "x {^+}" := (PlusL x).

  Hint Constructors StarL PlusL : lbase.
  Hint Immediate StarL PlusL : lbase.

  Lemma StarL_wf : ∀ L, ∀ (H:language_wf L), language_wf (L{*}).

  Lemma PlusL_wf : ∀ L, ∀ (H:language_wf L), language_wf (L{^+}).

  Hint Resolve StarL_wf PlusL_wf : lbase.
  Hint Immediate StarL_wf PlusL_wf : lbase.

  Definition LEq (L1 L2:language) := Same_set word L1 L2.

  Notation "x == y" := (LEq x y)(at level 70).
  Notation "x != y" := (~(x == y))(at level 70).

  Lemma LEq_equiv : Equivalence LEq.

  Add Parametric Relation : language LEq
    reflexivity proved by (@Equivalence_Reflexive _ _ LEq_equiv)
    symmetry proved by (@Equivalence_Symmetric _ _ LEq_equiv)
    transitivity proved by (@Equivalence_Transitive _ _ LEq_equiv) as LEq_rel.

  Add Morphism SymbL with signature syeq ==> LEq as SymL_m.

  Add Morphism UnionL : UnionL_m.

  Add Morphism ConcL : ConcL_m.

  Add Morphism ConcLn : ConcLn_m.

  Add Morphism StarL : StarL_m.

  Add Morphism PlusL : PlusL_m.

  Theorem empty_not_nil : {e} != {}.

  Lemma not_eq_left : ∀ l1 l2,
    (∃ w, w ?? l1 ∧ ¬ w ?? l2) → l1 != l2.

  Lemma not_eq_right : ∀ l1 l2,
    (∃ w, ¬ w ?? l1 ∧ w ?? l2) → l1 != l2.

Properties of union

Theorem union_inj_left : ∀ l1 l2 l3, l1 == l3 → l1{+}l2 == l3{+}l2.

Theorem union_inj_right : ∀ l1 l2 l3, l1 == l3 → l2{+}l1 == l2{+}l3.

Properties of concatenation

Theorem conc_inj_left : ∀ l1 l2 l3, l1 == l3 → l1{.}l2 == l3{.}l2.

Theorem conc_inj_right : ∀ l1 l2 l3, l1 == l3 → l2{.}l1 == l2{.}l3.

Tactics for set simplification

Ltac split_eq := split;unfold Included;intros.

Definition of regular language

  Inductive RL : language → Prop :=
  | RL0 : RL {}
  | RL1 : RL {e}
  | RLsy : ∀ a, RL {!a}
  | RLp : ∀ l1 l2, RL l1 → RL l2 → RL (l1{+}l2)
  | RLc : ∀ l1 l2, RL l1 → RL l2 → RL (l1{.}l2)
  | RLst : ∀ l, RL l → RL (l{*}).

  Hint Constructors RL : lbase.

Semi-ring properties

  Theorem ConcL_neutral_right : ∀ l, l{.}{e} == l.

  Theorem ConcL_neutral_left : ∀ l:language, {e}{.}l == l.

  Theorem ConcL_empty_left : ∀ l:language, {}{.}l == {}.

  Theorem ConcL_empty_right : ∀ l:language, l{.}{} == {}.

  Hint Resolve ConcL_empty_right ConcL_empty_left ConcL_neutral_left
    ConcL_neutral_right : lbase.

  Theorem lang_concat_assoc : ∀ l1 l2 l3,
    (l1{.}l2){.}l3 == l1{.}(l2{.}l3).

  Theorem lang_concat_distr_right : ∀ l1 l2 l3,
    l1{.}(l2{+}l3) == (l1{.}l2){+}(l1{.}l3).

  Theorem lang_concat_distr_left : ∀ l1 l2 l3,
    (l1{+}l2){.}l3 == (l1{.}l3){+}(l2{.}l3).

  Theorem lang_union_neutral_left : ∀ l:language, {}{+}l == l.

  Theorem lang_union_neutral_right : ∀ l:language, l{+}{} == l.

  Theorem lang_union_comm : ∀ l1 l2: language, l1{+}l2 == l2{+}l1.

  Theorem lang_union_idemp : ∀ l:language, l{+}l == l.

Tactics for the simplification of simple language operations

  Ltac simplc H :=
    repeat (match type of H with
              | context[_{.}{e}] ⇒ rewrite ConcL_neutral_right in H
              | context[{e}{.}_] ⇒ rewrite ConcL_neutral_left in H
              | context[{}{.}_] ⇒ rewrite ConcL_empty_left in H
              | context[_{.}{}] ⇒ rewrite ConcL_empty_right in H
           end).

  Ltac simplu H :=
    repeat (match type of H with
              | context[_{+}{}] ⇒ rewrite lang_union_neutral_right in H
              | context[{}{+}_] ⇒ rewrite lang_union_neutral_left in H
            end).

  Ltac simplcg :=
    match goal with
      | [ |- context[_{.}{e}]] ⇒ rewrite ConcL_neutral_right
      | [ |- context[{e}{.}_]] ⇒ rewrite ConcL_neutral_left
      | [ |- context[{}{.}_]] ⇒ rewrite ConcL_empty_left
      | [ |- context[_{.}{}]] ⇒ rewrite ConcL_empty_right
    end.

  Ltac simplug :=
    match goal with
      | [ |- context[?X{+}{}]] ⇒ rewrite lang_union_neutral_right
      | [ |- context[{}{+}?X]] ⇒ rewrite lang_union_neutral_left
    end.

  Theorem lang_union_assoc : ∀ l1 l2 l3, (l1{+}l2){+}l3 == l1{+}(l2{+}l3).

  Hint Resolve lang_concat_assoc lang_union_assoc lang_union_idemp lang_union_comm
    lang_union_neutral_right lang_concat_distr_left : lbase.

  Hint Immediate lang_concat_assoc lang_union_assoc lang_union_idemp lang_union_comm
    lang_union_neutral_right lang_concat_distr_left : lbase.

Definition and properties of the order on languages

  Definition LLeq (L1 L2:language) := L1{+}L2 == L2.

  Notation "x '<<=' y" := (LLeq x y)(at level 70).

  Add Morphism LLeq : LLeq_m.

  Hint Resolve LLeq_m : lbase.
  Hint Immediate LLeq_m : lbase.

  Theorem LLeq_refl : ∀ x, x <<= x.

  Hint Resolve LLeq_refl : lbase.
  Hint Immediate LLeq_refl : lbase.

  Theorem LLeq_trans : ∀ x y z, x <<= y → y <<= z → x <<= z.

  Hint Resolve LLeq_refl LLeq_trans : lbase.
  Hint Immediate LLeq_refl LLeq_trans : lbase.

  Lemma mon_concat : ∀ x y z:language, x <<= y → (x{.}z) <<= (y{.}z).

  Hint Resolve mon_concat : lbase.
  Hint Immediate mon_concat : lbase.

  Lemma eq_to_leq : ∀ x y : language, x == y → x <<= y.

  Hint Resolve eq_to_leq : lbase.
  Hint Immediate eq_to_leq : lbase.

  Lemma leq_to_eq : ∀ x y, x <<= y ∧ y <<= x → x == y.

  Hint Resolve eq_to_leq : lbase.
  Hint Immediate eq_to_leq : lbase.

Properties of kleene star

  Lemma StarL_UnionL_comm : ∀ l,
    l{+}(l{*}) == l{*}.

  Hint Resolve StarL_UnionL_comm : lbase.
  Hint Immediate StarL_UnionL_comm : lbase.

  Lemma star_plus_on : ∀ l, {e}{+}(l{*}) == l{*}.

  Hint Resolve star_plus_on : lbase.
  Hint Immediate star_plus_on : lbase.

  Lemma empty_star_is_epsilon : {}{*} == {e}.

  Lemma id_empty_star_is_epsilon : {e}{*} == {e}.

  Hint Resolve empty_star_is_epsilon id_empty_star_is_epsilon : lbase.
  Hint Immediate empty_star_is_epsilon id_empty_star_is_epsilon : lbase.

  Lemma lang_in_star_to_n : ∀ w r, w ?? (r{*}) → ∃ n, w ?? (r{^}n).

  Theorem lang_in_star : ∀ l, l <<= (l{*}).

  Lemma StarL_ConL_comm : ∀ l,
    (l{.}(l{*})) <<= (l{*}).

  Hint Resolve lang_in_star lang_in_star_to_n StarL_ConL_comm : lbase.
  Hint Immediate lang_in_star lang_in_star_to_n StarL_ConL_comm : lbase.

  Theorem inProdProdStar : ∀ l,
    (l{.}(l{*})) <<= ((l{*}){.}(l{*})).

  Theorem inProdProdInv : ∀ l, ((l{*}){.}l) <<= ((l{*}){.}(l{*})).

  Hint Resolve inProdProdStar inProdProdInv : lbase.
  Hint Immediate inProdProdStar inProdProdInv : lbase.

  Lemma PlusL_conc : ∀ l n m,
    l{^}(n+m) == (l{^}n){.}(l{^}m).

  Hint Resolve PlusL_conc : lbase.
  Hint Immediate PlusL_conc : lbase.

  Lemma assoc_succ_conc : ∀ l n m,
    l{.}(l{^}(n+m)) == (l{^}(S n)){.}(l{^}m).

  Hint Resolve assoc_succ_conc : lbase.
  Hint Immediate assoc_succ_conc : lbase.

  Lemma nconcat_invert_order : ∀ n l,
    (l{^}(S n)) == ((l{^}n){.}l).

  Theorem star_prod_eq_star : ∀ l, l{*} == (l{*}){.}(l{*}).

  Hint Resolve nconcat_invert_order star_prod_eq_star : lbase.
  Hint Immediate nconcat_invert_order star_prod_eq_star : lbase.

  Theorem power_of_star_lang : ∀ n l, ((l{*}){^}n) <<= (l{*}).

  Theorem double_star_in_star : ∀ l, ((l{*}){*}) <<= (l{*}).

  Theorem double_star_eq_star : ∀ l, ((l{*}){*}) == (l{*}).

  Hint Resolve power_of_star_lang double_star_in_star : lbase.
  Hint Immediate power_of_star_lang double_star_in_star : lbase.

  Theorem kat_ax_1_aux_1 : ∀ l, ({e}{+}(l{.}(l{*}))) <<= (l{*}).

  Theorem kat_ax_1_aux_2 : ∀ l, (l{*}) <<= ({e}{+}(l{.}(l{*}))).

  Hint Resolve kat_ax_1_aux_1 kat_ax_1_aux_2 : lbase.
  Hint Immediate kat_ax_1_aux_1 kat_ax_1_aux_2 : lbase.

  Theorem kat_ax_1_lang : ∀ l, {e}{+}(l{.}(l{*})) == l{*}.

  Theorem kat_ax2_aux_1 : ∀ l, ({e}{+}((l{*}){.}l)) <<= (l{*}).

  Hint Resolve kat_ax_1_lang kat_ax2_aux_1 : lbase.
  Hint Immediate kat_ax_1_lang kat_ax2_aux_1 : lbase.

  Lemma kat_ax2_aux_2_a : ∀ n l w,
    (w) ?? ((l{^}n){.}l) → (w) ?? (l{*}{.}l).

  Theorem kat_ax2_aux_2 : ∀ l, (l{*}) <<= ({e}{+}((l{*}){.}l)).

  Hint Resolve kat_ax2_aux_2_a kat_ax2_aux_2 : lbase.
  Hint Immediate kat_ax2_aux_2_a kat_ax2_aux_2 : lbase.

  Theorem kat_ax_2_lang : ∀ l, {e}{+}((l{*}){.}l) == l{*}.

  Hint Resolve kat_ax_2_lang : lbase.
  Hint Immediate kat_ax_2_lang : lbase.

Remaining axioms for Kleene algebra

  Section ThirdAxiom.

    Variables l1 l2 : language.

    Lemma forall_n_closure_lang : ∀ l,
      (∀ n:nat, ((l1{^}n){.}l2) <<= l) → ((l1{*}){.}l2) <<= l.

    Lemma kat_ax3_aux_4 : ∀ l,
      l2 <<= l ∧ (l1{.}l) <<= l →
      (∀ n, ((l1{^}n){.}l2) <<= l).

    Lemma kat_ax3_aux_5 : ∀ x,
      ((l1{.}x){+}l2) <<= x → l2 <<= x ∧ (l1{.}x) <<= x.

    Theorem kat_ax_3_lang : ∀ x,
      ((l1{.}x){+}l2) <<= x → ((l1{*}){.}l2) <<= x.

  End ThirdAxiom.

  Hint Resolve kat_ax_3_lang : lbase.
  Hint Immediate kat_ax_3_lang : lbase.

  Section FourthAxiom.

    Variables l1 l2 : language.

    Lemma forall_n_closure_lang_inv : ∀ l,
      (∀ n, (l2{.}(l1{^}n)) <<= l) →
      (l2{.}(l1{*})) <<= l.

    Lemma kat_ax4_aux_4 : ∀ x,
      l2 <<= x ∧ (x{.}l1) <<= x →
      (∀ n, (l2{.}(l1{^}n)) <<= x).

    Lemma kat_ax4_aux_5 : ∀ x,
      ((x{.}l1){+}l2) <<= x → l2 <<= x ∧ (x{.}l1) <<= x.

    Theorem kat_ax_4_lang : ∀ x,
      ((x{.}l1){+}l2) <<= x → (l2{.}(l1{*})) <<= x.

  End FourthAxiom.

  Hint Resolve kat_ax_4_lang : lbase.
  Hint Immediate kat_ax_4_lang : lbase.

A few more usefull theorems usualy used in making proofs about Kleene algebra

Note : Currently adapting old proofs from and older version

  Section KaBissimulation.

    Lemma Bissimulation_aux_1 : ∀ a b x, (x{+}a{.}x{.}b{*}) <<= (x{+}x{.}b{.}b{*}) → (a{*}{.}x) <<= (x{.}b{*}).

    Lemma ka_bisimulation : ∀ l1 l2 l3, l1{.}l2 == l2{.}l3 → l1{*}{.}l2 == l2{.}(l3{*}).

  End KaBissimulation.

  Lemma ka_denesting : ∀ l1 l2, (l1{+}l2){*} == l1{*}{.}(l2{.}l1{*}){*}.

  Lemma ka_sliding : ∀ l1 l2, (l1{.}l2){*}{.}l1 == l1{.}(l2{.}l1){*}.

Language model of partial derivatives w.r.t. a symbol

  Reserved Notation "x %Lq y" (at level 60).
  Inductive LQ (l:language) : A → language :=
  | in_quo : ∀ x a, (a::x) ?? l → x ?? (l %Lq a)
    where "x %Lq y" := (LQ x y).

Language model of partial derivatives w.r.t. a word

  Reserved Notation "x %Lqw y" (at level 60).
  Inductive LQw (l:language) : word → language :=
  | in_quow : ∀ x w, (w ++ x) ?? l → x ?? (l %Lqw w)
    where "x %Lqw y" := (LQw x y).

  Hint Constructors LQ LQw : lbase.

  Add Morphism LQ : LQ_m.

  Add Morphism LQw with signature LEq ==> (@Logic.eq word) ==> LEq as LQw_m.

Epsilon acceptance

  Inductive RLs : language → Type :=
  | RLs0 : RLs {}
  | RLs1 : RLs {e}
  | RLss : ∀ a : A, RLs {!a}
  | RLsp : ∀ l1 l2 : language, RLs l1 → RLs l2 → RLs (l1{+}l2)
  | RLsc : ∀ l1 l2 : language, RLs l1 → RLs l2 → RLs (l1{.}l2)
  | RLsst : ∀ l : language, RLs l → RLs (l{*}).

  Add Morphism RLs : RLs_m.

  Fixpoint cases_epsilon (l:language)(R:RLs l) : language :=
    (match R in RLs l return RLs l → language with
       | RLs0 ⇒ fun _ ⇒ {}
       | RLs1 ⇒ fun _ ⇒ {e}
       | RLss a ⇒ fun _ ⇒ {}
       | RLsp l1 l2 r r0 ⇒ fun _ ⇒ cases_epsilon l1 r {+} cases_epsilon l2 r0
       | RLsc l1 l2 r r0 ⇒ fun _ ⇒ cases_epsilon l1 r {.} cases_epsilon l2 r0
       | RLsst l0 r ⇒ fun _ ⇒ {e}
     end) R.

  Notation "%L" := cases_epsilon.

Decidability of epsilon acceptance for regular languages

  Lemma cases_epsilon_dec : ∀ l H, {%L l H == {}}+{%L l H == {e}}.

  Definition cases_epsilon_fun (l:language)(R:RLs l) : RLs (%L l R).
  Defined.

  Lemma cases_epsilon_true : ∀ l H, %L l H == {e} → nil ?? l.

  Lemma true_cases_epsilon : ∀ l H, nil ?? l → %L l H == {e}.

  Lemma cases_epsilon_false : ∀ l H, %L l H == {} → ¬ nil ?? l.

  Lemma false_cases_epsilon : ∀ l H, ¬ nil ?? l→ %L l H == {}.

Consistencia do sistema pode ser questionavel : o uso do axioma da extensionalidade de conjuntos!!

  Definition cases_epsilon_RLs_false (l:language)(H:RLs l) : %L l H == {} → RLs (%L l H ) = RLs {}.
  Defined.

  Definition cases_epsilon_RLs_true (l:language)(H:RLs l) : %L l H == {e} → RLs (%L l H ) = RLs {e}.
  Defined.

  Theorem empty_or_empty : ∀ l1 l2, l1{+}l2 == {} ↔ l1 == {} ∧ l2 == {}.

Properties of left-quotients of regular languages

  Section LQProperties.

    Variables (a:A) (SyA:IsSy a).
    Variables (b:A) (SyB:IsSy b).

    Lemma LQ_EmptyL : ∀ a, {} %Lq a == {}.

    Lemma LQ_EpsL : ∀ a, {e} %Lq a == {}.

    Lemma LQ_SyL_eq : a = b → {!a} %Lq b == {e}.

    Lemma LQ_SyL_neq : a ≠ b → {!a} %Lq b == {}.

Expansion of the left quocient of the union of two languages

    Lemma LQ_union : ∀ l1 l2 a, (l1{+}l2) %Lq a == (l1 %Lq a){+}(l2 %Lq a).

    Local Hint Resolve LQ_EmptyL LQ_EpsL LQ_SyL_eq LQ_SyL_neq
      LQ_union : lbase.

    Section LQConcReqs.

      Lemma LangDecompose_to_0 : ∀ l,forall (H:RLs l),
        ∃ l',exists H', l == (cases_epsilon l H){+} l' ∧ (cases_epsilon l' H') == {}.

      Lemma lang_decompose_plus_1 : ∀ l l' H H' a,
        l == (%L l H) {+} l' → %L l' H' == {} → l %Lq a == (l'{+}{e}) %Lq a.

      Lemma LQ_cases_epsilon : ∀ l H a, (%L l H) %Lq a == {}.

      Lemma lang_eq_plus_1 : ∀ l a, l %Lq a == (l{+}{e}) %Lq a.

Intermediate constructions for proving correctness of the partial derivative of a regular expressions, based on the words it describes

      Inductive LQConcSplit : language → language → A → language :=
      | in_lqconcsplit : ∀ l1 l2 s w1 w2,
        w1 ?? (l1 %Lq s) → w2 ?? l2 → (w1++w2) ?? (LQConcSplit l1 l2 s).

      Notation "l %split( x ) m" := (LQConcSplit l m x)(at level 60).

      Add Morphism LQConcSplit : LQConcSplit_m.

      Hint Constructors LQConcSplit : lbase.

      Lemma LQConcSplit_EmptyL : ∀ l1 l2 H1 a,
        %L l1 H1 == {} → (l1{.}l2) %Lq a == l1 %split(a) l2.

      Lemma LQConcIsolate : ∀ l1 l2 a,
        l1 %split(a) l2 == (l1 %Lq a){.}l2.

    End LQConcReqs.

    Lemma SL_conc : ∀ l1 l2 a,forall (H1:RLs l1),
      if cases_epsilon_dec l1 H1 then
        (l1{.}l2) %Lq a == (l1 %Lq a){.}l2
        else
          (l1{.}l2) %Lq a == ((l1 %Lq a){.}l2) {+} (l2 %Lq a).

    Section LQ_StarL_Requirements.

Auxiliary data types for propagating the derivation along l{*}

      Inductive StarL_split : language → A → language :=
      | in_split_union : ∀ n l (H:RLs l) w a, w ?? (l{^}n %Lq a) → w ?? StarL_split l a.

      Inductive StarL_split_pos : language → A → language :=
      | in_starl_split_pos : ∀ n l (H:RLs l) w a, 1 ≤ n → w ?? (l{^}n %Lq a) → w ?? StarL_split_pos l a.

      Inductive StarL_split_pos_red : language → A → language :=
      | in_starl_split_pos_red : ∀ n l (H:RLs l) w a, 1 ≤ n → w ?? LQConcSplit l (l{^}(n-1)) a → w ?? StarL_split_pos_red l a.

      Inductive PlusL_alt : language → language :=
      | in_plusl_alt : ∀ n l (H:RLs l) w, 1 ≤ n → w ?? (l{^}n-1) → w ?? PlusL_alt l.

Now follows a sequence of lemmas that prove the equation of the left-quotient of a star language

      Lemma LQ_StarL_eq_StarL_split : ∀ l (HRl:RLs l) a, l{*} %Lq a == StarL_split l a.

      Lemma LQ_StarL_splits_eq : ∀ l (HRl:RLs l) a, StarL_split l a == StarL_split_pos l a.

      Lemma LConcSplit_unfold : ∀ l (HRl:RLs l) a, StarL_split_pos l a == StarL_split_pos_red l a.

      Lemma StarL_split_pos_red_decompose : ∀ l (H:RLs l) a, StarL_split_pos_red l a == (l %Lq a){.}PlusL_alt l.

      Lemma PlusL_alt_StarL_eq : ∀ l (H:RLs l), PlusL_alt l == l{*}.

      Lemma LQConcSplit_unsplit : ∀ l1 l2 (H1:RLs l1) (H2:RLs l2) a,
        LQConcSplit l1 l2 a == (l1 %Lq a){.}l2.

    End LQ_StarL_Requirements.

    Lemma LQ_StarL : ∀ l (H:RLs l), l{*} %Lq a == (l %Lq a){.}l{*}.

    Lemma LQ_StarL_PlusL_eq : ∀ l a, l{*} %Lq a == l{^+} %Lq a.

  End LQProperties.

Left-quocient of a regular language w.r.t a word

  Section LQwProperties.

    Lemma LQw_nil : ∀ l, l %Lqw [] == l.

    Lemma LQw_sy_LQ_eq : ∀ l (HRl:RLs l) a, l %Lqw [a] == l %Lq a.

    Lemma LQw_split : ∀ l (HRl:RLs l) w1 w2, l %Lqw (w1++w2) == (l %Lqw w1) %Lqw w2.

    Lemma LQw_LQ_cons : ∀ l (HRl:RLs l) a w,
      l %Lqw (a::w) == (l %Lq a) %Lqw w.

    Lemma LQw_EmptyL : ∀ w, LQw {} w == {}.

    Inductive SigmaPlus : language :=
    | in_sp_sy : ∀ a, IsSy a → [a] ?? SigmaPlus
    | in_sp_sy_ins : ∀ a w, IsSy a → w ?? SigmaPlus → (a::w) ?? SigmaPlus.

    Notation "{Sig+}" := SigmaPlus.

    Local Hint Constructors SigmaPlus.

    Lemma LQw_EpsL : ∀ w, (w ?? {Sig+}) → {e} %Lqw w == {}.

    Lemma LQw_SyL_sy_eq : ∀ a (H:IsSy a), {!a} %Lqw [a] == {e}.

    Lemma LQw_SyL_sy_neq : ∀ w a, w ?? {Sig+} → w ≠ [a] → LQw {!a} w == {}.

    Lemma LQw_UnionL : ∀ l1 l2 w, w ?? {Sig+} → (l1{+}l2) %Lqw w == (l1 %Lqw w){+}(l2 %Lqw w).

  End LQwProperties.

Words as members of partial derivatives w.r.t words

Lemma w_in_Lang_eq_nil_in_LQw : ∀ w l, w ?? l → [] ?? LQw l w.

Lemma nil_in_LQw_eq_w_in_lang : ∀ w l, [] ?? LQw l w → w ?? l.

Language of the derivative w.r.t all words

End Language.