Library theories.reg_expr

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 language.

Module RegExpr(a:Alphabet).

  Import a.
  Module Lang := Language(a).
  Export Lang.

  Inductive re : Set :=
  | re0 : re
  | re1 : re
  | re_sy : ∀ x, IsSy x → re
  | re_union : re → re → re
  | re_conc : re → re → re
  | re_star : re → re.

  Close Scope nat_scope.
  Hint Constructors re : lbase.

  Notation "0" := re0.
  Notation "1" := re1.
  Notation "s ;; H" := (re_sy s H)(at level 30).
  Notation "x + y" := (re_union x y)(at level 50,left associativity).
  Notation "x × y" := (re_conc x y)(at level 40,left associativity).
  Notation "x #" := (re_star x)(at level 45).

  Fixpoint len_re (r:re) : nat :=
    match r with
      | 0 ⇒ O
      | 1 ⇒ S O
      | _;;_ ⇒ 1%nat
      | x + y ⇒ S (len_re x + len_re y)
      | x × y ⇒ S (len_re x + len_re y)
      | x # ⇒ S (len_re x)
    end.

Symbol-length of regular expressions

  Reserved Notation "|< x >|".
  Fixpoint sylen (r:re) : nat :=
    match r with
      | 0 ⇒ 0%nat
      | 1 ⇒ 0%nat
      | _;;_ ⇒ 1%nat
      | x + y ⇒ (|<x>| + |<y>|)%nat
      | x × y ⇒ (|<x>| + |<y>|)%nat
      | x # ⇒ |<x>|
    end
    where "|< x >|" := (sylen x).

Converting re's to their respective languages

  Fixpoint re2rel (x:re) : language :=
    match x with
      | 0 ⇒ {}
      | 1 ⇒ {e}
      | a;;_ ⇒ {!a}
      | X + Y ⇒ (re2rel X){+}(re2rel Y)
      | X × Y ⇒ (re2rel X){.}(re2rel Y)
      | X # ⇒ (re2rel X){*}
    end.

  Coercion re2rel : re >-> language.

  Add Morphism re2rel : re2rel_m.

  Fixpoint re2RLs (x:re) : RLs (re2rel x) :=
    match x return RLs (re2rel x) with
      | 0 ⇒ RLs0
      | 1 ⇒ RLs1
      | a;;Sya ⇒ RLss a
      | X + Y ⇒ let A := re2RLs X in let B := re2RLs Y in RLsp X Y A B
      | X × Y ⇒ let A := re2RLs X in let B := re2RLs Y in RLsc X Y A B
      | X # ⇒ let A := re2RLs X in RLsst X A
    end.

Equality of regular expressions

Definition LReEq (x y:re) := x == y.

Theorem re2rel_is_RL : ∀ r:re, RL r.

Word of the language of regular expressions is well formed

Lemma re_wf : ∀ r:re, language_wf (r).

Lemma re_sy_dec : ∀ r1 r2:re, {r1=r2}+{r1<>r2}.

Parts of the ordering function for regular expressions

  Definition lt_re0 (x:re) := x ≠ 0.

  Lemma ex_not_lt_re : ∃ x, ~lt_re0 x.

  Lemma not_all_lt_re0 : ~(forall x, lt_re0 x).

  Hint Resolve ex_not_lt_re not_all_lt_re0 : lbase.

Lexicografical less-then ordering for regular expressions

Required only for defining sets of regular expressions

NOTE : Usefull for developing reflexive proof tactics for deriving regular expressions modulo ACI

  Definition lt_re1 (x:re) := x ≠ 0 ∧ x ≠ 1.

  Definition lt_resy (x:re)(s:A) := match x with
                                       | b;;_ ⇒ sylt b s
                                       | _ ⇒ lt_re1 x
                                     end.

  Definition lt_union (a b x:re)(f:re->re->Prop):=
    match x with
      | y+z ⇒ f a y ∨ (a = y ∧ f b z)
      | _*_ ⇒ True
      | _# ⇒ True
      | _ ⇒ False
    end.

  Definition lt_conc (a b x:re)(f:re->re->Prop):=
    match x with
      | y*z ⇒ f a y ∨ (a = y ∧ f b z)
      | _# ⇒ True
      | _ ⇒ False
    end.

  Definition lt_star (a x:re)(f:re->re->Prop):=
    match x with
      | y# ⇒ f a y
      | _ ⇒ False
    end.

Main less than relation for regular expressions

  Reserved Notation "x << y" (at level 60).
  Fixpoint lt_re (x y:re) : Prop :=
    match x with
      | 0 ⇒ lt_re0 y
      | 1 ⇒ lt_re1 y
      | a;;_ ⇒ lt_resy y a
      | a+b ⇒ lt_union a b y lt_re
      | a*b ⇒ lt_conc a b y lt_re
      | a# ⇒ lt_star a y lt_re
    end
    where "x << y" := (lt_re x y).

  Lemma not_lt_re0_refl : ¬ lt_re0 0.

  Lemma not_lt_re1_refl : ¬ lt_re1 1.

  Lemma not_lt_resy_refl : ∀ x i, ¬ lt_resy (x;;i) x.

  Lemma lt_re_1_trans : ∀ z, 1 << z → 0 << z.

  Hint Resolve not_lt_re0_refl not_lt_re1_refl not_lt_resy_refl : lbase.

  Lemma lt_re_nrefl : ∀ r, ~(r << r).

  Hint Resolve lt_re_nrefl : lbase.

  Lemma lt_re_neq : ∀ x y, x << y → ~(x = y).

  Ltac unfold_lt := unfold
    lt_re0,lt_re1,lt_resy,lt_union,lt_conc,lt_star in × |- ×.

  Lemma lt_re_trans : ∀ x y z, x << y → y << z → x << z.

  Hint Resolve lt_re_trans lt_re_neq lt_re_nrefl : lbase.

Constant part of a regular expression

  Reserved Notation "% y" (at level 45,right associativity).
  Fixpoint c_of_re (r:re) : bool :=
    match r with
      | 0 ⇒ false
      | 1 ⇒ true
      | _;;_ ⇒ false
      | _# ⇒ true
      | x+y ⇒ (% x) || (% y)
      | x*y ⇒ (% x) && (% y)
    end
    where "% y" := (c_of_re y).

  Add Morphism c_of_re : c_of_re_m.

Production of the language corresponding to the emptyness of an re.

  Definition lc_of_re (r:re) := if % r then {e} else {}.
  Notation "$% x" := (lc_of_re x)(at level 45).

  Add Morphism lc_of_re : lc_of_re_m.

Production of the re. corresponding to the emptyness of the re. given as argument

Definition c_c_of_re (r:re) := if % r then 1 else 0.
Notation "%$ x" := (c_c_of_re x)(at level 45).

Decidability of emptyness testing for an re.

Lemma c_of_re_dec : ∀ r, {% r = false}+{% r = true}.

Properties of the epsilon operator, and its relatorion to languages

  Lemma c_of_re_cases_epsilon_false : ∀ r, c_of_re r = false → cases_epsilon r (re2RLs r) == {}.

  Lemma cases_epsilon_false_c_of_re : ∀ r:re, cases_epsilon r (re2RLs r) == {} → c_of_re r = false.

  Lemma c_of_re_cases_epsilon_true : ∀ r, c_of_re r = true → cases_epsilon r (re2RLs r) == {e}.

  Lemma cases_epsilon_true_c_of_re : ∀ r:re, cases_epsilon r (re2RLs r) == {e} → c_of_re r = true.

End RegExpr.