Library LangAlg.algebra
Set Implicit Arguments.
Require Export completeness.
Open Scope expr.
Section language_algebra.
Hypothesis A : Type.
Hypothesis join : A → A → A.
Hypothesis prod : A → A → A.
Hypothesis meet : A → A → A.
Hypothesis inv : A → A.
Hypothesis bottom : A.
Hypothesis unit : A.
Hypothesis eqA : A → A → Prop.
Class lang_sig (eqA : A → A → Prop) join prod meet inv :=
{ eqA_Equivalence : Equivalence eqA;
join_eqA : Proper (eqA ==> eqA ==> eqA) join;
meet_eqA : Proper (eqA ==> eqA ==> eqA) meet;
prod_eqA : Proper (eqA ==> eqA ==> eqA) prod;
inv_eqA : Proper (eqA ==> eqA) inv }.
Hint Constructors lang_sig.
Hypothesis lang_sig : lang_sig eqA join prod meet inv.
Notation " e ⋆ " := (inv e) (at level 10).
Infix " • " := prod (at level 40).
Infix " ∧ " := meet (at level 50).
Infix " ∨ " := join (at level 60).
Infix " == " := eqA (at level 80).
Class lang_alg :=
{ axiom_conv_1 : (unit ⋆) == unit;
axiom_conv_0 : (bottom ⋆) == bottom;
axiom_conv_plus e f: ((e ∨ f)⋆) == (e⋆ ∨ f⋆);
axiom_conv_fois e f: ((e • f)⋆) == (f⋆ • e⋆);
axiom_conv_inter e f: ((e∧f)⋆) == (e⋆ ∧ f⋆);
axiom_conv_conv e : (e ⋆ ⋆) == e;
axiom_plus_com e f : (e∨f) == (f∨e);
axiom_plus_idem e : (e∨e) == e;
axiom_plus_ass e f g : (e∨(f∨g)) == ((e∨f)∨g);
axiom_plus_0 e : (e∨bottom) == e;
axiom_fois_0 e : (e•bottom) == bottom;
axiom_0_fois e : (bottom•e) == bottom;
axiom_plus_fois e f g: ((e ∨ f)•g) == (e•g ∨ f•g);
axiom_fois_plus e f g: (e•(f ∨ g)) == (e•f ∨ e•g);
axiom_inter_0 e : (e∧bottom) == bottom ;
axiom_plus_inter e f g: ((e ∨ f)∧g) == (e∧g ∨ f∧g);
axiom_inter_plus e f : ((e∧f)∨e) == e;
axiom_fois_assoc e f g : (e•(f • g)) == ((e•f)•g);
axiom_fois_1 e : (unit•e) == e;
axiom_1_fois e : (e•unit) == e;
axiom_inter_assoc e f g : (e∧(f ∧ g)) == ((e∧f)∧g);
axiom_inter_comm e f : (e∧f) == (f∧e);
axiom_inter_idem e : (e ∧ e) == e;
axiom_inter_1_fois e f : (unit ∧ (e•f)) == (unit ∧ (e ∧ f));
axiom_inter_1_conv e : (unit ∧ (e⋆)) == (unit ∧ e);
axiom_inter_1_comm_fois e f : ((unit ∧ e)•f) == (f•(unit ∧ e));
axiom_inter_1_inter e f g :
(((unit ∧ e)•f) ∧ g) == ((unit ∧ e)•(f ∧ g)) }.
Hint Constructors lang_alg.
Reserved Notation " σ ⎣ e ⎦ " (at level 10).
Fixpoint interpretation (σ : nat → A) e :=
match e with
| 1 ⇒ unit
| 0 ⇒ bottom
| 𝐄_var a ⇒ σ a
| e + f ⇒ σ ⎣e⎦ ∨ σ ⎣f⎦
| e ⋅ f ⇒ σ ⎣e⎦ • σ ⎣f⎦
| e ∩ f ⇒ σ ⎣e⎦ ∧ σ ⎣f⎦
| e° ⇒ σ⎣e⎦⋆
end
where " σ ⎣ e ⎦ " := (interpretation σ e).
Definition is_lang_alg :=
∀ σ e f, e ≡ f → σ ⎣ e ⎦ == σ ⎣ f ⎦.
Lemma is_lang_alg_ax :
is_lang_alg ↔
(∀ σ e f, ax e f → σ ⎣ e ⎦ == σ ⎣ f ⎦).
Definition is_free_lang_alg :=
is_lang_alg ∧
(∀ e f, (∀ σ, σ ⎣ e ⎦ == σ ⎣ f ⎦) → e ≃ f).
Lemma axiom_is_lang_alg :
lang_alg → is_lang_alg.
Lemma is_free_lang_alg_spec :
is_free_lang_alg ↔ (∀ e f, e ≃ f ↔ (∀ σ, σ ⎣ e ⎦ == σ ⎣ f ⎦)).
Lemma is_lang_alg_axiom :
is_lang_alg → lang_alg.
End language_algebra.
Lemma is_lang_alg_equiv A e j p m i (b u:A) :
lang_sig e j p m i →
is_lang_alg j p m i b u e ↔ lang_alg j p m i b u e.
Section languages.
Hypothesis Σ : Set.
Notation interpr :=
(interpretation
(@language.union Σ) (@language.prod Σ) (@language.intersection Σ)
(@language.mirror Σ) (@language.empty Σ) (@language.unit Σ)).
Definition eqLang (l1 l2 : language Σ) := ∀ w, l1 w ↔ l2 w.
Lemma eqLang_Equivalence : Equivalence eqLang.
Lemma join_eqLang : Proper (eqLang ==> eqLang ==> eqLang) (@union Σ).
Lemma meet_eqLang : Proper (eqLang ==> eqLang ==> eqLang)
(@intersection Σ).
Lemma prod_eqLang : Proper (eqLang ==> eqLang ==> eqLang)
(@language.prod Σ).
Lemma inv_eqLang : Proper (eqLang ==> eqLang) (@mirror Σ).
Lemma to_lang_𝐄_interpretation (σ : assignment nat Σ) e :
⟦e⟧σ ≃ interpr σ e.
Lemma is_lang_alg_languages :
is_lang_alg
(@language.union Σ) (@language.prod Σ) (@language.intersection Σ)
(@mirror Σ) (@language.empty Σ) (@language.unit Σ)
eqLang.
End languages.
Lemma is_lang_alg_𝐄 (X :Set) (d:decidable_set X) :
is_lang_alg
(@𝐄_plus X) (@𝐄_seq X) (@𝐄_inter X)
(@𝐄_conv X) (@𝐄_zero X) (@𝐄_one X) (fun e f ⇒ e ≡ f).
Section funky_alg.
Hypothesis A : Type.
Hypothesis B : Type.
Hypothesis eqA : A → A → Prop.
Hypothesis join : A → A → A.
Hypothesis prod : A → A → A.
Hypothesis meet : A → A → A.
Hypothesis inv : A → A.
Hypothesis bottom : A.
Hypothesis unit : A.
Hypothesis eqB : B → B → Prop.
Hypothesis π : A → B.
Hypothesis ρ : B → A.
Class funky_alg_sig
(eqA : A → A → Prop) (join prod meet : A → A → A)
(inv : A → A) (bottom unit : A)
(eqB : B → B → Prop) (π : A → B) (ρ : B → A)
:= { funky_lang_sig :> lang_sig eqA join prod meet inv;
eqB_Equivalence : Equivalence eqB}.
Hypothesis funky : funky_alg_sig eqA join prod meet inv
bottom unit eqB π ρ.
Infix " == " := eqA (at level 80).
Notation " e ⋆ " := (inv e) (at level 10).
Infix " • " := prod (at level 40).
Infix " ∧ " := meet (at level 50).
Infix " ∨ " := join (at level 60).
Notation " ⊤ " := unit.
Notation " ⊥ " := bottom.
Infix " ==' " := eqB (at level 80).
Class funky_alg :=
{ ρ_morph : Proper (eqB ==> eqA) ρ;
ρπ : ∀ a, ρ (π a) == ⊤ ∧ a;
π_prod : ∀ a b, π (a • b) ==' π (a ∧ b);
π_inv : ∀ a, π (a⋆) ==' π a;
funky_ax_conv_1 : ⊤ ⋆ == ⊤ ;
funky_ax_conv_0 : ⊥ ⋆ == ⊥ ;
funky_ax_conv_plus e f: (e ∨ f)⋆ == e⋆ ∨ f⋆ ;
funky_ax_conv_fois e f: ((e • f)⋆) == (f⋆ • e⋆) ;
funky_ax_conv_inter e f: ((e∧f)⋆) == (e⋆ ∧ f⋆) ;
funky_ax_conv_conv e : (e ⋆ ⋆) == e ;
funky_ax_plus_com e f : (e∨f) == (f∨e) ;
funky_ax_plus_idem e : (e∨e) == e ;
funky_ax_plus_ass e f g : (e∨(f∨g)) == ((e∨f)∨g) ;
funky_ax_plus_0 e : (e∨⊥) == e ;
funky_ax_fois_0 e : (e•⊥) == ⊥ ;
funky_ax_0_fois e : (⊥•e) == ⊥ ;
funky_ax_plus_fois e f g: ((e ∨ f)•g) == (e•g ∨ f•g) ;
funky_ax_fois_plus e f g: (e•(f ∨ g)) == (e•f ∨ e•g) ;
funky_ax_inter_0 e : (e∧⊥) == ⊥ ;
funky_ax_plus_inter e f g: ((e ∨ f)∧g) == (e∧g ∨ f∧g) ;
funky_ax_inter_plus e f : ((e∧f)∨e) == e ;
funky_ax_fois_assoc e f g : (e•(f • g)) == ((e•f)•g) ;
funky_ax_fois_1 e : (⊤•e) == e ;
funky_ax_1_fois e : (e•⊤) == e ;
funky_ax_inter_assoc e f g : (e∧(f ∧ g)) == ((e∧f)∧g) ;
funky_ax_inter_comm e f : (e∧f) == (f∧e) ;
funky_ax_inter_idem e : (e ∧ e) == e ;
funky_ax_ρ_prod a b : (a • (ρ b)) == ((ρ b) • a) ;
funky_ax_ρ_prod_meet a b c :
(((ρ b) • a) ∧ c) == ((ρ b) • (a ∧ c)) }.
Lemma funky_is_lang_alg :
funky_alg →
is_lang_alg join prod meet inv bottom unit eqA.
End funky_alg.
Lemma funky_𝐄 (X : Set) :
funky_alg_sig (fun e f ⇒ e≡f) (@𝐄_plus X) (@𝐄_seq X)
(@𝐄_inter X) (@𝐄_conv X) (@𝐄_zero X) (@𝐄_one X)
(fun e f ⇒ 1 ∩ e ≡ 1 ∩ f)
(fun e ⇒ e) (fun e ⇒ 1 ∩ e).
Lemma funky_alg_𝐄 (X : Set) :
funky_alg (fun e f ⇒ e ≡ f) (@𝐄_plus X) (@𝐄_seq X) (@𝐄_inter X)
(@𝐄_conv X) (@𝐄_zero X) (@𝐄_one X)
(fun e f ⇒ 1 ∩ e ≡ 1 ∩ f)
(fun e ⇒ e) (fun e ⇒ 1 ∩ e).
Section lang_to_funky.
Hypothesis A : Type.
Hypothesis join : A → A → A.
Hypothesis prod : A → A → A.
Hypothesis meet : A → A → A.
Hypothesis inv : A → A.
Hypothesis bottom : A.
Hypothesis unit : A.
Hypothesis eqA : A → A → Prop.
Notation " e ⋆ " := (inv e) (at level 10).
Infix " • " := prod (at level 40).
Infix " ∧ " := meet (at level 50).
Infix " ∨ " := join (at level 60).
Infix " == " := eqA (at level 80).
Hypothesis lang_sig : lang_sig eqA join prod meet inv.
Hypothesis lang_alg : lang_alg join prod meet inv bottom unit eqA.
Lemma lang_alg_is_funky_alg_sig :
funky_alg_sig eqA join prod meet inv bottom unit
(fun e f ⇒ unit ∧ e == unit ∧ f)
(fun e ⇒ e) (fun e ⇒ unit ∧ e).
Lemma lang_alg_is_funky_alg :
funky_alg eqA join prod meet inv bottom unit
(fun e f ⇒ unit ∧ e == unit ∧ f)
(fun e ⇒ e) (fun e ⇒ unit ∧ e).
End lang_to_funky.
Section powermonoid.
Hypothesis M : Type.
Hypothesis prod : M → M → M.
Hypothesis unit : M.
Hypothesis inv : M → M.
Notation " e ⋆ " := (inv e) (at level 10).
Infix " • " := prod (at level 40).
Hypothesis left_neutrality : ∀ x, unit • x = x.
Hypothesis right_neutrality : ∀ x, x • unit = x.
Hypothesis associativity : ∀ x y z, x • (y • z) = (x • y) • z.
Hypothesis inv_unit : unit⋆=unit.
Hypothesis inv_inv : ∀ x, x⋆⋆=x.
Hypothesis inv_prod : ∀ x y, (x•y)⋆=y⋆•x⋆.
Hypothesis unit_not_prod : ∀ x y,
x•y = unit → x = unit ∧ y = unit.
Require Import Ensembles Finite_sets Finite_sets_facts.
Notation " { x } " := (Singleton M x).
Definition ε := {unit}.
Definition ø := Empty_set M.
Infix " ∧ " := (Intersection M) (at level 50).
Infix " ∨ " := (Union M) (at level 60).
Inductive inverse (X : Ensemble M) : Ensemble M :=
| inverse_In x : In _ X x → In _ (inverse X) (x⋆).
Notation " x # " := (inverse x) (at level 20).
Infix " ⊑ " := (Included M) (at level 80).
Infix " == " := (Same_set M) (at level 80).
Infix " @@ " := (Add M) (at level 30).
Lemma emptyset_inverse : ø == ø #.
Lemma add_inverse x X : X# @@ x⋆ == (X @@ x) #.
Lemma finite_inverse a : Finite _ a → Finite _ (a#).
Inductive concat X Y : Ensemble M :=
| concat_In x y : In _ X x → In _ Y y → In _ (concat X Y) (x•y).
Infix " @ " := concat (at level 40).
Lemma finite_concat a b :
Finite _ a → Finite _ b → Finite _ (a @ b).
Lemma powermon_lang_sig :
lang_sig (Same_set M) (Union M) concat (Intersection M) inverse.
Lemma powermon_lang_alg :
lang_alg (Union M) concat (Intersection M) inverse
ø ε (Same_set M).
End powermonoid.
Close Scope expr.
Require Export completeness.
Open Scope expr.
Section language_algebra.
Hypothesis A : Type.
Hypothesis join : A → A → A.
Hypothesis prod : A → A → A.
Hypothesis meet : A → A → A.
Hypothesis inv : A → A.
Hypothesis bottom : A.
Hypothesis unit : A.
Hypothesis eqA : A → A → Prop.
Class lang_sig (eqA : A → A → Prop) join prod meet inv :=
{ eqA_Equivalence : Equivalence eqA;
join_eqA : Proper (eqA ==> eqA ==> eqA) join;
meet_eqA : Proper (eqA ==> eqA ==> eqA) meet;
prod_eqA : Proper (eqA ==> eqA ==> eqA) prod;
inv_eqA : Proper (eqA ==> eqA) inv }.
Hint Constructors lang_sig.
Hypothesis lang_sig : lang_sig eqA join prod meet inv.
Notation " e ⋆ " := (inv e) (at level 10).
Infix " • " := prod (at level 40).
Infix " ∧ " := meet (at level 50).
Infix " ∨ " := join (at level 60).
Infix " == " := eqA (at level 80).
Class lang_alg :=
{ axiom_conv_1 : (unit ⋆) == unit;
axiom_conv_0 : (bottom ⋆) == bottom;
axiom_conv_plus e f: ((e ∨ f)⋆) == (e⋆ ∨ f⋆);
axiom_conv_fois e f: ((e • f)⋆) == (f⋆ • e⋆);
axiom_conv_inter e f: ((e∧f)⋆) == (e⋆ ∧ f⋆);
axiom_conv_conv e : (e ⋆ ⋆) == e;
axiom_plus_com e f : (e∨f) == (f∨e);
axiom_plus_idem e : (e∨e) == e;
axiom_plus_ass e f g : (e∨(f∨g)) == ((e∨f)∨g);
axiom_plus_0 e : (e∨bottom) == e;
axiom_fois_0 e : (e•bottom) == bottom;
axiom_0_fois e : (bottom•e) == bottom;
axiom_plus_fois e f g: ((e ∨ f)•g) == (e•g ∨ f•g);
axiom_fois_plus e f g: (e•(f ∨ g)) == (e•f ∨ e•g);
axiom_inter_0 e : (e∧bottom) == bottom ;
axiom_plus_inter e f g: ((e ∨ f)∧g) == (e∧g ∨ f∧g);
axiom_inter_plus e f : ((e∧f)∨e) == e;
axiom_fois_assoc e f g : (e•(f • g)) == ((e•f)•g);
axiom_fois_1 e : (unit•e) == e;
axiom_1_fois e : (e•unit) == e;
axiom_inter_assoc e f g : (e∧(f ∧ g)) == ((e∧f)∧g);
axiom_inter_comm e f : (e∧f) == (f∧e);
axiom_inter_idem e : (e ∧ e) == e;
axiom_inter_1_fois e f : (unit ∧ (e•f)) == (unit ∧ (e ∧ f));
axiom_inter_1_conv e : (unit ∧ (e⋆)) == (unit ∧ e);
axiom_inter_1_comm_fois e f : ((unit ∧ e)•f) == (f•(unit ∧ e));
axiom_inter_1_inter e f g :
(((unit ∧ e)•f) ∧ g) == ((unit ∧ e)•(f ∧ g)) }.
Hint Constructors lang_alg.
Reserved Notation " σ ⎣ e ⎦ " (at level 10).
Fixpoint interpretation (σ : nat → A) e :=
match e with
| 1 ⇒ unit
| 0 ⇒ bottom
| 𝐄_var a ⇒ σ a
| e + f ⇒ σ ⎣e⎦ ∨ σ ⎣f⎦
| e ⋅ f ⇒ σ ⎣e⎦ • σ ⎣f⎦
| e ∩ f ⇒ σ ⎣e⎦ ∧ σ ⎣f⎦
| e° ⇒ σ⎣e⎦⋆
end
where " σ ⎣ e ⎦ " := (interpretation σ e).
Definition is_lang_alg :=
∀ σ e f, e ≡ f → σ ⎣ e ⎦ == σ ⎣ f ⎦.
Lemma is_lang_alg_ax :
is_lang_alg ↔
(∀ σ e f, ax e f → σ ⎣ e ⎦ == σ ⎣ f ⎦).
Definition is_free_lang_alg :=
is_lang_alg ∧
(∀ e f, (∀ σ, σ ⎣ e ⎦ == σ ⎣ f ⎦) → e ≃ f).
Lemma axiom_is_lang_alg :
lang_alg → is_lang_alg.
Lemma is_free_lang_alg_spec :
is_free_lang_alg ↔ (∀ e f, e ≃ f ↔ (∀ σ, σ ⎣ e ⎦ == σ ⎣ f ⎦)).
Lemma is_lang_alg_axiom :
is_lang_alg → lang_alg.
End language_algebra.
Lemma is_lang_alg_equiv A e j p m i (b u:A) :
lang_sig e j p m i →
is_lang_alg j p m i b u e ↔ lang_alg j p m i b u e.
Section languages.
Hypothesis Σ : Set.
Notation interpr :=
(interpretation
(@language.union Σ) (@language.prod Σ) (@language.intersection Σ)
(@language.mirror Σ) (@language.empty Σ) (@language.unit Σ)).
Definition eqLang (l1 l2 : language Σ) := ∀ w, l1 w ↔ l2 w.
Lemma eqLang_Equivalence : Equivalence eqLang.
Lemma join_eqLang : Proper (eqLang ==> eqLang ==> eqLang) (@union Σ).
Lemma meet_eqLang : Proper (eqLang ==> eqLang ==> eqLang)
(@intersection Σ).
Lemma prod_eqLang : Proper (eqLang ==> eqLang ==> eqLang)
(@language.prod Σ).
Lemma inv_eqLang : Proper (eqLang ==> eqLang) (@mirror Σ).
Lemma to_lang_𝐄_interpretation (σ : assignment nat Σ) e :
⟦e⟧σ ≃ interpr σ e.
Lemma is_lang_alg_languages :
is_lang_alg
(@language.union Σ) (@language.prod Σ) (@language.intersection Σ)
(@mirror Σ) (@language.empty Σ) (@language.unit Σ)
eqLang.
End languages.
Lemma is_lang_alg_𝐄 (X :Set) (d:decidable_set X) :
is_lang_alg
(@𝐄_plus X) (@𝐄_seq X) (@𝐄_inter X)
(@𝐄_conv X) (@𝐄_zero X) (@𝐄_one X) (fun e f ⇒ e ≡ f).
Section funky_alg.
Hypothesis A : Type.
Hypothesis B : Type.
Hypothesis eqA : A → A → Prop.
Hypothesis join : A → A → A.
Hypothesis prod : A → A → A.
Hypothesis meet : A → A → A.
Hypothesis inv : A → A.
Hypothesis bottom : A.
Hypothesis unit : A.
Hypothesis eqB : B → B → Prop.
Hypothesis π : A → B.
Hypothesis ρ : B → A.
Class funky_alg_sig
(eqA : A → A → Prop) (join prod meet : A → A → A)
(inv : A → A) (bottom unit : A)
(eqB : B → B → Prop) (π : A → B) (ρ : B → A)
:= { funky_lang_sig :> lang_sig eqA join prod meet inv;
eqB_Equivalence : Equivalence eqB}.
Hypothesis funky : funky_alg_sig eqA join prod meet inv
bottom unit eqB π ρ.
Infix " == " := eqA (at level 80).
Notation " e ⋆ " := (inv e) (at level 10).
Infix " • " := prod (at level 40).
Infix " ∧ " := meet (at level 50).
Infix " ∨ " := join (at level 60).
Notation " ⊤ " := unit.
Notation " ⊥ " := bottom.
Infix " ==' " := eqB (at level 80).
Class funky_alg :=
{ ρ_morph : Proper (eqB ==> eqA) ρ;
ρπ : ∀ a, ρ (π a) == ⊤ ∧ a;
π_prod : ∀ a b, π (a • b) ==' π (a ∧ b);
π_inv : ∀ a, π (a⋆) ==' π a;
funky_ax_conv_1 : ⊤ ⋆ == ⊤ ;
funky_ax_conv_0 : ⊥ ⋆ == ⊥ ;
funky_ax_conv_plus e f: (e ∨ f)⋆ == e⋆ ∨ f⋆ ;
funky_ax_conv_fois e f: ((e • f)⋆) == (f⋆ • e⋆) ;
funky_ax_conv_inter e f: ((e∧f)⋆) == (e⋆ ∧ f⋆) ;
funky_ax_conv_conv e : (e ⋆ ⋆) == e ;
funky_ax_plus_com e f : (e∨f) == (f∨e) ;
funky_ax_plus_idem e : (e∨e) == e ;
funky_ax_plus_ass e f g : (e∨(f∨g)) == ((e∨f)∨g) ;
funky_ax_plus_0 e : (e∨⊥) == e ;
funky_ax_fois_0 e : (e•⊥) == ⊥ ;
funky_ax_0_fois e : (⊥•e) == ⊥ ;
funky_ax_plus_fois e f g: ((e ∨ f)•g) == (e•g ∨ f•g) ;
funky_ax_fois_plus e f g: (e•(f ∨ g)) == (e•f ∨ e•g) ;
funky_ax_inter_0 e : (e∧⊥) == ⊥ ;
funky_ax_plus_inter e f g: ((e ∨ f)∧g) == (e∧g ∨ f∧g) ;
funky_ax_inter_plus e f : ((e∧f)∨e) == e ;
funky_ax_fois_assoc e f g : (e•(f • g)) == ((e•f)•g) ;
funky_ax_fois_1 e : (⊤•e) == e ;
funky_ax_1_fois e : (e•⊤) == e ;
funky_ax_inter_assoc e f g : (e∧(f ∧ g)) == ((e∧f)∧g) ;
funky_ax_inter_comm e f : (e∧f) == (f∧e) ;
funky_ax_inter_idem e : (e ∧ e) == e ;
funky_ax_ρ_prod a b : (a • (ρ b)) == ((ρ b) • a) ;
funky_ax_ρ_prod_meet a b c :
(((ρ b) • a) ∧ c) == ((ρ b) • (a ∧ c)) }.
Lemma funky_is_lang_alg :
funky_alg →
is_lang_alg join prod meet inv bottom unit eqA.
End funky_alg.
Lemma funky_𝐄 (X : Set) :
funky_alg_sig (fun e f ⇒ e≡f) (@𝐄_plus X) (@𝐄_seq X)
(@𝐄_inter X) (@𝐄_conv X) (@𝐄_zero X) (@𝐄_one X)
(fun e f ⇒ 1 ∩ e ≡ 1 ∩ f)
(fun e ⇒ e) (fun e ⇒ 1 ∩ e).
Lemma funky_alg_𝐄 (X : Set) :
funky_alg (fun e f ⇒ e ≡ f) (@𝐄_plus X) (@𝐄_seq X) (@𝐄_inter X)
(@𝐄_conv X) (@𝐄_zero X) (@𝐄_one X)
(fun e f ⇒ 1 ∩ e ≡ 1 ∩ f)
(fun e ⇒ e) (fun e ⇒ 1 ∩ e).
Section lang_to_funky.
Hypothesis A : Type.
Hypothesis join : A → A → A.
Hypothesis prod : A → A → A.
Hypothesis meet : A → A → A.
Hypothesis inv : A → A.
Hypothesis bottom : A.
Hypothesis unit : A.
Hypothesis eqA : A → A → Prop.
Notation " e ⋆ " := (inv e) (at level 10).
Infix " • " := prod (at level 40).
Infix " ∧ " := meet (at level 50).
Infix " ∨ " := join (at level 60).
Infix " == " := eqA (at level 80).
Hypothesis lang_sig : lang_sig eqA join prod meet inv.
Hypothesis lang_alg : lang_alg join prod meet inv bottom unit eqA.
Lemma lang_alg_is_funky_alg_sig :
funky_alg_sig eqA join prod meet inv bottom unit
(fun e f ⇒ unit ∧ e == unit ∧ f)
(fun e ⇒ e) (fun e ⇒ unit ∧ e).
Lemma lang_alg_is_funky_alg :
funky_alg eqA join prod meet inv bottom unit
(fun e f ⇒ unit ∧ e == unit ∧ f)
(fun e ⇒ e) (fun e ⇒ unit ∧ e).
End lang_to_funky.
Section powermonoid.
Hypothesis M : Type.
Hypothesis prod : M → M → M.
Hypothesis unit : M.
Hypothesis inv : M → M.
Notation " e ⋆ " := (inv e) (at level 10).
Infix " • " := prod (at level 40).
Hypothesis left_neutrality : ∀ x, unit • x = x.
Hypothesis right_neutrality : ∀ x, x • unit = x.
Hypothesis associativity : ∀ x y z, x • (y • z) = (x • y) • z.
Hypothesis inv_unit : unit⋆=unit.
Hypothesis inv_inv : ∀ x, x⋆⋆=x.
Hypothesis inv_prod : ∀ x y, (x•y)⋆=y⋆•x⋆.
Hypothesis unit_not_prod : ∀ x y,
x•y = unit → x = unit ∧ y = unit.
Require Import Ensembles Finite_sets Finite_sets_facts.
Notation " { x } " := (Singleton M x).
Definition ε := {unit}.
Definition ø := Empty_set M.
Infix " ∧ " := (Intersection M) (at level 50).
Infix " ∨ " := (Union M) (at level 60).
Inductive inverse (X : Ensemble M) : Ensemble M :=
| inverse_In x : In _ X x → In _ (inverse X) (x⋆).
Notation " x # " := (inverse x) (at level 20).
Infix " ⊑ " := (Included M) (at level 80).
Infix " == " := (Same_set M) (at level 80).
Infix " @@ " := (Add M) (at level 30).
Lemma emptyset_inverse : ø == ø #.
Lemma add_inverse x X : X# @@ x⋆ == (X @@ x) #.
Lemma finite_inverse a : Finite _ a → Finite _ (a#).
Inductive concat X Y : Ensemble M :=
| concat_In x y : In _ X x → In _ Y y → In _ (concat X Y) (x•y).
Infix " @ " := concat (at level 40).
Lemma finite_concat a b :
Finite _ a → Finite _ b → Finite _ (a @ b).
Lemma powermon_lang_sig :
lang_sig (Same_set M) (Union M) concat (Intersection M) inverse.
Lemma powermon_lang_alg :
lang_alg (Union M) concat (Intersection M) inverse
ø ε (Same_set M).
End powermonoid.
Close Scope expr.