regexp.prelude
From mathcomp Require Export all_ssreflect.
From Stdlib Require Export Setoid Relation_Definitions Classes.Morphisms Classes.RelationClasses.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Declare Scope concrete_scope.
Delimit Scope concrete_scope with con.
Declare Scope synthesis_scope.
Delimit Scope synthesis_scope with syn.
Declare Scope language_scope.
Delimit Scope language_scope with lan.
Declare Scope regexp_scope.
Delimit Scope regexp_scope with re.
Lemma foldl_map :
∀ [T1 T2 : Type] (h : T1 → T2) [R : Type] (f : R → T2 → R) (z0 : R) (s : seq T1),
foldl f z0 [seq h i | i <- s] = foldl (fun r ⇒ f r \o h) z0 s.
move ⇒ T1 T2 h R f z0 ss; move: z0.
elim: ss ⇒ [| r ss IH]; by rewrite //=.
Qed.
Section Map.
Context [A B : Type][f : A → B].
Lemma map_nil [xs : seq A] : map f xs = [::] → xs = [::].
case xs; rewrite //=.
Qed.
Lemma map_single [xs : seq A][b : B] :
map f xs = [:: b] → ∃ a, xs = [:: a] ∧ b = f a.
case xs; rewrite //=.
move ⇒ a zs; case ⇒ h1 h2; ∃ a; by rewrite (map_nil h2).
Qed.
Lemma map_catE [ys1 : seq B] : ∀ [xs : seq A] [ys2 : seq B],
map f xs = ys1 ++ ys2 → ∃ xs1 xs2, xs = xs1 ++ xs2 ∧ map f xs1 = ys1 ∧ map f xs2 = ys2.
elim: ys1 ⇒ [| y ys IH].
- by move ⇒ xs ys2; rewrite //=; ∃ [::]; ∃ xs.
- move ⇒ xs ys2; rewrite cat_cons; case xs.
+ rewrite //=.
+ move ⇒ a zs; rewrite //= ⇒ Hyp.
case: Hyp ⇒ Hy /IH Hyp.
case: Hyp ⇒ xs1 [xs2 [Hzs [H1 H2]]].
∃ (a :: xs1); ∃ xs2; by rewrite cat_cons Hzs //= Hy H1.
Qed.
End Map.
Section EqFun.
Check eqfun.
Context {B : Type}{A : B → Type}.
Lemma eqfun_refl (f : ∀ b, A b) : f =1 f.
done.
Qed.
Lemma eqfun_sym (f g : ∀ b, A b) : f =1 g → g =1 f.
move ⇒ hyp; done.
Qed.
Lemma eqfun_trans (f g h : ∀ b, A b) : f =1 g → g =1 h → f =1 h.
move ⇒ hfg hgh x; by rewrite hfg hgh.
Qed.
End EqFun.
Add Parametric Relation B (A : B → Type) : (∀ b, A b) (@eqfun B A)
reflexivity proved by eqfun_refl symmetry proved by eqfun_sym transitivity proved by eqfun_trans as eqfun_equivalence.
From Stdlib Require Export Setoid Relation_Definitions Classes.Morphisms Classes.RelationClasses.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Declare Scope concrete_scope.
Delimit Scope concrete_scope with con.
Declare Scope synthesis_scope.
Delimit Scope synthesis_scope with syn.
Declare Scope language_scope.
Delimit Scope language_scope with lan.
Declare Scope regexp_scope.
Delimit Scope regexp_scope with re.
Lemma foldl_map :
∀ [T1 T2 : Type] (h : T1 → T2) [R : Type] (f : R → T2 → R) (z0 : R) (s : seq T1),
foldl f z0 [seq h i | i <- s] = foldl (fun r ⇒ f r \o h) z0 s.
move ⇒ T1 T2 h R f z0 ss; move: z0.
elim: ss ⇒ [| r ss IH]; by rewrite //=.
Qed.
Section Map.
Context [A B : Type][f : A → B].
Lemma map_nil [xs : seq A] : map f xs = [::] → xs = [::].
case xs; rewrite //=.
Qed.
Lemma map_single [xs : seq A][b : B] :
map f xs = [:: b] → ∃ a, xs = [:: a] ∧ b = f a.
case xs; rewrite //=.
move ⇒ a zs; case ⇒ h1 h2; ∃ a; by rewrite (map_nil h2).
Qed.
Lemma map_catE [ys1 : seq B] : ∀ [xs : seq A] [ys2 : seq B],
map f xs = ys1 ++ ys2 → ∃ xs1 xs2, xs = xs1 ++ xs2 ∧ map f xs1 = ys1 ∧ map f xs2 = ys2.
elim: ys1 ⇒ [| y ys IH].
- by move ⇒ xs ys2; rewrite //=; ∃ [::]; ∃ xs.
- move ⇒ xs ys2; rewrite cat_cons; case xs.
+ rewrite //=.
+ move ⇒ a zs; rewrite //= ⇒ Hyp.
case: Hyp ⇒ Hy /IH Hyp.
case: Hyp ⇒ xs1 [xs2 [Hzs [H1 H2]]].
∃ (a :: xs1); ∃ xs2; by rewrite cat_cons Hzs //= Hy H1.
Qed.
End Map.
Section EqFun.
Check eqfun.
Context {B : Type}{A : B → Type}.
Lemma eqfun_refl (f : ∀ b, A b) : f =1 f.
done.
Qed.
Lemma eqfun_sym (f g : ∀ b, A b) : f =1 g → g =1 f.
move ⇒ hyp; done.
Qed.
Lemma eqfun_trans (f g h : ∀ b, A b) : f =1 g → g =1 h → f =1 h.
move ⇒ hfg hgh x; by rewrite hfg hgh.
Qed.
End EqFun.
Add Parametric Relation B (A : B → Type) : (∀ b, A b) (@eqfun B A)
reflexivity proved by eqfun_refl symmetry proved by eqfun_sym transitivity proved by eqfun_trans as eqfun_equivalence.