# 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: ((ef)⋆) == (e f);
axiom_conv_conv e : (e ) == e;
axiom_plus_com e f : (ef) == (fe);
axiom_plus_idem e : (ee) == e;
axiom_plus_ass e f g : (e∨(fg)) == ((ef)∨g);
axiom_plus_0 e : (ebottom) == e;
axiom_fois_0 e : (ebottom) == bottom;
axiom_0_fois e : (bottome) == bottom;
axiom_plus_fois e f g: ((e f)•g) == (eg fg);
axiom_fois_plus e f g: (e•(f g)) == (ef eg);
axiom_inter_0 e : (ebottom) == bottom ;
axiom_plus_inter e f g: ((e f)∧g) == (eg fg);
axiom_inter_plus e f : ((ef)∨e) == e;
axiom_fois_assoc e f g : (e•(f g)) == ((ef)•g);
axiom_fois_1 e : (unite) == e;
axiom_1_fois e : (eunit) == e;
axiom_inter_assoc e f g : (e∧(f g)) == ((ef)∧g);
axiom_inter_comm e f : (ef) == (fe);
axiom_inter_idem e : (e e) == e;
axiom_inter_1_fois e f : (unit (ef)) == (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 fe 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: ((ef)⋆) == (e f) ;
funky_ax_conv_conv e : (e ) == e ;
funky_ax_plus_com e f : (ef) == (fe) ;
funky_ax_plus_idem e : (ee) == e ;
funky_ax_plus_ass e f g : (e∨(fg)) == ((ef)∨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) == (eg fg) ;
funky_ax_fois_plus e f g: (e•(f g)) == (ef eg) ;
funky_ax_inter_0 e : (e) == ;
funky_ax_plus_inter e f g: ((e f)∧g) == (eg fg) ;
funky_ax_inter_plus e f : ((ef)∨e) == e ;
funky_ax_fois_assoc e f g : (e•(f g)) == ((ef)•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)) == ((ef)∧g) ;
funky_ax_inter_comm e f : (ef) == (fe) ;
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 fef) (@𝐄_plus X) (@𝐄_seq X)
(@𝐄_inter X) (@𝐄_conv X) (@𝐄_zero X) (@𝐄_one X)
(fun e f ⇒ 1 e 1 f)
(fun ee) (fun e ⇒ 1 e).

Lemma funky_alg_𝐄 (X : Set) :
funky_alg (fun e fe f) (@𝐄_plus X) (@𝐄_seq X) (@𝐄_inter X)
(@𝐄_conv X) (@𝐄_zero X) (@𝐄_one X)
(fun e f ⇒ 1 e 1 f)
(fun ee) (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 funit e == unit f)
(fun ee) (fun eunit e).
Lemma lang_alg_is_funky_alg :
funky_alg eqA join prod meet inv bottom unit
(fun e funit e == unit f)
(fun ee) (fun eunit 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, (xy)⋆=yx.
Hypothesis unit_not_prod : x y,
xy = 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) (xy).

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.