Library theories.dsr_dsl
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 re_sets.
Module DSR_and_DSL(a:Alphabet).
Module resets_lib := RegExprSets(a).
Export resets_lib.
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 re_sets.
Module DSR_and_DSL(a:Alphabet).
Module resets_lib := RegExprSets(a).
Export resets_lib.
fold_conc and fold_concl : right/left-concatenation of a regular expression to all the elements
of a finite set of regular expressions
Definition fold_conc (s:Sre)(r:re) :=
[{F}]( (fun x ⇒ reset.add (x*r)) , s , [{}] ).
Definition fold_concl (r:re)(s:Sre) :=
[{F}]( fun x ⇒ reset.add (r*x) , s , [{}] ).
Infix "[{F.}]" := fold_conc(at level 60).
Infix "[{.F}]" := fold_concl(at level 60).
[{F}]( (fun x ⇒ reset.add (x*r)) , s , [{}] ).
Definition fold_concl (r:re)(s:Sre) :=
[{F}]( fun x ⇒ reset.add (r*x) , s , [{}] ).
Infix "[{F.}]" := fold_conc(at level 60).
Infix "[{.F}]" := fold_concl(at level 60).
Main properties of the map concatenation function defined above
Lemma fold_conc_empty : ∀ r,
([{}][{F.}]r) [=] [{}].
Lemma fold_conc_singleton : ∀ x r,
([! x ] [{F.}]r) [=] [!(x*r)].
Lemma fold_concl_empty : ∀ r,
(r[{.F}][{}]) [=] [{}].
Lemma fold_concl_singleton : ∀ x r,
(r[{.F}][!x]) [=] [!r × x].
Local Hint Resolve fold_conc_empty fold_conc_singleton
fold_concl_empty fold_concl_singleton : lbase.
Lemma compat_op_fold_conc : ∀ r,
compat_op (@Logic.eq re) reset.Equal (fun x1 ⇒ reset.add (x1*r)).
Lemma transpose_fold_conc : ∀ r,
transpose reset.Equal (fun x1 ⇒ reset.add (x1*r)).
Lemma compat_op_fold_concl : ∀ r,
compat_op (@Logic.eq re) reset.Equal (fun x1 ⇒ reset.add (r*x1)).
Lemma transpose_fold_concl : ∀ r,
transpose reset.Equal (fun x1 ⇒ reset.add (r*x1)).
Lemma elem_conc_in_fold_conc : ∀ s x r,
x ? s → (x*r) ? (s[{F.}]r).
Lemma elem_conc_in_fold_concl : ∀ s x r,
x ? s → (r*x) ? (r[{.F}]s).
([{}][{F.}]r) [=] [{}].
Lemma fold_conc_singleton : ∀ x r,
([! x ] [{F.}]r) [=] [!(x*r)].
Lemma fold_concl_empty : ∀ r,
(r[{.F}][{}]) [=] [{}].
Lemma fold_concl_singleton : ∀ x r,
(r[{.F}][!x]) [=] [!r × x].
Local Hint Resolve fold_conc_empty fold_conc_singleton
fold_concl_empty fold_concl_singleton : lbase.
Lemma compat_op_fold_conc : ∀ r,
compat_op (@Logic.eq re) reset.Equal (fun x1 ⇒ reset.add (x1*r)).
Lemma transpose_fold_conc : ∀ r,
transpose reset.Equal (fun x1 ⇒ reset.add (x1*r)).
Lemma compat_op_fold_concl : ∀ r,
compat_op (@Logic.eq re) reset.Equal (fun x1 ⇒ reset.add (r*x1)).
Lemma transpose_fold_concl : ∀ r,
transpose reset.Equal (fun x1 ⇒ reset.add (r*x1)).
Lemma elem_conc_in_fold_conc : ∀ s x r,
x ? s → (x*r) ? (s[{F.}]r).
Lemma elem_conc_in_fold_concl : ∀ s x r,
x ? s → (r*x) ? (r[{.F}]s).
Elimination rule for elements of fold_conc
Lemma elem_conc_fold_conc_in : ∀ s x r,
(x*r) ? (s[{F.}]r) → x ? s.
Lemma elem_conc_fold_concl_in : ∀ s x r,
(r*x) ? (r[{.F}]s) → x ? s.
Lemma elem_conc_nin_dsr : ∀ s x r,
x ~? s → (x*r) ~? (s[{F.}]r).
Lemma elem_conc_nin_dsl : ∀ s x r,
x ~? s → (r*x) ~? (r[{.F}]s).
Lemma elem_conc_dsr_nin : ∀ s x r,
(x*r) ~? (s[{F.}]r) →
x ~? s.
Lemma elem_conc_dsl_nin : ∀ s x r,
(r*x) ~? (r[{.F}]s) →
x ~? s.
Lemma elem_conc_in_ex : ∀ s x r,
x ? (s[{F.}]r) → ∃ y, y ? s ∧ x = y*r.
Lemma elem_concl_in_ex : ∀ s x r,
x ? (r[{.F}]s) → ∃ y, y ? s ∧ x = r*y.
Lemma elem_conc_nin_ex : ∀ s x r,
x ~? (s[{F.}]r) → ~exists y, y ? s ∧ x = y*r.
Lemma elem_concl_nin_ex : ∀ s x r,
x ~? (r[{.F}]s) → ~exists y, y ? s ∧ x = r*y.
Lemma elem_conc_ex_nin : ∀ s x r,
x ~? s → ~exists y, (y*r) ? (s[{F.}]r) ∧ x = y.
Lemma elem_concl_ex_nin : ∀ s x r,
x ~? s → ~exists y, (r*y) ? (r[{.F}]s) ∧ x = y.
Add Morphism fold_conc : fold_conc_m.
Add Morphism fold_concl : fold_concl_m.
Lemma fold_conc_add : ∀ s r x x0,
x ? ((reset.add x0 s)[{F.}]r) → x ? (reset.add (x0*r) (s[{F.}]r)).
Lemma fold_concl_add : ∀ s r x x0,
x ? (r[{.F}](reset.add x0 s)) → x ? (reset.add (r*x0) (r[{.F}]s)).
Lemma fold_add_conc : ∀ s r x x0,
x ? (reset.add (x0*r) (s[{F.}]r)) → x ? ((reset.add x0 s)[{F.}]r).
Lemma fold_add_concl : ∀ s r x x0,
x ? (reset.add (r*x0) (r[{.F}]s)) → x ? (r[{.F}](reset.add x0 s)).
Lemma fold_conc_add_eq : ∀ s r x, ((reset.add x s)[{F.}]r)[=](reset.add (x*r) (s[{F.}]r)).
Lemma fold_concl_add_eq : ∀ s r x, (r[{.F}](reset.add x s))[=](reset.add (r*x) (r[{.F}]s)).
Lemma fold_conc_union : ∀ x y r a,
a ? ((x[+]y)[{F.}]r) → a ? ((x[{F.}]r)[+](y[{F.}]r)).
Lemma fold_concl_union : ∀ x y r a,
a ? (r[{.F}](x[+]y)) → a ? ((r[{.F}]x)[+](r[{.F}]y)).
Lemma fold_union_conc : ∀ x y r a,
a ? ((x[{F.}]r)[+](y[{F.}]r)) → a ? ((x[+]y)[{F.}]r).
Lemma fold_union_concl : ∀ x y r a,
a ? ((r[{.F}]x)[+](r[{.F}]y)) →
a ? (r[{.F}](x[+]y)).
Lemma fold_conc_card : ∀ s r,
#(s[{F.}]r) = #s.
Lemma fold_concl_card : ∀ s r,
#(r[{.F}]s) = #s.
Hint Resolve fold_conc_empty fold_conc_singleton
fold_concl_empty fold_concl_singleton : lbase.
Hint Resolve elem_conc_fold_conc_in elem_conc_in_fold_conc elem_conc_in_ex
fold_conc_singleton elem_conc_ex_nin fold_conc_empty fold_add_conc fold_conc_add
fold_conc_union fold_union_conc fold_conc_card : lbase.
Hint Resolve elem_conc_fold_concl_in elem_conc_in_fold_concl elem_concl_in_ex
fold_concl_singleton elem_concl_ex_nin fold_concl_empty fold_add_concl
fold_concl_add fold_concl_union fold_union_concl fold_concl_card : lbase.
(x*r) ? (s[{F.}]r) → x ? s.
Lemma elem_conc_fold_concl_in : ∀ s x r,
(r*x) ? (r[{.F}]s) → x ? s.
Lemma elem_conc_nin_dsr : ∀ s x r,
x ~? s → (x*r) ~? (s[{F.}]r).
Lemma elem_conc_nin_dsl : ∀ s x r,
x ~? s → (r*x) ~? (r[{.F}]s).
Lemma elem_conc_dsr_nin : ∀ s x r,
(x*r) ~? (s[{F.}]r) →
x ~? s.
Lemma elem_conc_dsl_nin : ∀ s x r,
(r*x) ~? (r[{.F}]s) →
x ~? s.
Lemma elem_conc_in_ex : ∀ s x r,
x ? (s[{F.}]r) → ∃ y, y ? s ∧ x = y*r.
Lemma elem_concl_in_ex : ∀ s x r,
x ? (r[{.F}]s) → ∃ y, y ? s ∧ x = r*y.
Lemma elem_conc_nin_ex : ∀ s x r,
x ~? (s[{F.}]r) → ~exists y, y ? s ∧ x = y*r.
Lemma elem_concl_nin_ex : ∀ s x r,
x ~? (r[{.F}]s) → ~exists y, y ? s ∧ x = r*y.
Lemma elem_conc_ex_nin : ∀ s x r,
x ~? s → ~exists y, (y*r) ? (s[{F.}]r) ∧ x = y.
Lemma elem_concl_ex_nin : ∀ s x r,
x ~? s → ~exists y, (r*y) ? (r[{.F}]s) ∧ x = y.
Add Morphism fold_conc : fold_conc_m.
Add Morphism fold_concl : fold_concl_m.
Lemma fold_conc_add : ∀ s r x x0,
x ? ((reset.add x0 s)[{F.}]r) → x ? (reset.add (x0*r) (s[{F.}]r)).
Lemma fold_concl_add : ∀ s r x x0,
x ? (r[{.F}](reset.add x0 s)) → x ? (reset.add (r*x0) (r[{.F}]s)).
Lemma fold_add_conc : ∀ s r x x0,
x ? (reset.add (x0*r) (s[{F.}]r)) → x ? ((reset.add x0 s)[{F.}]r).
Lemma fold_add_concl : ∀ s r x x0,
x ? (reset.add (r*x0) (r[{.F}]s)) → x ? (r[{.F}](reset.add x0 s)).
Lemma fold_conc_add_eq : ∀ s r x, ((reset.add x s)[{F.}]r)[=](reset.add (x*r) (s[{F.}]r)).
Lemma fold_concl_add_eq : ∀ s r x, (r[{.F}](reset.add x s))[=](reset.add (r*x) (r[{.F}]s)).
Lemma fold_conc_union : ∀ x y r a,
a ? ((x[+]y)[{F.}]r) → a ? ((x[{F.}]r)[+](y[{F.}]r)).
Lemma fold_concl_union : ∀ x y r a,
a ? (r[{.F}](x[+]y)) → a ? ((r[{.F}]x)[+](r[{.F}]y)).
Lemma fold_union_conc : ∀ x y r a,
a ? ((x[{F.}]r)[+](y[{F.}]r)) → a ? ((x[+]y)[{F.}]r).
Lemma fold_union_concl : ∀ x y r a,
a ? ((r[{.F}]x)[+](r[{.F}]y)) →
a ? (r[{.F}](x[+]y)).
Lemma fold_conc_card : ∀ s r,
#(s[{F.}]r) = #s.
Lemma fold_concl_card : ∀ s r,
#(r[{.F}]s) = #s.
Hint Resolve fold_conc_empty fold_conc_singleton
fold_concl_empty fold_concl_singleton : lbase.
Hint Resolve elem_conc_fold_conc_in elem_conc_in_fold_conc elem_conc_in_ex
fold_conc_singleton elem_conc_ex_nin fold_conc_empty fold_add_conc fold_conc_add
fold_conc_union fold_union_conc fold_conc_card : lbase.
Hint Resolve elem_conc_fold_concl_in elem_conc_in_fold_concl elem_concl_in_ex
fold_concl_singleton elem_concl_ex_nin fold_concl_empty fold_add_concl
fold_concl_add fold_concl_union fold_union_concl fold_concl_card : lbase.
Partial map for prefixing regular expressions
Definition dsr (s:Sre)(r:re): Sre :=
match r with
| 0 ⇒ [{}]
| 1 ⇒ s
| _ ⇒ s[{F.}]r
end.
Definition dsl (r:re)(s:Sre) : Sre :=
match r with
| 0 ⇒ [{}]
| 1 ⇒ s
| _ ⇒ r[{.F}]s
end.
Notation "x [.] y" := (dsr x y)(at level 60).
Notation "x [<.] y" := (dsl x y)(at level 60).
Hint Unfold dsr dsl.
Lemma dsl_re0 : ∀ s, (0 [<.] s)[=][{}].
Lemma dsr_re0 : ∀ s, (s [.] 0)[=][{}].
Lemma dsr_empty : ∀ r, ([{}][.]r)[=][{}].
Lemma dsl_empty : ∀ r, (r[<.][{}])[=][{}].
Definition Not_0_1 (r:re) := r ≠ 0 ∧ r ≠ 1.
Hint Unfold Not_0_1.
Lemma dsr_singleton : ∀ x r, Not_0_1 r →
([! x] [.] r)[=][!(x*r)].
Lemma dsl_singleton : ∀ x r, Not_0_1 r →
(r [<.] [!x])[=][!(r*x)].
Hint Resolve dsr_singleton dsr_empty dsr_re0 dsl_singleton dsl_empty dsl_re0 : lbase.
Hint Unfold dsr.
Add Morphism dsr : dsr_mor.
Add Morphism dsl : dsl_mor.
Hint Resolve dsr_mor dsl_mor : lbase.
match r with
| 0 ⇒ [{}]
| 1 ⇒ s
| _ ⇒ s[{F.}]r
end.
Definition dsl (r:re)(s:Sre) : Sre :=
match r with
| 0 ⇒ [{}]
| 1 ⇒ s
| _ ⇒ r[{.F}]s
end.
Notation "x [.] y" := (dsr x y)(at level 60).
Notation "x [<.] y" := (dsl x y)(at level 60).
Hint Unfold dsr dsl.
Lemma dsl_re0 : ∀ s, (0 [<.] s)[=][{}].
Lemma dsr_re0 : ∀ s, (s [.] 0)[=][{}].
Lemma dsr_empty : ∀ r, ([{}][.]r)[=][{}].
Lemma dsl_empty : ∀ r, (r[<.][{}])[=][{}].
Definition Not_0_1 (r:re) := r ≠ 0 ∧ r ≠ 1.
Hint Unfold Not_0_1.
Lemma dsr_singleton : ∀ x r, Not_0_1 r →
([! x] [.] r)[=][!(x*r)].
Lemma dsl_singleton : ∀ x r, Not_0_1 r →
(r [<.] [!x])[=][!(r*x)].
Hint Resolve dsr_singleton dsr_empty dsr_re0 dsl_singleton dsl_empty dsl_re0 : lbase.
Hint Unfold dsr.
Add Morphism dsr : dsr_mor.
Add Morphism dsl : dsl_mor.
Hint Resolve dsr_mor dsl_mor : lbase.
Cases of the result of dsr
Lemma dsr_cases : ∀ s r,
(s[.]r)[=][{}] ∨ (s[.]r)[=]s ∨ (Not_0_1 r ∧ (s[.]r)[=](s[{F.}]r)).
Lemma dsl_cases : ∀ s r,
(r[<.]s)[=][{}] ∨ (r[<.]s)[=]s ∨ (Not_0_1 r ∧ (r[<.]s)[=](r[{.F}]s)).
Hint Resolve dsr_cases dsl_cases : lbase.
Lemma elem_conc_dsr_in : ∀ s x r,
Not_0_1 r → x ? s → (x*r) ? (s[.]r).
Lemma elem_conc_dsl_in : ∀ s x r,
Not_0_1 r → x ? s → (r*x) ? (r[<.]s).
Lemma elem_conc_in_dsr : ∀ s x r,
Not_0_1 r → (x*r) ? (s[.]r) → x ? s.
Lemma elem_conc_in_dsl : ∀ s x r,
Not_0_1 r → (r*x) ? (r[<.]s) → x ? s.
Hint Resolve elem_conc_dsr_in elem_conc_in_dsr elem_conc_dsl_in elem_conc_in_dsl : lbase.
Lemma dsr_add : ∀ s x r,
Not_0_1 r → ((x[@]s)[.]r)[=]((x*r)[@](s[.]r)).
Lemma dsl_add : ∀ s x r,
Not_0_1 r → (r[<.](x[@]s))[=]((r*x)[@](r[<.]s)).
(s[.]r)[=][{}] ∨ (s[.]r)[=]s ∨ (Not_0_1 r ∧ (s[.]r)[=](s[{F.}]r)).
Lemma dsl_cases : ∀ s r,
(r[<.]s)[=][{}] ∨ (r[<.]s)[=]s ∨ (Not_0_1 r ∧ (r[<.]s)[=](r[{.F}]s)).
Hint Resolve dsr_cases dsl_cases : lbase.
Lemma elem_conc_dsr_in : ∀ s x r,
Not_0_1 r → x ? s → (x*r) ? (s[.]r).
Lemma elem_conc_dsl_in : ∀ s x r,
Not_0_1 r → x ? s → (r*x) ? (r[<.]s).
Lemma elem_conc_in_dsr : ∀ s x r,
Not_0_1 r → (x*r) ? (s[.]r) → x ? s.
Lemma elem_conc_in_dsl : ∀ s x r,
Not_0_1 r → (r*x) ? (r[<.]s) → x ? s.
Hint Resolve elem_conc_dsr_in elem_conc_in_dsr elem_conc_dsl_in elem_conc_in_dsl : lbase.
Lemma dsr_add : ∀ s x r,
Not_0_1 r → ((x[@]s)[.]r)[=]((x*r)[@](s[.]r)).
Lemma dsl_add : ∀ s x r,
Not_0_1 r → (r[<.](x[@]s))[=]((r*x)[@](r[<.]s)).
Emptyness of dsr and dsl implies emptyness of the set, or that the regular
expressions considered is 0
Lemma dsr_empty_res : ∀ s r, [?{}](s[.]r) → [?{}]s ∨ r = 0.
Lemma dsl_empty_res : ∀ s r, [?{}](r[<.]s) → [?{}]s ∨ r = 0.
Hint Resolve dsr_empty_res dsl_empty_res : lbase.
Lemma dsr_union : ∀ s x r,
((x[+]s)[.]r)[=]((x[.]r)[+](s[.]r)).
Lemma dsl_union : ∀ s x r,
(r[<.](x[+]s))[=]((r[<.]x)[+](r[<.]s)).
Lemma dsr_not_empty : ∀ s r,
¬[?{}] s → r ≠ 0 → ¬[?{}] (s[.]r).
Lemma dsl_not_empty : ∀ s r,
¬[?{}] s → r ≠ 0 → ¬[?{}](r[<.]s).
Hint Resolve dsr_add dsr_union dsr_not_empty dsl_add dsl_union dsl_not_empty : lbase.
Lemma dsl_empty_res : ∀ s r, [?{}](r[<.]s) → [?{}]s ∨ r = 0.
Hint Resolve dsr_empty_res dsl_empty_res : lbase.
Lemma dsr_union : ∀ s x r,
((x[+]s)[.]r)[=]((x[.]r)[+](s[.]r)).
Lemma dsl_union : ∀ s x r,
(r[<.](x[+]s))[=]((r[<.]x)[+](r[<.]s)).
Lemma dsr_not_empty : ∀ s r,
¬[?{}] s → r ≠ 0 → ¬[?{}] (s[.]r).
Lemma dsl_not_empty : ∀ s r,
¬[?{}] s → r ≠ 0 → ¬[?{}](r[<.]s).
Hint Resolve dsr_add dsr_union dsr_not_empty dsl_add dsl_union dsl_not_empty : lbase.
Some counter-example based lemmas
Lemma in_dsr_re0 : ∀ s, ~exists x, x ? (s[.]0).
Lemma in_dsl_re0 : ∀ s, ~exists x, x ? (0[<.]s).
Lemma in_dsr_re_sy : ∀ s a H x,
x ? (s[.]a;;H) →
∃ y, x = y*a;;H ∧ y ? s.
Lemma in_dsl_re_sy : ∀ s a H x,
x ? (a;;H[<.]s) →
∃ y, x = a;;H*y ∧ y ? s.
Lemma in_dsr_re_union : ∀ s x r1 r2,
x ? (s[.](r1+r2)) →
∃ y, x = y*(r1+r2) ∧ y ? s.
Lemma in_dsl_re_union : ∀ s x r1 r2,
x ? ((r1+r2) [<.] s) →
∃ y, x = (r1+r2)*y ∧ y ? s.
Lemma in_dsr_re_conc : ∀ s x r1 r2,
x ? (s[.](r1*r2)) →
∃ y, x = y*(r1*r2) ∧ y ? s.
Lemma in_dsl_re_conc : ∀ s x r1 r2,
x ? ((r1*r2)[<.]s) →
∃ y, x = (r1*r2)*y ∧ y ? s.
Lemma in_dsr_re_star : ∀ s x r,
x ? (s[.](r#)) →
∃ y, x = y*(r#) ∧ y ? s.
Lemma in_dsl_re_star : ∀ s x r,
x ? ((r#)[<.] s) →
∃ y, x = (r#)*y ∧ y ? s.
Lemma in_dsr : ∀ s r x,
Not_0_1 r → x ? (s[.]r) →
∃ y', y' ? s ∧ x = y' × r.
Lemma in_dsl : ∀ s r x,
Not_0_1 r → x ? (r [<.] s) →
∃ y', y' ? s ∧ x = r*y'.
Hint Resolve in_dsr_re0 in_dsr_re_sy in_dsr_re_union in_dsr_re_conc in_dsr_re_star
in_dsr in_dsl_re0 in_dsl_re_sy in_dsl_re_union in_dsl_re_conc in_dsl_re_star
in_dsl : lbase.
Lemma in_dsl_re0 : ∀ s, ~exists x, x ? (0[<.]s).
Lemma in_dsr_re_sy : ∀ s a H x,
x ? (s[.]a;;H) →
∃ y, x = y*a;;H ∧ y ? s.
Lemma in_dsl_re_sy : ∀ s a H x,
x ? (a;;H[<.]s) →
∃ y, x = a;;H*y ∧ y ? s.
Lemma in_dsr_re_union : ∀ s x r1 r2,
x ? (s[.](r1+r2)) →
∃ y, x = y*(r1+r2) ∧ y ? s.
Lemma in_dsl_re_union : ∀ s x r1 r2,
x ? ((r1+r2) [<.] s) →
∃ y, x = (r1+r2)*y ∧ y ? s.
Lemma in_dsr_re_conc : ∀ s x r1 r2,
x ? (s[.](r1*r2)) →
∃ y, x = y*(r1*r2) ∧ y ? s.
Lemma in_dsl_re_conc : ∀ s x r1 r2,
x ? ((r1*r2)[<.]s) →
∃ y, x = (r1*r2)*y ∧ y ? s.
Lemma in_dsr_re_star : ∀ s x r,
x ? (s[.](r#)) →
∃ y, x = y*(r#) ∧ y ? s.
Lemma in_dsl_re_star : ∀ s x r,
x ? ((r#)[<.] s) →
∃ y, x = (r#)*y ∧ y ? s.
Lemma in_dsr : ∀ s r x,
Not_0_1 r → x ? (s[.]r) →
∃ y', y' ? s ∧ x = y' × r.
Lemma in_dsl : ∀ s r x,
Not_0_1 r → x ? (r [<.] s) →
∃ y', y' ? s ∧ x = r*y'.
Hint Resolve in_dsr_re0 in_dsr_re_sy in_dsr_re_union in_dsr_re_conc in_dsr_re_star
in_dsr in_dsl_re0 in_dsl_re_sy in_dsl_re_union in_dsl_re_conc in_dsl_re_star
in_dsl : lbase.
dsr cardinality
Theorem dsr_cardinal : ∀ s r, le (# (s[.]r)) (# s).
dsl cardinality
Theorem dsl_cardinal : ∀ s r, le (# (r[<.]s)) (# s).
Hint Resolve dsr_cardinal dsl_cardinal : lbase.
Hint Resolve dsr_cardinal dsl_cardinal : lbase.
Simple properties of a language of a sets of regular expressions
Lemma LangOfFSet_empty : [{}] == {}.
Lemma LangOfFSet_singleton : ∀ r, [!r] == r.
Lemma LangOfFSet_union : ∀ r1 r2, r1[+]r2 == r1{+}r2.
Lemma LangOfFSet_singleton : ∀ r, [!r] == r.
Lemma LangOfFSet_union : ∀ r1 r2, r1[+]r2 == r1{+}r2.
Lemma LangOfFSet_fconc : ∀ s r,
[{L}] (s[{F.}]r) == ([{L}] s){.}r.
Lemma LangOfFset_dsr : ∀ s r,
[{L}] (s[.]r) == ([{L}] s){.}r.
End DSR_and_DSL.
[{L}] (s[{F.}]r) == ([{L}] s){.}r.
Lemma LangOfFset_dsr : ∀ s r,
[{L}] (s[.]r) == ([{L}] s){.}r.
End DSR_and_DSL.