Qcert.Basic.Util.Monoid
Definition of monoids over collections, loosely based on ideas
from "Optimizing object queries using an effective
calculus. Leonidas Fegaras and David Maier. In ACM
Transactions on Database Systems (TODS) 25.4 (2000): 457-516."
Some of the type classes structure follow from:
"A Gentle Introduction to Type Classes and Relations in
Coq. Pierre Castéran and Matthieu Sozeau"
Definition associative {A} eqA `{equivA : Equivalence A eqA} (op : A→A→A)
:= ∀ x₁ x₂ x₃, op (op x₁ x₂) x₃ === op x₁ (op x₂ x₃).
Definition commutative {A} eqA `{equivA : Equivalence A eqA} (op : binary_operation A)
:= ∀ x₁ x₂, op x₁ x₂ === op x₂ x₁.
Definition idempotent {A} eqA `{equivA : Equivalence A eqA} (op : binary_operation A)
:= ∀ x, op x x === x.
Definition anti_idempotent {A} eqA `{equivA : Equivalence A eqA} (op : binary_operation A)
:= ∀ x, not (op x x === x).
Definition zero_left {A} eqA `{equivA : Equivalence A eqA} (op : binary_operation A) (z : A)
:= ∀ x, op z x === x.
Definition zero_right {A} eqA `{equivA : Equivalence A eqA} (op : binary_operation A) (z : A)
:= ∀ x, op x z === x.
Class Monoid (A:Type) (eqA:A→A→Prop) {equivB:Equivalence eqA}
:= {
merge: A → A → A;
z: A;
merge_morphism :> Proper (eqA ==> eqA ==> eqA) merge ;
z_morphism :> Proper (eqA) z;
merge_assoc: associative eqA merge;
z_left: zero_left eqA merge z;
z_right: zero_right eqA merge z
}.
Infix "⊕" := merge (at level 70). Infix "ζ" := z (at level 70).
A collection monoid.
A commutative monoid.
Class CMonoid {A:Type}
(eqA:A→A→Prop)
`{monoid:Monoid A eqA}
:= {
c_merge_comm: commutative eqA merge
}.
An idempotent monoid.
Class IMonoid {A:Type}
(eqA:A→A→Prop)
`{monoid:Monoid A eqA}
:= {
i_merge_idem: idempotent eqA merge
}.
An anti-idempotent monoid.
Class AIMonoid {A:Type}
(eqA:A→A→Prop)
`{monoid:Monoid A eqA}
:= {
ai_merge_anti_idem: anti_idempotent eqA merge
}.
A commutative & idempotent monoid.
Class CIMonoid {A:Type}
(eqA:A→A→Prop)
`{monoid:Monoid A eqA}
:= {
ci_merge_comm: commutative eqA merge;
ci_merge_idem: idempotent eqA merge
}.
A commutative & anti-idempotent monoid.