Non-expansive commutative monoids and their morphisms.

Monoids for Big Operators

• Monoid contains the laws and requires an OFE structure.
• Uses explicit op parameters to support multiple monoids on the same type.

class Iris.Algebra.MonoidOps {M : Type u} [OFE M] (op : M → M → M) (unit : outParam M) : Prop

A commutative monoid on an OFE, used for big operators. The operation must be non-expansive, associative, commutative, and have a left identity.

• op_ne : OFE.NonExpansive₂ op

  The operation is non-expansive in both arguments

• op_assoc {a b c : M} : op (op a b) c = op a (op b c)

  Associativity

• op_comm {a b : M} : op a b = op b a

  Commutativity

• op_left_id {a : M} : op unit a = a

  Left identity

theorem Iris.Algebra.MonoidOps.op_right_id {M : Type u} [OFE M] {unit : M} {op : M → M → M} {a : M} [MonoidOps op unit] : op a unit = a

Right identity follows from commutativity and left identity.

theorem Iris.Algebra.MonoidOps.op_op_op_comm {M : Type u} [OFE M] {unit : M} {op : M → M → M} [MonoidOps op unit] {a b c d : M} : op (op a b) (op c d) = op (op a c) (op b d)

Rearrange (a * b) * (c * d) to (a * c) * (b * d).

theorem Iris.Algebra.MonoidOps.op_left_comm {M : Type u} [OFE M] {unit : M} {op : M → M → M} [MonoidOps op unit] {a b c : M} : op a (op b c) = op b (op a c)

Swap inner elements: a * (b * c) to b * (a * c).

theorem Iris.Algebra.MonoidOps.op_dist {M : Type u} [OFE M] {unit : M} {op : M → M → M} {n : Nat} {a a' b b' : M} [MonoidOps op unit] (ha : OFE.Dist n a a') (hb : OFE.Dist n b b') : OFE.Dist n (op a b) (op a' b')

Non-expansiveness for dist.

Monoid Homomorphisms

class Iris.Algebra.WeakMonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂) [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂] (R : M₂ → M₂ → Prop) (f : M₁ → M₂) : Prop

A weak monoid homomorphism preserves the operation but not necessarily the unit.

• rel_refl {a : M₂} : R a a

  The relation is reflexive

• rel_trans {a b c : M₂} : R a b → R b c → R a c

  The relation is transitive

• op_proper {a a' b b' : M₂} : R a a' → R b b' → R (op₂ a b) (op₂ a' b')

  The operation is proper with respect to R

• map_ne : OFE.NonExpansive f

  The function is non-expansive

• map_op {x y : M₁} : R (f (op₁ x y)) (op₂ (f x) (f y))

  The homomorphism property

class Iris.Algebra.MonoidHomomorphism {M₁ : Type u} {M₂ : Type v} [OFE M₁] [OFE M₂] (op₁ : M₁ → M₁ → M₁) (op₂ : M₂ → M₂ → M₂) (unit₁ : M₁) (unit₂ : M₂) [MonoidOps op₁ unit₁] [MonoidOps op₂ unit₂] (R : M₂ → M₂ → Prop) (f : M₁ → M₂) extends Iris.Algebra.WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f : Prop

A monoid homomorphism preserves both the operation and the unit.

• rel_refl {a : M₂} : R a a
• rel_trans {a b c : M₂} : R a b → R b c → R a c
• op_proper {a a' b b' : M₂} : R a a' → R b b' → R (op₂ a b) (op₂ a' b')
• map_ne : OFE.NonExpansive f
• map_op {x y : M₁} : R (f (op₁ x y)) (op₂ (f x) (f y))
• map_unit : R (f unit₁) unit₂

  The unit is preserved