Library theories.pdrvs
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 dsr_dsl.
Module PDrvs(a:Alphabet).
Module dsr_dsl_lib := DSR_and_DSL(a).
Export dsr_dsl_lib.
Require Import Setoid.
Require Export FSets.
Require Export Ensembles Constructive_sets.
Require Import ProofIrrelevance ProofIrrelevanceFacts.
Require Import Program.
Require Import alphabet.
Require Import dsr_dsl.
Module PDrvs(a:Alphabet).
Module dsr_dsl_lib := DSR_and_DSL(a).
Export dsr_dsl_lib.
Definition of partial derivative of a regular expression
Reserved Notation "r %d s" (at level 60).
Fixpoint pdrv (r:re)(s:A) :=
match r with
| 0 ⇒ [{}]
| 1 ⇒ [{}]
| s';;_ ⇒
match syeq_dec s' s with
| left _ ⇒ [! 1]
| right _ ⇒ [{}]
end
| x+y ⇒ (x %d s)[+](y %d s)
| x*y ⇒ match c_of_re_dec x with
| left _ ⇒ dsr (x %d s) y
| right _ ⇒ (dsr (x %d s) y)[+](y %d s)
end
| x# ⇒ dsr (x %d s) (x#)
end
where "r %d s" := (pdrv r s).
Reserved Notation "x %de y" (at level 60).
Fixpoint pdrv_ext (r:re)(s:A) : Sre :=
match r with
| 0 ⇒ [{}]
| 1 ⇒ [{}]
| s';;_ ⇒
match syeq_dec s' s with
| left _ ⇒ [! 1]
| right _ ⇒ [{}]
end
| x+y ⇒ (x %de s) [+] (y %de s)
| x*y ⇒ ((x %de s)[.]y) [+] ((c_c_of_re x)[<.](y %de s))
| x# ⇒ (x %de s)[.](x#)
end
where "x %de y" := (pdrv_ext x y).
Lemma pdrv_eq_pdrv_ext : ∀ r a, pdrv r a [=] pdrv_ext r a.
Add Parametric Morphism : pdrv
with signature (@Logic.eq re) ==> (@Logic.eq A) ==> reset.Equal as pdrv_m.
Fixpoint pdrv (r:re)(s:A) :=
match r with
| 0 ⇒ [{}]
| 1 ⇒ [{}]
| s';;_ ⇒
match syeq_dec s' s with
| left _ ⇒ [! 1]
| right _ ⇒ [{}]
end
| x+y ⇒ (x %d s)[+](y %d s)
| x*y ⇒ match c_of_re_dec x with
| left _ ⇒ dsr (x %d s) y
| right _ ⇒ (dsr (x %d s) y)[+](y %d s)
end
| x# ⇒ dsr (x %d s) (x#)
end
where "r %d s" := (pdrv r s).
Reserved Notation "x %de y" (at level 60).
Fixpoint pdrv_ext (r:re)(s:A) : Sre :=
match r with
| 0 ⇒ [{}]
| 1 ⇒ [{}]
| s';;_ ⇒
match syeq_dec s' s with
| left _ ⇒ [! 1]
| right _ ⇒ [{}]
end
| x+y ⇒ (x %de s) [+] (y %de s)
| x*y ⇒ ((x %de s)[.]y) [+] ((c_c_of_re x)[<.](y %de s))
| x# ⇒ (x %de s)[.](x#)
end
where "x %de y" := (pdrv_ext x y).
Lemma pdrv_eq_pdrv_ext : ∀ r a, pdrv r a [=] pdrv_ext r a.
Add Parametric Morphism : pdrv
with signature (@Logic.eq re) ==> (@Logic.eq A) ==> reset.Equal as pdrv_m.
Definition pdrv_set (sre:Sre)(s:A) :=
[{F}](fun x ⇒ reset.union (x %d s) , sre , [{}]).
Notation "x %dS y" := (pdrv_set x y)(at level 60).
Lemma compat_op_pdrv_set : ∀ s,
compat_op (@Logic.eq re) reset.Equal (fun x0 ⇒ reset.union (x0 %d s)).
Lemma transpose_pdrv_set : ∀ s,
transpose reset.Equal (fun x0 ⇒ reset.union (x0 %d s)).
Hint Resolve compat_op_pdrv_set transpose_pdrv_set : lbase.
Add Parametric Morphism (s:A) : (reset.fold (fun x ⇒ reset.union (x %d s)))
with signature reset.Equal ==> (@Logic.eq Sre) ==> reset.Equal as fold_union_m.
Add Morphism pdrv_set : pdrv_set_m.
Lemma pdrv_correct : ∀ r a, (r %d a) == r %Lq a.
[{F}](fun x ⇒ reset.union (x %d s) , sre , [{}]).
Notation "x %dS y" := (pdrv_set x y)(at level 60).
Lemma compat_op_pdrv_set : ∀ s,
compat_op (@Logic.eq re) reset.Equal (fun x0 ⇒ reset.union (x0 %d s)).
Lemma transpose_pdrv_set : ∀ s,
transpose reset.Equal (fun x0 ⇒ reset.union (x0 %d s)).
Hint Resolve compat_op_pdrv_set transpose_pdrv_set : lbase.
Add Parametric Morphism (s:A) : (reset.fold (fun x ⇒ reset.union (x %d s)))
with signature reset.Equal ==> (@Logic.eq Sre) ==> reset.Equal as fold_union_m.
Add Morphism pdrv_set : pdrv_set_m.
Lemma pdrv_correct : ∀ r a, (r %d a) == r %Lq a.
Section Pi.
Definition of support by structural recursion
Fixpoint PI (r:re) : Sre :=
match r with
| 0 ⇒ [{}]
| 1 ⇒ [{}]
| _;;_ ⇒ [!1]
| x+y ⇒ (PI x)[+](PI y)
| x*y ⇒ ((PI x)[.]y)[+](PI y)
| x# ⇒ (PI x)[.](x#)
end.
Definition PISet(r:Sre) :=
reset.fold (fun x ⇒ reset.union (PI x)) r [{}].
Lemma in_pdrv_0 : ~exists y, y ? (PI 0).
Lemma in_pdrv_1 : ~exists y, y ? (PI 1).
Lemma in_pdrv_sy : ∀ y s H, y ? (PI (s;;H)) → y = 1.
Lemma in_pdrv_union : ∀ x y z, x ? (PI (y+z)) →
x ? (PI y) ∨ x ? (PI z).
Lemma in_pdrv_conc : ∀ x y z,
Not_0_1 z → x ? (PI (y*z)) →
x ? (PI z) ∨ ∃ y', x = y'*z ∧ y' ? (PI y).
Lemma in_pdrv_star : ∀ x y,
x ? (PI (y#)) → ∃ y', x = y'*(y#) ∧ y' ? (PI y).
End Pi.
Lemma get_symbol : {x | IsSy x}.
Hint Resolve get_symbol : ret.
Section AllPDrv.
match r with
| 0 ⇒ [{}]
| 1 ⇒ [{}]
| _;;_ ⇒ [!1]
| x+y ⇒ (PI x)[+](PI y)
| x*y ⇒ ((PI x)[.]y)[+](PI y)
| x# ⇒ (PI x)[.](x#)
end.
Definition PISet(r:Sre) :=
reset.fold (fun x ⇒ reset.union (PI x)) r [{}].
Lemma in_pdrv_0 : ~exists y, y ? (PI 0).
Lemma in_pdrv_1 : ~exists y, y ? (PI 1).
Lemma in_pdrv_sy : ∀ y s H, y ? (PI (s;;H)) → y = 1.
Lemma in_pdrv_union : ∀ x y z, x ? (PI (y+z)) →
x ? (PI y) ∨ x ? (PI z).
Lemma in_pdrv_conc : ∀ x y z,
Not_0_1 z → x ? (PI (y*z)) →
x ? (PI z) ∨ ∃ y', x = y'*z ∧ y' ? (PI y).
Lemma in_pdrv_star : ∀ x y,
x ? (PI (y#)) → ∃ y', x = y'*(y#) ∧ y' ? (PI y).
End Pi.
Lemma get_symbol : {x | IsSy x}.
Hint Resolve get_symbol : ret.
Section AllPDrv.
Set of all partial derivatives as proved by Champarnaud & Ziadi
Definition PD(r:re) := [!r][+](PI r).
Lemma PI_upper_bound : ∀ r, le (#(PI r)) (sylen r).
Theorem PD_upper_bound : ∀ r, le (#(PD r)) (S |<r >|).
End AllPDrv.
Lemma PI_upper_bound : ∀ r, le (#(PI r)) (sylen r).
Theorem PD_upper_bound : ∀ r, le (#(PD r)) (S |<r >|).
End AllPDrv.
All partial derivatives w.r.t a symbol belong to PI
Theorem all_pdrv_in_PI : ∀ x r, (x %d r)[≤](PI x).
Transitivity of the PI function
Lemma PI_trans : ∀ x y,
y ? (PI x) → ∀ z, z ? (PI y) → z ? (PI x).
Lemma all_PI_in_PD : ∀ r x,
x ? (PI r) → x ? (PD r).
y ? (PI x) → ∀ z, z ? (PI y) → z ? (PI x).
Lemma all_PI_in_PD : ∀ r x,
x ? (PI r) → x ? (PD r).
Lemma compat_op_leq : compat_op (@Logic.eq re) LEq (fun x ⇒ UnionL (re2rel x)).
Lemma transpose_leq : transpose LEq (fun x ⇒ UnionL (re2rel x)).
Lemma pdrv_set_singleton : ∀ r a,
([!r] %dS a)[=](r %d a).
Lemma pdrv_set_empty : ∀ a,
([{}] %dS a)[=][{}].
Lemma In_pdrv_set : ∀ s x a,
x ? (s %dS a) → ∃ y, y ? s ∧ x ? (y %d a).
Lemma In_pdrv_in_pdrv_set : ∀ s x y a,
y ? (x %d a) → x ? s → y ? (s %dS a).
Hint Resolve pdrv_set_singleton pdrv_set_empty In_pdrv_set In_pdrv_in_pdrv_set : lbase.
Operations on sets of partial derivatives
Lemma pdrv_set_add : ∀ s x a,
((x[@]s) %dS a)[=]((x %d a)[+](s %dS a)).
Lemma pdrv_set_union : ∀ s1 s2 a,
((s1[+]s2) %dS a)[=]((s1 %dS a)[+](s2 %dS a)).
((x[@]s) %dS a)[=]((x %d a)[+](s %dS a)).
Lemma pdrv_set_union : ∀ s1 s2 a,
((s1[+]s2) %dS a)[=]((s1 %dS a)[+](s2 %dS a)).
subset of s that accepts the word given as argument
Lemma In_SreL_elem : ∀ (s:Sre) (w:word),
w ?? SreL s → ∃ r, r ? s ∧ w ?? (re2rel r).
w ?? SreL s → ∃ r, r ? s ∧ w ?? (re2rel r).
word belonging to the language of a bigger set
Lemma In_re2rel_in_SL : ∀ w (r:re),
w ?? re2rel r → ∀ s, r ? s → w ?? (SreL s).
Lemma SreL_add_re_in : ∀ s r, r ? s → s == r[@]s.
Lemma LangOfPdrvSet : ∀ s a, s %dS a == s %Lq a.
Add Morphism fold_conc : fold_conc_M.
Lemma SL_dsr_re0 : ∀ s, s[.]0 == {}.
Lemma SL_dsl_re0 : ∀ s, 0[<.]s == {}.
w ?? re2rel r → ∀ s, r ? s → w ?? (SreL s).
Lemma SreL_add_re_in : ∀ s r, r ? s → s == r[@]s.
Lemma LangOfPdrvSet : ∀ s a, s %dS a == s %Lq a.
Add Morphism fold_conc : fold_conc_M.
Lemma SL_dsr_re0 : ∀ s, s[.]0 == {}.
Lemma SL_dsl_re0 : ∀ s, 0[<.]s == {}.
Lemma LQw_single : ∀ (r:re) a, r %Lqw (a::nil) == r %Lq a.
Lemma LQw_split_app : ∀ w1 w2 r, r %Lqw (w1++w2) == (r %Lqw w1) %Lqw w2.
Reserved Notation "x %dw y" (at level 60).
Fixpoint pdrv_iw (sre:Sre)(w:iword) : Sre :=
match w with
| <[] ⇒ sre
| xs <:: x ⇒ (sre %dw xs) %dS x
end
where "x %dw y" := (pdrv_iw x y).
Lemma LQw_split_app : ∀ w1 w2 r, r %Lqw (w1++w2) == (r %Lqw w1) %Lqw w2.
Reserved Notation "x %dw y" (at level 60).
Fixpoint pdrv_iw (sre:Sre)(w:iword) : Sre :=
match w with
| <[] ⇒ sre
| xs <:: x ⇒ (sre %dw xs) %dS x
end
where "x %dw y" := (pdrv_iw x y).
Simple/base properties
Lemma pdrv_iw_sy_icons : ∀ w r s,
(s %dw (w <:: r))[=] ((s %dw w) %dS r).
Lemma pdrv_iw_sy_nil : ∀ s,
(s %dw <[])[=]s.
Lemma pdrv_iw_empty : ∀ w,
([{}] %dw w)[=][{}].
Add Morphism pdrv_iw : pdrv_iw_m.
(s %dw (w <:: r))[=] ((s %dw w) %dS r).
Lemma pdrv_iw_sy_nil : ∀ s,
(s %dw <[])[=]s.
Lemma pdrv_iw_empty : ∀ w,
([{}] %dw w)[=][{}].
Add Morphism pdrv_iw : pdrv_iw_m.
wprdv expansion by concatenation of two words
Lemma pdrv_iw_app : ∀ w w' s,
(s %dw (w <++ w'))[=](pdrv_iw (s %dw w) w').
Lemma pdrv_iw_union : ∀ w s1 s2,
((s1[+]s2) %dw w)[=]((s1 %dw w)[+](s2 %dw w)).
(s %dw (w <++ w'))[=](pdrv_iw (s %dw w) w').
Lemma pdrv_iw_union : ∀ w s1 s2,
((s1[+]s2) %dw w)[=]((s1 %dw w)[+](s2 %dw w)).
Existance of elements
Lemma in_pdrv_iw_pdrv : ∀ s w x,
x ? (s %dw w) → ∃ y, y ? s ∧ x ? ([!y] %dw w).
Lemma iw_pdrv_in_pdrv : ∀ w s x y,
y ? s → x ? ([!y] %dw w) → x ? (s %dw w).
Lemma pdrv_set_comp : ∀ s x a0 a1,
x ? ((s %dS a1) %dS a0) → x ? (s %dw ((<[]<::a1)<::a0)).
x ? (s %dw w) → ∃ y, y ? s ∧ x ? ([!y] %dw w).
Lemma iw_pdrv_in_pdrv : ∀ w s x y,
y ? s → x ? ([!y] %dw w) → x ? (s %dw w).
Lemma pdrv_set_comp : ∀ s x a0 a1,
x ? ((s %dS a1) %dS a0) → x ? (s %dw ((<[]<::a1)<::a0)).
Derivation of a single regular expression by a word
Definition wpdrv (r:re)(w:list A) :=
pdrv_iw ([!r]) (word_to_iword w).
Notation "x %dW y" := (wpdrv x y)(at level 60).
pdrv_iw ([!r]) (word_to_iword w).
Notation "x %dW y" := (wpdrv x y)(at level 60).
Derivation of a single regular expression by a word
Definition wpdrv_set (s:Sre)(w:list A) :=
s %dw (<@ w).
Notation "x %dWS y" := (wpdrv_set x y)(at level 60).
Add Morphism wpdrv : wpdrv_m.
Add Morphism wpdrv_set : wpdrv_set_m.
Add Morphism wpdrv_set with signature reset.Subset ++> Logic.eq ++> reset.Subset as wpdrv_set_subset.
Lemma wpdrv_nil : ∀ r,
(r %dW nil)[=][!r].
Lemma wpdrv_set_nil : ∀ s,
(s %dWS nil)[=]s.
Lemma wpdrv_set_empty : ∀ w,
([{}] %dWS w)[=][{}].
Lemma wpdrv_sy_nil : ∀ r x,
(r %dW (x::nil))[=]([!r] %dS x).
Lemma wpdrv_cons : ∀ r x w,
(r %dW (w++(x::nil)))[=]( (r %dW w) %dWS (x::nil)).
Lemma wpdrv_app : ∀ r w w',
(r %dW (w++w'))[=]((r %dW w) %dWS w').
Lemma Lqw_Lq_app : ∀ w r s, r %Lqw (@>((inil<::s)<++w)) == (r %Lq s) %Lqw (@>w).
Lemma wpdrv_corr : ∀ w r, (r %dw w) == (r %Lqw (@>w)).
Lemma wpdrv_correct : ∀ w r, (r %dW w) == (r %Lqw w).
s %dw (<@ w).
Notation "x %dWS y" := (wpdrv_set x y)(at level 60).
Add Morphism wpdrv : wpdrv_m.
Add Morphism wpdrv_set : wpdrv_set_m.
Add Morphism wpdrv_set with signature reset.Subset ++> Logic.eq ++> reset.Subset as wpdrv_set_subset.
Lemma wpdrv_nil : ∀ r,
(r %dW nil)[=][!r].
Lemma wpdrv_set_nil : ∀ s,
(s %dWS nil)[=]s.
Lemma wpdrv_set_empty : ∀ w,
([{}] %dWS w)[=][{}].
Lemma wpdrv_sy_nil : ∀ r x,
(r %dW (x::nil))[=]([!r] %dS x).
Lemma wpdrv_cons : ∀ r x w,
(r %dW (w++(x::nil)))[=]( (r %dW w) %dWS (x::nil)).
Lemma wpdrv_app : ∀ r w w',
(r %dW (w++w'))[=]((r %dW w) %dWS w').
Lemma Lqw_Lq_app : ∀ w r s, r %Lqw (@>((inil<::s)<++w)) == (r %Lq s) %Lqw (@>w).
Lemma wpdrv_corr : ∀ w r, (r %dw w) == (r %Lqw (@>w)).
Lemma wpdrv_correct : ∀ w r, (r %dW w) == (r %Lqw w).
Lemma all_wpdrv_in_PD : ∀ w x r, x ? ([!r] %dw w) → x ? PD(r).
Lemma word_in_pdrv : ∀ w (r:re), w ?? (re2rel r) → $$% (wpdrv r w) = true.
Lemma word_in_pdrv_true : ∀ w (r:re), $$% (wpdrv r w) = true → w ?? (re2rel r).
Lemma word_in_pdrv : ∀ w (r:re), w ?? (re2rel r) → $$% (wpdrv r w) = true.
Lemma word_in_pdrv_true : ∀ w (r:re), $$% (wpdrv r w) = true → w ?? (re2rel r).
Function PI applied to sets of regular expressions
Definition PIset(s:Sre) := reset.fold (fun x ⇒ reset.union (PI x)) s [{}].
Lemma compat_op_PIset : compat_op Logic.eq reset.Equal
(fun x : reset.elt ⇒ reset.union (PI x)).
Lemma transpose_PIset :
transpose reset.Equal (fun x : reset.elt ⇒ reset.union (PI x)).
Lemma PIset_in_PI : ∀ s x,
s[≤]PI x → PIset s [≤] PI x.
Lemma in_PIset : ∀ s x,
x ? PIset s → ∃ y, y ? s ∧ x ? PI y.
Lemma PIset_in : ∀ s x y,
x ? PI y → y ? s → x ? PIset s.
Lemma subset_PIset : ∀ s t, s[≤]PIset t → ∀ x, x ? s → ∃ y, y ? t ∧ x ? PI y.
End PDrvs.
Lemma compat_op_PIset : compat_op Logic.eq reset.Equal
(fun x : reset.elt ⇒ reset.union (PI x)).
Lemma transpose_PIset :
transpose reset.Equal (fun x : reset.elt ⇒ reset.union (PI x)).
Lemma PIset_in_PI : ∀ s x,
s[≤]PI x → PIset s [≤] PI x.
Lemma in_PIset : ∀ s x,
x ? PIset s → ∃ y, y ? s ∧ x ? PI y.
Lemma PIset_in : ∀ s x y,
x ? PI y → y ? s → x ? PIset s.
Lemma subset_PIset : ∀ s t, s[≤]PIset t → ∀ x, x ? s → ∃ y, y ? t ∧ x ? PI y.
End PDrvs.