RIS.algebra: algebraic structures.
Let A be some type equipped with an equivalence relation ⩵ and a partial order ≦.
Context {A : Type} {eqA: relation A} {leqA : relation A}.
Context {equivA : @Equivalence A eqA} {preA : @PreOrder A leqA}
{partialA : @PartialOrder A eqA equivA leqA preA}.
Infix " ≦ " := leqA (at level 80).
Infix " ⩵ " := eqA (at level 80).
Context {equivA : @Equivalence A eqA} {preA : @PreOrder A leqA}
{partialA : @PartialOrder A eqA equivA leqA preA}.
Infix " ≦ " := leqA (at level 80).
Infix " ⩵ " := eqA (at level 80).
We introduce some notations.
Class Un := un : A.
Notation " 𝟭 " := un.
Class Zero := zero : A.
Notation " 𝟬 " := zero.
Class Product := prod : A → A → A.
Infix " · " := prod (at level 40).
Class Join := join : A → A → A.
Infix " ∪ " := join (at level 45).
Class Star := star : A → A.
Notation " e ⋆ " := (star e) (at level 35).
Notation " 𝟭 " := un.
Class Zero := zero : A.
Notation " 𝟬 " := zero.
Class Product := prod : A → A → A.
Infix " · " := prod (at level 40).
Class Join := join : A → A → A.
Infix " ∪ " := join (at level 45).
Class Star := star : A → A.
Notation " e ⋆ " := (star e) (at level 35).
Class Associative (prod : A → A → A) :=
associative : (∀ a b c : A, prod a (prod b c) ⩵ prod (prod a b) c).
Class Commutative (prod : A → A → A) :=
commutative : (∀ a b : A, prod a b ⩵ prod b a).
Class Idempotent (prod : A → A → A) :=
idempotent : (∀ a : A, prod a a ⩵ a).
Class Unit (prod : A → A → A) (unit : A) :=
{
left_unit : ∀ a : A, prod unit a ⩵ a;
right_unit : ∀ a : A, prod a unit ⩵ a
}.
Class Absorbing (prod : A → A → A) (z : A) :=
{
left_absorbing : ∀ a : A, prod z a ⩵ z;
right_absorbing : ∀ a : A, prod a z ⩵ z
}.
associative : (∀ a b c : A, prod a (prod b c) ⩵ prod (prod a b) c).
Class Commutative (prod : A → A → A) :=
commutative : (∀ a b : A, prod a b ⩵ prod b a).
Class Idempotent (prod : A → A → A) :=
idempotent : (∀ a : A, prod a a ⩵ a).
Class Unit (prod : A → A → A) (unit : A) :=
{
left_unit : ∀ a : A, prod unit a ⩵ a;
right_unit : ∀ a : A, prod a unit ⩵ a
}.
Class Absorbing (prod : A → A → A) (z : A) :=
{
left_absorbing : ∀ a : A, prod z a ⩵ z;
right_absorbing : ∀ a : A, prod a z ⩵ z
}.
Class Monoid (prod : A → A → A) (unit : A) :=
{
mon_assoc :> Associative prod;
mon_unit :> Unit prod unit;
}.
Class Semilattice (join : A → A → A) :=
{
lat_assoc :> Associative join;
lat_comm :> Commutative join;
lat_idem :> Idempotent join;
}.
Class Lattice (m j : A → A → A) :=
{
lat_meet_assoc :> Associative m;
lat_meet_comm :> Commutative m;
lat_join_assoc :> Associative j;
lat_join_comm :> Commutative j;
lat_join_meet : ∀ a b, j a (m a b) ⩵ a;
lat_meet_join : ∀ a b, m a (j a b) ⩵ a;
}.
Class SemiRing (prod add : A → A → A) (u z : A) :=
{
semiring_prod :> Monoid prod u;
semiring_add :> Monoid add z;
semiring_comm :> Commutative add;
semiring_zero :> Absorbing prod z;
semiring_left_distr : ∀ a b c, prod a (add b c) ⩵ add (prod a b) (prod a c);
semiring_right_distr : ∀ a b c, prod (add a b) c ⩵ add (prod a c) (prod b c);
}.
{
mon_assoc :> Associative prod;
mon_unit :> Unit prod unit;
}.
Class Semilattice (join : A → A → A) :=
{
lat_assoc :> Associative join;
lat_comm :> Commutative join;
lat_idem :> Idempotent join;
}.
Class Lattice (m j : A → A → A) :=
{
lat_meet_assoc :> Associative m;
lat_meet_comm :> Commutative m;
lat_join_assoc :> Associative j;
lat_join_comm :> Commutative j;
lat_join_meet : ∀ a b, j a (m a b) ⩵ a;
lat_meet_join : ∀ a b, m a (j a b) ⩵ a;
}.
Class SemiRing (prod add : A → A → A) (u z : A) :=
{
semiring_prod :> Monoid prod u;
semiring_add :> Monoid add z;
semiring_comm :> Commutative add;
semiring_zero :> Absorbing prod z;
semiring_left_distr : ∀ a b c, prod a (add b c) ⩵ add (prod a b) (prod a c);
semiring_right_distr : ∀ a b c, prod (add a b) c ⩵ add (prod a c) (prod b c);
}.
The property JoinOrder states that the partial order we choose
coincides with the natural ordering we get from a join
Semilattice.
An idempotent semi-ring is in particular a semi-lattice.
Global Instance IdemSemiRing_Semilattice p j u z `{SemiRing p j u z} `{Idempotent j} : Semilattice j.
Class KleeneAlgebra (j: Join) (p: Product) (z: Zero) (u:Un) (s:Star) :=
{
proper_prod :> Proper (eqA ==> eqA ==> eqA) prod;
proper_join :> Proper (eqA ==> eqA ==> eqA) join;
proper_star :> Proper (eqA ==> eqA) star;
ka_semiring :> SemiRing prod join un zero;
ka_idem :> Idempotent join;
ka_joinOrder :> JoinOrder join;
ka_star_unfold : ∀ a, 𝟭 ∪ a · a ⋆ ≦ a⋆ ;
ka_star_left_ind : ∀ a b, a · b ≦ b → a ⋆ · b ≦ b;
ka_star_right_ind : ∀ a b, a · b ≦ a → a · b ⋆ ≦ a;
}.
Class BooleanAlgebra (t f : A) (n : A → A) (c d: A → A → A) :=
{
proper_c :> Proper (eqA ==> eqA ==> eqA) c;
proper_d :> Proper (eqA ==> eqA ==> eqA) d;
proper_n :> Proper (eqA ==> eqA) n;
ba_conj_comm :> Commutative c;
ba_disj_comm :> Commutative d;
ba_true : ∀ a, c a t ⩵ a;
ba_false : ∀ a, d a f ⩵ a;
ba_conj_disj : ∀ x y z, c x (d y z) ⩵ d (c x y) (c x z);
ba_disj_conj : ∀ x y z, d x (c y z) ⩵ c (d x y) (d x z);
ba_neg_conj : ∀ a, c a (n a) ⩵ f;
ba_neg_disj : ∀ a, d a (n a) ⩵ t;
}.
End algebra.
Notation " 𝟭 " := un.
Notation " 𝟬 " := zero.
Infix " · " := prod (at level 40).
Infix " ∪ " := join (at level 45).
Notation " e ⋆ " := (star e) (at level 35).
{
proper_prod :> Proper (eqA ==> eqA ==> eqA) prod;
proper_join :> Proper (eqA ==> eqA ==> eqA) join;
proper_star :> Proper (eqA ==> eqA) star;
ka_semiring :> SemiRing prod join un zero;
ka_idem :> Idempotent join;
ka_joinOrder :> JoinOrder join;
ka_star_unfold : ∀ a, 𝟭 ∪ a · a ⋆ ≦ a⋆ ;
ka_star_left_ind : ∀ a b, a · b ≦ b → a ⋆ · b ≦ b;
ka_star_right_ind : ∀ a b, a · b ≦ a → a · b ⋆ ≦ a;
}.
Class BooleanAlgebra (t f : A) (n : A → A) (c d: A → A → A) :=
{
proper_c :> Proper (eqA ==> eqA ==> eqA) c;
proper_d :> Proper (eqA ==> eqA ==> eqA) d;
proper_n :> Proper (eqA ==> eqA) n;
ba_conj_comm :> Commutative c;
ba_disj_comm :> Commutative d;
ba_true : ∀ a, c a t ⩵ a;
ba_false : ∀ a, d a f ⩵ a;
ba_conj_disj : ∀ x y z, c x (d y z) ⩵ d (c x y) (c x z);
ba_disj_conj : ∀ x y z, d x (c y z) ⩵ c (d x y) (d x z);
ba_neg_conj : ∀ a, c a (n a) ⩵ f;
ba_neg_disj : ∀ a, d a (n a) ⩵ t;
}.
End algebra.
Notation " 𝟭 " := un.
Notation " 𝟬 " := zero.
Infix " · " := prod (at level 40).
Infix " ∪ " := join (at level 45).
Notation " e ⋆ " := (star e) (at level 35).
Section booleanAlgebra.
Context {A : Type} {eqA: relation A} {leqA : relation A}.
Context {equivA : @Equivalence A eqA} {preA : @PreOrder A leqA}
{partialA : @PartialOrder A eqA equivA leqA preA}.
Infix " ≦ " := leqA (at level 80).
Infix " ⩵ " := eqA (at level 80).
Context {top bot : A} {neg : A → A} {conj disj : A → A → A}.
Context `{BooleanAlgebra A eqA top bot neg conj disj}.
Notation " ⊤ " := top.
Notation " ⊥ " := bot.
Notation " ¬ " := neg.
Infix " ∧ " := conj (at level 40).
Infix " ∨ " := disj (at level 45).
Context {A : Type} {eqA: relation A} {leqA : relation A}.
Context {equivA : @Equivalence A eqA} {preA : @PreOrder A leqA}
{partialA : @PartialOrder A eqA equivA leqA preA}.
Infix " ≦ " := leqA (at level 80).
Infix " ⩵ " := eqA (at level 80).
Context {top bot : A} {neg : A → A} {conj disj : A → A → A}.
Context `{BooleanAlgebra A eqA top bot neg conj disj}.
Notation " ⊤ " := top.
Notation " ⊥ " := bot.
Notation " ¬ " := neg.
Infix " ∧ " := conj (at level 40).
Infix " ∨ " := disj (at level 45).
When we defined boolean algebra before, we relied on
Huntington's 1904 axiomatization, which differs from the usual way
they are defined, but is much more concise. We now show that this
axiomatization indeed implies all the properties we expect of a
boolean algebra. The following subsection is a straightforward
adaptation of the proofs detailed on the wikipedia page of boolean
algebra:
en.wikipedia.org/wiki/Boolean_algebra_(structure).
Elementary properties
Lemma UId1 o : (∀ x, x ∨ o ⩵ x) → o ⩵ ⊥.
Lemma Idm1 x : x ∨ x ⩵ x.
Lemma Bnd1 x : x ∨ ⊤ ⩵ ⊤.
Lemma Abs1 x y : x ∨ (x ∧ y) ⩵ x.
Lemma UId2 o : (∀ x, x ∧ o ⩵ x) → o ⩵ ⊤.
Lemma Idm2 x : x ∧ x ⩵ x.
Lemma Bnd2 x : x ∧ ⊥ ⩵ ⊥.
Lemma Abs2 x y : x ∧ (x ∨ y) ⩵ x.
Lemma UNg x x' : x ∨ x' ⩵ ⊤ → x ∧ x' ⩵ ⊥ → x' ⩵ ¬ x.
Lemma DNg x : ¬(¬ x) ⩵ x.
Lemma A1 x y : x ∨ (¬ x ∨ y) ⩵ ⊤.
Lemma A2 x y : x ∧ (¬ x ∧ y) ⩵ ⊥.
Lemma B1 x y : (x ∨ y)∨(¬x∧¬y)⩵⊤.
Lemma B2 x y : (x ∧ y)∧(¬x∨¬y)⩵⊥.
Lemma C1 x y : (x ∨ y)∧ (¬x∧¬y)⩵⊥.
Lemma C2 x y : (x ∧ y)∨ (¬x∨¬y)⩵⊤.
Lemma DMg1 x y : ¬ (x∨y) ⩵ ¬ x ∧ ¬ y.
Lemma DMg2 x y : ¬ (x∧y) ⩵ ¬ x ∨ ¬ y.
Lemma D1 x y z : (x∨(y∨z))∨¬x⩵⊤.
Lemma D2 x y z : (x∧(y∧z))∧¬x⩵⊥.
Lemma E1 x y z : y∧(x∨(y∨z))⩵ y.
Lemma E2 x y z : y∨(x∧(y∧z))⩵ y.
Lemma F1 x y z : (x∨(y∨z))∨¬y ⩵ ⊤.
Lemma F2 x y z : (x∧(y∧z))∧¬y ⩵ ⊥.
Lemma G1 x y z : (x ∨(y∨z))∨¬z⩵⊤.
Lemma G2 x y z : (x ∧(y∧z))∧¬z⩵⊥.
Lemma H1 x y z : ¬ ((x∨y)∨z)∧x⩵⊥.
Lemma H2 x y z : ¬ ((x∧y)∧z)∨x⩵⊤.
Lemma I1 x y z : ¬ ((x∨y)∨z)∧y⩵⊥.
Lemma I2 x y z : ¬ ((x∧y)∧z)∨y⩵⊤.
Lemma J1 x y z : ¬((x∨y)∨z)∧z⩵⊥.
Lemma J2 x y z : ¬((x∧y)∧z)∨z⩵⊤.
Lemma K1 x y z : (x∨(y∨z))∨¬((x∨y)∨z)⩵⊤.
Lemma K2 x y z : (x∧(y∧z))∧¬((x∧y)∧z)⩵⊥.
Lemma L1 x y z : (x∨(y∨z))∧¬((x∨y)∨z) ⩵ ⊥.
Lemma L2 x y z : (x∧(y∧z))∨¬((x∧y)∧z) ⩵ ⊤.
Lemma Ass1 x y z : x∨(y∨z)⩵(x∨y)∨z.
Lemma Ass2 x y z : x∧(y∧z)⩵(x∧y)∧z.
Lemma Idm1 x : x ∨ x ⩵ x.
Lemma Bnd1 x : x ∨ ⊤ ⩵ ⊤.
Lemma Abs1 x y : x ∨ (x ∧ y) ⩵ x.
Lemma UId2 o : (∀ x, x ∧ o ⩵ x) → o ⩵ ⊤.
Lemma Idm2 x : x ∧ x ⩵ x.
Lemma Bnd2 x : x ∧ ⊥ ⩵ ⊥.
Lemma Abs2 x y : x ∧ (x ∨ y) ⩵ x.
Lemma UNg x x' : x ∨ x' ⩵ ⊤ → x ∧ x' ⩵ ⊥ → x' ⩵ ¬ x.
Lemma DNg x : ¬(¬ x) ⩵ x.
Lemma A1 x y : x ∨ (¬ x ∨ y) ⩵ ⊤.
Lemma A2 x y : x ∧ (¬ x ∧ y) ⩵ ⊥.
Lemma B1 x y : (x ∨ y)∨(¬x∧¬y)⩵⊤.
Lemma B2 x y : (x ∧ y)∧(¬x∨¬y)⩵⊥.
Lemma C1 x y : (x ∨ y)∧ (¬x∧¬y)⩵⊥.
Lemma C2 x y : (x ∧ y)∨ (¬x∨¬y)⩵⊤.
Lemma DMg1 x y : ¬ (x∨y) ⩵ ¬ x ∧ ¬ y.
Lemma DMg2 x y : ¬ (x∧y) ⩵ ¬ x ∨ ¬ y.
Lemma D1 x y z : (x∨(y∨z))∨¬x⩵⊤.
Lemma D2 x y z : (x∧(y∧z))∧¬x⩵⊥.
Lemma E1 x y z : y∧(x∨(y∨z))⩵ y.
Lemma E2 x y z : y∨(x∧(y∧z))⩵ y.
Lemma F1 x y z : (x∨(y∨z))∨¬y ⩵ ⊤.
Lemma F2 x y z : (x∧(y∧z))∧¬y ⩵ ⊥.
Lemma G1 x y z : (x ∨(y∨z))∨¬z⩵⊤.
Lemma G2 x y z : (x ∧(y∧z))∧¬z⩵⊥.
Lemma H1 x y z : ¬ ((x∨y)∨z)∧x⩵⊥.
Lemma H2 x y z : ¬ ((x∧y)∧z)∨x⩵⊤.
Lemma I1 x y z : ¬ ((x∨y)∨z)∧y⩵⊥.
Lemma I2 x y z : ¬ ((x∧y)∧z)∨y⩵⊤.
Lemma J1 x y z : ¬((x∨y)∨z)∧z⩵⊥.
Lemma J2 x y z : ¬((x∧y)∧z)∨z⩵⊤.
Lemma K1 x y z : (x∨(y∨z))∨¬((x∨y)∨z)⩵⊤.
Lemma K2 x y z : (x∧(y∧z))∧¬((x∧y)∧z)⩵⊥.
Lemma L1 x y z : (x∨(y∨z))∧¬((x∨y)∨z) ⩵ ⊥.
Lemma L2 x y z : (x∧(y∧z))∨¬((x∧y)∧z) ⩵ ⊤.
Lemma Ass1 x y z : x∨(y∨z)⩵(x∨y)∨z.
Lemma Ass2 x y z : x∧(y∧z)⩵(x∧y)∧z.
Global Instance BooleanAlgebra_Join_Lattice : @Lattice A eqA conj disj.
Global Instance BooleanAlgebra_Join_Semilattice : Semilattice A eqA disj.
Global Instance BooleanAlgebra_Meet_Semilattice : Semilattice A eqA conj.
Global Instance BooleanAlgebra_Meet_Monoid : @Monoid A eqA conj top.
Global Instance BooleanAlgebra_Join_Monoid : @Monoid A eqA disj bot.
Global Instance BooleanAlgebra_Semiring : SemiRing A eqA conj disj top bot.
End booleanAlgebra.
Global Instance BooleanAlgebra_Join_Semilattice : Semilattice A eqA disj.
Global Instance BooleanAlgebra_Meet_Semilattice : Semilattice A eqA conj.
Global Instance BooleanAlgebra_Meet_Monoid : @Monoid A eqA conj top.
Global Instance BooleanAlgebra_Join_Monoid : @Monoid A eqA disj bot.
Global Instance BooleanAlgebra_Semiring : SemiRing A eqA conj disj top bot.
End booleanAlgebra.
Section joinSemiLattice.
Context {A : Type} {eqA: relation A} {leqA : relation A}.
Context {equivA : @Equivalence A eqA} {preA : @PreOrder A leqA}
{partialA : @PartialOrder A eqA equivA leqA preA}.
Infix " ≦ " := leqA (at level 80).
Infix " ⩵ " := eqA (at level 80).
Context {j : Join A} {semLatA: Semilattice A eqA join}.
Context {proper_join: Proper (eqA ==> eqA ==> eqA) join}.
Lemma refactor e f g h : (e ∪ f) ∪ (g ∪ h) ⩵ (e ∪ g) ∪ (f ∪ h).
Context {joA : JoinOrder A eqA leqA join}.
Global Instance proper_join_inf : Proper (leqA ==> leqA ==> leqA) join.
Lemma inf_cup_left a b : a ≦ a ∪ b.
Lemma inf_cup_right a b : b ≦ a ∪ b.
Lemma inf_join_inf a b c : a ≦ c → b ≦ c → a ∪ b ≦ c.
Context {z : Zero A} {u : @Unit A eqA join zero}.
Lemma zero_minimal x : zero ≦ x.
End joinSemiLattice.
Context {A : Type} {eqA: relation A} {leqA : relation A}.
Context {equivA : @Equivalence A eqA} {preA : @PreOrder A leqA}
{partialA : @PartialOrder A eqA equivA leqA preA}.
Infix " ≦ " := leqA (at level 80).
Infix " ⩵ " := eqA (at level 80).
Context {j : Join A} {semLatA: Semilattice A eqA join}.
Context {proper_join: Proper (eqA ==> eqA ==> eqA) join}.
Lemma refactor e f g h : (e ∪ f) ∪ (g ∪ h) ⩵ (e ∪ g) ∪ (f ∪ h).
Context {joA : JoinOrder A eqA leqA join}.
Global Instance proper_join_inf : Proper (leqA ==> leqA ==> leqA) join.
Lemma inf_cup_left a b : a ≦ a ∪ b.
Lemma inf_cup_right a b : b ≦ a ∪ b.
Lemma inf_join_inf a b c : a ≦ c → b ≦ c → a ∪ b ≦ c.
Context {z : Zero A} {u : @Unit A eqA join zero}.
Lemma zero_minimal x : zero ≦ x.
End joinSemiLattice.
Section ka_facts.
Context {A : Type} {eqA: relation A} {leqA : relation A}.
Context {equivA : @Equivalence A eqA} {preA : @PreOrder A leqA}
{partialA : @PartialOrder A eqA equivA leqA preA}.
Infix " ≦ " := leqA (at level 80).
Infix " ⩵ " := eqA (at level 80).
Context {j: Join A}{p: Product A}{z: Zero A}{u:Un A}{s:Star A}.
Context {ka: KleeneAlgebra A eqA leqA}.
Global Instance proper_join_eq : Proper (eqA ==> eqA ==> eqA) join.
Global Instance proper_prod_inf : Proper (leqA ==> leqA ==> leqA) prod.
Global Instance join_semilattice : Semilattice A eqA join.
Lemma ka_star_unfold_eq a : a⋆ ⩵ 𝟭 ∪ a · a ⋆.
Lemma ka_star_dup a : a ⋆ · a ⋆ ⩵ a ⋆.
Lemma one_inf_star e : 𝟭 ≦ e⋆.
Lemma star_incr e : e ≦ e⋆.
Global Instance proper_star_inf : Proper (leqA ==> leqA) star.
Lemma ka_star_star a : a⋆ ⩵ (a ⋆)⋆.
Lemma ka_star_unfold_right a : 𝟭 ∪ a⋆ · a ≦ a⋆.
Lemma star_join e f : (e ∪ f)⋆ ⩵ e ⋆ ∪ f⋆·(e·f⋆)⋆.
Lemma un_star : un⋆ ⩵ un.
Lemma star_switch_side e : e⋆·e ⩵ e· e⋆.
Definition Σ l := fold_right (fun e f ⇒ join e f) zero l.
Lemma Σ_distr_l e L : e · Σ L ⩵ Σ (map (prod e) L).
Lemma Σ_distr_r e L : Σ L · e ⩵ Σ (map (fun f ⇒ f · e) L).
Lemma Σ_app L M : Σ L ∪ Σ M ⩵ Σ (L++M).
Lemma Σ_incl L M : L ⊆ M → Σ L ≦ Σ M.
Global Instance Σ_equivalent : Proper (@equivalent _ ==> eqA) Σ.
Lemma Σ_bigger e L : e ∈ L → e ≦ Σ L.
Lemma Σ_bounded e L : (∀ f, f ∈ L → f ≦ e) ↔ Σ L ≦ e.
Lemma ka_star_mid_split e : e⋆·e·e⋆ ≦ e⋆.
Lemma ka_zero_star : 𝟬 ⋆ ⩵ 𝟭.
End ka_facts.
Context {A : Type} {eqA: relation A} {leqA : relation A}.
Context {equivA : @Equivalence A eqA} {preA : @PreOrder A leqA}
{partialA : @PartialOrder A eqA equivA leqA preA}.
Infix " ≦ " := leqA (at level 80).
Infix " ⩵ " := eqA (at level 80).
Context {j: Join A}{p: Product A}{z: Zero A}{u:Un A}{s:Star A}.
Context {ka: KleeneAlgebra A eqA leqA}.
Global Instance proper_join_eq : Proper (eqA ==> eqA ==> eqA) join.
Global Instance proper_prod_inf : Proper (leqA ==> leqA ==> leqA) prod.
Global Instance join_semilattice : Semilattice A eqA join.
Lemma ka_star_unfold_eq a : a⋆ ⩵ 𝟭 ∪ a · a ⋆.
Lemma ka_star_dup a : a ⋆ · a ⋆ ⩵ a ⋆.
Lemma one_inf_star e : 𝟭 ≦ e⋆.
Lemma star_incr e : e ≦ e⋆.
Global Instance proper_star_inf : Proper (leqA ==> leqA) star.
Lemma ka_star_star a : a⋆ ⩵ (a ⋆)⋆.
Lemma ka_star_unfold_right a : 𝟭 ∪ a⋆ · a ≦ a⋆.
Lemma star_join e f : (e ∪ f)⋆ ⩵ e ⋆ ∪ f⋆·(e·f⋆)⋆.
Lemma un_star : un⋆ ⩵ un.
Lemma star_switch_side e : e⋆·e ⩵ e· e⋆.
Definition Σ l := fold_right (fun e f ⇒ join e f) zero l.
Lemma Σ_distr_l e L : e · Σ L ⩵ Σ (map (prod e) L).
Lemma Σ_distr_r e L : Σ L · e ⩵ Σ (map (fun f ⇒ f · e) L).
Lemma Σ_app L M : Σ L ∪ Σ M ⩵ Σ (L++M).
Lemma Σ_incl L M : L ⊆ M → Σ L ≦ Σ M.
Global Instance Σ_equivalent : Proper (@equivalent _ ==> eqA) Σ.
Lemma Σ_bigger e L : e ∈ L → e ≦ Σ L.
Lemma Σ_bounded e L : (∀ f, f ∈ L → f ≦ e) ↔ Σ L ≦ e.
Lemma ka_star_mid_split e : e⋆·e·e⋆ ≦ e⋆.
Lemma ka_zero_star : 𝟬 ⋆ ⩵ 𝟭.
End ka_facts.