Library theories.re_sets
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 reg_expr.
Module RegExprSets(a:Alphabet).
Export a.
Module Re := RegExpr(a).
Export Re.
Require Import Setoid.
Require Export FSets.
Require Export Ensembles Constructive_sets.
Require Import ProofIrrelevance ProofIrrelevanceFacts.
Require Import Program.
Require Import alphabet.
Require Import reg_expr.
Module RegExprSets(a:Alphabet).
Export a.
Module Re := RegExpr(a).
Export Re.
Sets of regular expressions : definition of the ordered type
Defining sets of regular expressions
Module ReElem <: OrderedType.
Definition t := re.
Definition eq := @Logic.eq re.
Definition lt := lt_re.
Lemma eq_refl : ∀ x : t, eq x x.
Lemma eq_sym : ∀ x y : t, eq x y → eq y x.
Lemma eq_trans : ∀ x y z : t, eq x y → eq y z → eq x z.
Lemma lt_trans : ∀ x y z : t, lt x y → lt y z → lt x z.
Lemma lt_not_eq : ∀ x y : t, lt x y → ¬ eq x y.
Lemma eq_dec : ∀ x y, {eq x y}+{~eq x y}.
Definition compare : ∀ x y : t, Compare lt eq x y.
End ReElem.
Module reset := FSetAVL.Make(ReElem).
Module resetp := Properties(reset).
Module resetf := Facts(reset).
Module resetd := Decide(reset).
Notation Sre := reset.t.
Notation "[?{}]" := reset.Empty.
Notation "[{}]" := reset.empty.
Notation "[! s ]" := (reset.singleton s)(at level 0).
Notation "x ? y" := (reset.In x y)(at level 60).
Notation "x ~? y" := (~(x ? y))(at level 45).
Notation "# x" := (reset.cardinal x)(at level 30).
Notation "x [=] y" := (reset.Equal x y)(at level 60).
Notation "x [!=] y" := (~(x[=]y))(at level 60).
Notation "x [<=] y" := (reset.Subset x y)(at level 60).
Notation "x [@] y" := (reset.add x y)(at level 60).
Notation "x [+] y" := (reset.union x y)(at level 60).
Notation "x [&] y" := (reset.inter x y)(at level 60).
Notation "'[{F}](' f ',' s ',' d ')'" := (reset.fold (f) s d)(at level 30).
Lemma compat_bool_true : ∀ f:re->bool, compat_bool Logic.eq f.
Definition t := re.
Definition eq := @Logic.eq re.
Definition lt := lt_re.
Lemma eq_refl : ∀ x : t, eq x x.
Lemma eq_sym : ∀ x y : t, eq x y → eq y x.
Lemma eq_trans : ∀ x y z : t, eq x y → eq y z → eq x z.
Lemma lt_trans : ∀ x y z : t, lt x y → lt y z → lt x z.
Lemma lt_not_eq : ∀ x y : t, lt x y → ¬ eq x y.
Lemma eq_dec : ∀ x y, {eq x y}+{~eq x y}.
Definition compare : ∀ x y : t, Compare lt eq x y.
End ReElem.
Module reset := FSetAVL.Make(ReElem).
Module resetp := Properties(reset).
Module resetf := Facts(reset).
Module resetd := Decide(reset).
Notation Sre := reset.t.
Notation "[?{}]" := reset.Empty.
Notation "[{}]" := reset.empty.
Notation "[! s ]" := (reset.singleton s)(at level 0).
Notation "x ? y" := (reset.In x y)(at level 60).
Notation "x ~? y" := (~(x ? y))(at level 45).
Notation "# x" := (reset.cardinal x)(at level 30).
Notation "x [=] y" := (reset.Equal x y)(at level 60).
Notation "x [!=] y" := (~(x[=]y))(at level 60).
Notation "x [<=] y" := (reset.Subset x y)(at level 60).
Notation "x [@] y" := (reset.add x y)(at level 60).
Notation "x [+] y" := (reset.union x y)(at level 60).
Notation "x [&] y" := (reset.inter x y)(at level 60).
Notation "'[{F}](' f ',' s ',' d ')'" := (reset.fold (f) s d)(at level 30).
Lemma compat_bool_true : ∀ f:re->bool, compat_bool Logic.eq f.
Lemma reset_union_empty : ∀ s, s[+][{}][=]s.
Hint Resolve compat_bool_true reset_union_empty : lbase.
Add Morphism reset.filter : resetfilter_m.
Hint Resolve compat_bool_true reset_union_empty : lbase.
Add Morphism reset.filter : resetfilter_m.
Filter empty
Lemma reset_filter_empty : ∀ f, reset.filter f [{}] [=] [{}].
Filter singleton
Lemma reset_filter_subset : ∀ (f:re->bool) s, reset.filter f s [≤] s.
Filter add
Lemma reset_filter_add : ∀ s x (f:re->bool),
reset.filter f (x[@]s) [=] if f x then [!x][+]reset.filter f s else reset.filter f s.
Lemma reset_filter_non_empty_ex : ∀ s1 s2, reset.inter s1 s2 [!=][{}] → ∃ z, z ? s1 ∧ z ? s2.
Lemma reset_filter_ex_non_empty : ∀ s1 s2, (∃ z, z ? s1 ∧ z ? s2) → reset.inter s1 s2 [!=][{}].
reset.filter f (x[@]s) [=] if f x then [!x][+]reset.filter f s else reset.filter f s.
Lemma reset_filter_non_empty_ex : ∀ s1 s2, reset.inter s1 s2 [!=][{}] → ∃ z, z ? s1 ∧ z ? s2.
Lemma reset_filter_ex_non_empty : ∀ s1 s2, (∃ z, z ? s1 ∧ z ? s2) → reset.inter s1 s2 [!=][{}].
Module ReSetSetElem <: DecidableType.
Definition t := Sre.
Definition eq := reset.Equal.
Lemma eq_refl : ∀ x : t, eq x x.
Lemma eq_sym : ∀ x y : t, eq x y → eq y x.
Lemma eq_trans : ∀ x y z : t, eq x y → eq y z → eq x z.
Lemma eq_dec : ∀ x y : t, { eq x y } + { ¬ eq x y }.
End ReSetSetElem.
Module resets := FSetWeakList.Make(ReSetSetElem).
Module resetsp := Properties(resets).
Module resetsf := Facts(resets).
Module resetsd := Decide(resets).
Notation SSre := resets.t.
Notation "[?{{}}]" := resets.Empty.
Notation "[{{}}]" := resets.empty.
Notation "[{! s }]" := (resets.singleton s)(at level 0).
Notation "x ??? y" := (resets.In x y)(at level 60).
Notation "x ~??? y" := (~(x ??? y))(at level 45).
Notation "## x" := (resets.cardinal x)(at level 30).
Notation "x [{=}] y" := (resets.Equal x y)(at level 60).
Notation "x [{!=}] y" := (~(x[{=}]y))(at level 60).
Notation "x [{<=}] y" := (resets.Subset x y)(at level 60).
Notation "x [{@}] y" := (resets.add x y)(at level 60).
Infix "[{+}]" := resets.union(at level 60).
Definition t := Sre.
Definition eq := reset.Equal.
Lemma eq_refl : ∀ x : t, eq x x.
Lemma eq_sym : ∀ x y : t, eq x y → eq y x.
Lemma eq_trans : ∀ x y z : t, eq x y → eq y z → eq x z.
Lemma eq_dec : ∀ x y : t, { eq x y } + { ¬ eq x y }.
End ReSetSetElem.
Module resets := FSetWeakList.Make(ReSetSetElem).
Module resetsp := Properties(resets).
Module resetsf := Facts(resets).
Module resetsd := Decide(resets).
Notation SSre := resets.t.
Notation "[?{{}}]" := resets.Empty.
Notation "[{{}}]" := resets.empty.
Notation "[{! s }]" := (resets.singleton s)(at level 0).
Notation "x ??? y" := (resets.In x y)(at level 60).
Notation "x ~??? y" := (~(x ??? y))(at level 45).
Notation "## x" := (resets.cardinal x)(at level 30).
Notation "x [{=}] y" := (resets.Equal x y)(at level 60).
Notation "x [{!=}] y" := (~(x[{=}]y))(at level 60).
Notation "x [{<=}] y" := (resets.Subset x y)(at level 60).
Notation "x [{@}] y" := (resets.add x y)(at level 60).
Infix "[{+}]" := resets.union(at level 60).
Adding a new element to each inhabitant of the set of sets
Definition add x (m : SSre) : SSre :=
resets.fold (fun s acc ⇒ resets.add (reset.add x s) acc ) m resets.empty.
resets.fold (fun s acc ⇒ resets.add (reset.add x s) acc ) m resets.empty.
Effective construction of the powerset from a set of regular expressions
Definition powerset (s : Sre) : SSre :=
reset.fold add s [{{}}].
Section ReSetSProperties.
Lemma resets_compat_op : ∀ x0,
compat_op reset.Equal resets.Equal
(fun (s1 : resets.elt) (acc : SSre) ⇒ (x0[@]s1)[{@}]acc).
Lemma resets_transpose : ∀ x0,
transpose resets.Equal
(fun (s1 : resets.elt) (acc : SSre) ⇒ (x0[@]s1)[{@}]acc).
End ReSetSProperties.
Add Morphism add : add_m.
Add Morphism powerset : powerset_m.
reset.fold add s [{{}}].
Section ReSetSProperties.
Lemma resets_compat_op : ∀ x0,
compat_op reset.Equal resets.Equal
(fun (s1 : resets.elt) (acc : SSre) ⇒ (x0[@]s1)[{@}]acc).
Lemma resets_transpose : ∀ x0,
transpose resets.Equal
(fun (s1 : resets.elt) (acc : SSre) ⇒ (x0[@]s1)[{@}]acc).
End ReSetSProperties.
Add Morphism add : add_m.
Add Morphism powerset : powerset_m.
Powerset invariants
Lemma add_spec : ∀ x m s, s ??? (add x m) ↔
(s ??? m ∨ ∃ s', s' ??? m ∧ (x[@]s')[=] s).
Lemma powerset_spec : ∀ s s',
s' ??? (powerset s) ↔ s'[≤] s.
(s ??? m ∨ ∃ s', s' ??? m ∧ (x[@]s')[=] s).
Lemma powerset_spec : ∀ s s',
s' ??? (powerset s) ↔ s'[≤] s.
Module ReSetPairElem <: DecidableType.
Definition t := prod Sre Sre.
Definition eq (x y:t) := fst x [=] fst y ∧ snd x [=] snd y.
Lemma eq_refl : ∀ x : t, eq x x.
Lemma eq_sym : ∀ x y : t, eq x y → eq y x.
Lemma eq_trans : ∀ x y z : t, eq x y → eq y z → eq x z.
Lemma eq_dec : ∀ x y : t, { eq x y } + { ¬ eq x y }.
End ReSetPairElem.
Lemma eq_equiv : @Equivalence _ (ReSetPairElem.eq).
Add Parametric Relation : ReSetPairElem.t ReSetPairElem.eq
reflexivity proved by (@Equivalence_Reflexive _ _ eq_equiv)
symmetry proved by (@Equivalence_Symmetric _ _ eq_equiv)
transitivity proved by (@Equivalence_Transitive _ _ eq_equiv) as eq_rel.
Module repset := FSetWeakList.Make(ReSetPairElem).
Module repsetp := Properties(repset).
Module repsetf := Facts(repset).
Module repsetd := Decide(repset).
Notation Srep := repset.t.
Notation "[?{}$]" := repset.Empty.
Notation "[{}$]" := repset.empty.
Notation "[! s , t $]" := (repset.singleton (pair s t))(at level 0,right associativity).
Notation "x ?$ y" := (repset.In x y)(at level 60).
Notation "x !?$ y" := (~(x ?$ y))(at level 45).
Notation "#$ x" := (repset.cardinal x)(at level 30).
Notation "x [=$] y" := (repset.Equal x y)(at level 60).
Notation "x [!=$] y" := (~(x[=$]y))(at level 60).
Notation "x [<=$] y" := (repset.Subset x y)(at level 60).
Notation "x [@$] y" := (repset.add x y)(at level 60).
Notation "x [+$] y" := (repset.union x y)(at level 60).
Notation "x [&$] y" := (repset.inter x y)(at level 60).
Notation "[<-$] x" := (repset.choose x)(at level 0).
Definition t := prod Sre Sre.
Definition eq (x y:t) := fst x [=] fst y ∧ snd x [=] snd y.
Lemma eq_refl : ∀ x : t, eq x x.
Lemma eq_sym : ∀ x y : t, eq x y → eq y x.
Lemma eq_trans : ∀ x y z : t, eq x y → eq y z → eq x z.
Lemma eq_dec : ∀ x y : t, { eq x y } + { ¬ eq x y }.
End ReSetPairElem.
Lemma eq_equiv : @Equivalence _ (ReSetPairElem.eq).
Add Parametric Relation : ReSetPairElem.t ReSetPairElem.eq
reflexivity proved by (@Equivalence_Reflexive _ _ eq_equiv)
symmetry proved by (@Equivalence_Symmetric _ _ eq_equiv)
transitivity proved by (@Equivalence_Transitive _ _ eq_equiv) as eq_rel.
Module repset := FSetWeakList.Make(ReSetPairElem).
Module repsetp := Properties(repset).
Module repsetf := Facts(repset).
Module repsetd := Decide(repset).
Notation Srep := repset.t.
Notation "[?{}$]" := repset.Empty.
Notation "[{}$]" := repset.empty.
Notation "[! s , t $]" := (repset.singleton (pair s t))(at level 0,right associativity).
Notation "x ?$ y" := (repset.In x y)(at level 60).
Notation "x !?$ y" := (~(x ?$ y))(at level 45).
Notation "#$ x" := (repset.cardinal x)(at level 30).
Notation "x [=$] y" := (repset.Equal x y)(at level 60).
Notation "x [!=$] y" := (~(x[=$]y))(at level 60).
Notation "x [<=$] y" := (repset.Subset x y)(at level 60).
Notation "x [@$] y" := (repset.add x y)(at level 60).
Notation "x [+$] y" := (repset.union x y)(at level 60).
Notation "x [&$] y" := (repset.inter x y)(at level 60).
Notation "[<-$] x" := (repset.choose x)(at level 0).
Product of sets of regular expressions
Definition prod_aux (x:Sre)(X:SSre) := resets.fold (fun y ⇒ repset.add (pair x y)) X [{}$].
Definition cart_prod (r1 r2:SSre) := resets.fold (fun x ⇒ repset.union (prod_aux x r2)) r1 [{}$].
Notation "x [X$] y" := (cart_prod x y)(at level 60).
Definition cart_prod (r1 r2:SSre) := resets.fold (fun x ⇒ repset.union (prod_aux x r2)) r1 [{}$].
Notation "x [X$] y" := (cart_prod x y)(at level 60).
Auxiliary lemmas for general rewriting on term having fold
Lemma prod_aux_compat_op : compat_op reset.Equal repset.Equal
(fun x : resets.elt ⇒ repset.union (prod_aux x [{{}}])).
Lemma prod_aux_transpose : transpose repset.Equal
(fun x : resets.elt ⇒ repset.union (prod_aux x [{{}}])).
Lemma prod_aux_add_compat_op : ∀ x0, compat_op reset.Equal repset.Equal
(fun y : resets.elt ⇒ repset.add (x0,y)).
Lemma prod_aux_add_transpose : ∀ x0, transpose repset.Equal (fun y : resets.elt ⇒ repset.add (x0,y)).
Lemma prod_aux_empty : ∀ X, prod_aux X [{{}}] [=$] [{}$].
Lemma in_prod_aux : ∀ X x y, y ??? X → pair x y ?$ prod_aux x X.
Lemma prod_aux_in : ∀ X x y, pair x y ?$ prod_aux x X → y ??? X.
Add Morphism prod_aux : prod_aux_m.
Section AuxCarProd.
Lemma cart_prod_compat_op : ∀ x1, compat_op reset.Equal repset.Equal
(fun x : resets.elt ⇒ repset.union (prod_aux x x1)).
Lemma cart_prod_empty_compat_op : compat_op reset.Equal repset.Equal
(fun _ : resets.elt ⇒ repset.union [{}$]).
Lemma cart_prod_transpose : ∀ x1, transpose repset.Equal
(fun x : resets.elt ⇒ repset.union (prod_aux x x1)).
Lemma cart_prod_empty_transpose :
transpose repset.Equal (fun _ : resets.elt ⇒ repset.union [{}$]).
End AuxCarProd.
Add Morphism cart_prod : cart_prod_m.
(fun x : resets.elt ⇒ repset.union (prod_aux x [{{}}])).
Lemma prod_aux_transpose : transpose repset.Equal
(fun x : resets.elt ⇒ repset.union (prod_aux x [{{}}])).
Lemma prod_aux_add_compat_op : ∀ x0, compat_op reset.Equal repset.Equal
(fun y : resets.elt ⇒ repset.add (x0,y)).
Lemma prod_aux_add_transpose : ∀ x0, transpose repset.Equal (fun y : resets.elt ⇒ repset.add (x0,y)).
Lemma prod_aux_empty : ∀ X, prod_aux X [{{}}] [=$] [{}$].
Lemma in_prod_aux : ∀ X x y, y ??? X → pair x y ?$ prod_aux x X.
Lemma prod_aux_in : ∀ X x y, pair x y ?$ prod_aux x X → y ??? X.
Add Morphism prod_aux : prod_aux_m.
Section AuxCarProd.
Lemma cart_prod_compat_op : ∀ x1, compat_op reset.Equal repset.Equal
(fun x : resets.elt ⇒ repset.union (prod_aux x x1)).
Lemma cart_prod_empty_compat_op : compat_op reset.Equal repset.Equal
(fun _ : resets.elt ⇒ repset.union [{}$]).
Lemma cart_prod_transpose : ∀ x1, transpose repset.Equal
(fun x : resets.elt ⇒ repset.union (prod_aux x x1)).
Lemma cart_prod_empty_transpose :
transpose repset.Equal (fun _ : resets.elt ⇒ repset.union [{}$]).
End AuxCarProd.
Add Morphism cart_prod : cart_prod_m.
Properties of the cartesian product of two sets of regular expressions
Lemma cart_prod_empty :
∀ x, [{{}}] [X$] x [=$] [{}$].
Lemma cart_prod_empty_comm :
∀ x, [{{}}] [X$] x [=$] (x [X$] [{{}}]).
Axiom cart_prod_union_left :
∀ x y z, x [X$] (y [{+}] z) [=$] ((x[X$]y)[+$](x[X$]y)).
Axiom cart_prod_union_right :
∀ x y z, ( x [{+}] y) [X$] z [=$] ((x[X$]z)[+$](y[X$]z)).
Axiom in_cart_prod : ∀ s1 s2 x1 x2,
x1 ??? s1 → x2 ??? s2 → (pair x1 x2) ?$ (s1 [X$] s2).
Axiom in_cart_prod_ex : ∀ s1 s2 x1 x2,
pair x1 x2 ?$ (s1[X$]s2) → x1 ??? s1 ∧ x2 ??? s2.
∀ x, [{{}}] [X$] x [=$] [{}$].
Lemma cart_prod_empty_comm :
∀ x, [{{}}] [X$] x [=$] (x [X$] [{{}}]).
Axiom cart_prod_union_left :
∀ x y z, x [X$] (y [{+}] z) [=$] ((x[X$]y)[+$](x[X$]y)).
Axiom cart_prod_union_right :
∀ x y z, ( x [{+}] y) [X$] z [=$] ((x[X$]z)[+$](y[X$]z)).
Axiom in_cart_prod : ∀ s1 s2 x1 x2,
x1 ??? s1 → x2 ??? s2 → (pair x1 x2) ?$ (s1 [X$] s2).
Axiom in_cart_prod_ex : ∀ s1 s2 x1 x2,
pair x1 x2 ?$ (s1[X$]s2) → x1 ??? s1 ∧ x2 ??? s2.
Inductive SreL : Sre → language :=
| in_sre_lang : ∀ (s:Sre)(w:word)(r:re),
r ? s → w ?? (re2rel r) → w ?? (SreL s).
Coercion SreL : Sre >-> language.
Hint Constructors SreL : lbase.
Notation "[{L}] x" := (SreL x)(at level 0).
Add Morphism SreL : SreL_m.
Notation "Y {<=} X" := (Included word Y X)(at level 0).
Lemma SreL_empty : [{}]=={}.
Lemma SreL_singleton : ∀ x,
[{L}][!x] == x.
Lemma SreL_union : ∀ x y,
[{L}] (x[+]y) == [{L}] x {+} [{L}] y.
Lemma SreL_add : ∀ a x,
[{L}](a[@]x) == [{L}] [!a] {+} [{L}] x.
| in_sre_lang : ∀ (s:Sre)(w:word)(r:re),
r ? s → w ?? (re2rel r) → w ?? (SreL s).
Coercion SreL : Sre >-> language.
Hint Constructors SreL : lbase.
Notation "[{L}] x" := (SreL x)(at level 0).
Add Morphism SreL : SreL_m.
Notation "Y {<=} X" := (Included word Y X)(at level 0).
Lemma SreL_empty : [{}]=={}.
Lemma SreL_singleton : ∀ x,
[{L}][!x] == x.
Lemma SreL_union : ∀ x y,
[{L}] (x[+]y) == [{L}] x {+} [{L}] y.
Lemma SreL_add : ∀ a x,
[{L}](a[@]x) == [{L}] [!a] {+} [{L}] x.
Emptyness test for a set of regular expressions
Definition c_of_re_set (s:Sre) := reset.fold (fun x ⇒ orb (%x)) s false.
Notation "$$% x" := (c_of_re_set x)(at level 45).
Lemma c_of_re_set_false : ∀ s, $$% s = false → ∀ x, x ? s → % x = false.
Lemma compat_op_c_of_re_set :
compat_op Logic.eq Logic.eq (fun x0 : reset.elt ⇒ orb (% x0)).
Hint Resolve compat_op_c_of_re_set : lbase.
Lemma transpose_c_of_re_set :
transpose Logic.eq (fun x1 : reset.elt ⇒ orb (% x1)).
Hint Resolve transpose_c_of_re_set : lbase.
Add Morphism c_of_re_set : c_of_re_set_m.
Lemma true_c_of_re_set : ∀ s x, x ? s → % x = true → $$% s = true.
Notation "$$% x" := (c_of_re_set x)(at level 45).
Lemma c_of_re_set_false : ∀ s, $$% s = false → ∀ x, x ? s → % x = false.
Lemma compat_op_c_of_re_set :
compat_op Logic.eq Logic.eq (fun x0 : reset.elt ⇒ orb (% x0)).
Hint Resolve compat_op_c_of_re_set : lbase.
Lemma transpose_c_of_re_set :
transpose Logic.eq (fun x1 : reset.elt ⇒ orb (% x1)).
Hint Resolve transpose_c_of_re_set : lbase.
Add Morphism c_of_re_set : c_of_re_set_m.
Lemma true_c_of_re_set : ∀ s x, x ? s → % x = true → $$% s = true.
Properties of re set emptyness
Lemma c_of_re_set_true : ∀ s, $$%s = true → ∃ x,( x ? s ∧ %x = true).
Lemma false_c_of_re_set : ∀ s, (∀ x, x ? s → % x = false) → $$% s = false.
Lemma c_of_re_set_dec : ∀ s, {$$% s = true}+{$$% s = false}.
End RegExprSets.
Lemma false_c_of_re_set : ∀ s, (∀ x, x ? s → % x = false) → $$% s = false.
Lemma c_of_re_set_dec : ∀ s, {$$% s = true}+{$$% s = false}.
End RegExprSets.