Typeclasses for commuting heterogeneous operations

The three classes in this file are for two-argument functions where one input is of type α, the output is of type β and the other input is of type α or β. They express the property that permuting arguments of type α does not change the result.

Main definitions

• IsSymmOp: for op : α → α → β, op a b = op b a.
• LeftCommutative: for op : α → β → β, op a₁ (op a₂ b) = op a₂ (op a₁ b).
• RightCommutative: for op : β → α → β, op (op b a₁) a₂ = op (op b a₂) a₁.

class IsSymmOp {α : Sort u} {β : Sort v} (op : α → α → β) : Prop

IsSymmOp op where op : α → α → β says that op is a symmetric operation, i.e. op a b = op b a. It is the natural generalisation of Std.Commutative (β = α) and IsSymm (β = Prop).

• symm_op : ∀ (a b : α), op a b = op b a

  A symmetric operation satisfies op a b = op b a.

class LeftCommutative {α : Sort u} {β : Sort v} (op : α → β → β) : Prop

LeftCommutative op where op : α → β → β says that op is a left-commutative operation, i.e. op a₁ (op a₂ b) = op a₂ (op a₁ b).

• left_comm : ∀ (a₁ a₂ : α) (b : β), op a₁ (op a₂ b) = op a₂ (op a₁ b)

  A left-commutative operation satisfies op a₁ (op a₂ b) = op a₂ (op a₁ b).

class RightCommutative {α : Sort u} {β : Sort v} (op : β → α → β) : Prop

RightCommutative op where op : β → α → β says that op is a right-commutative operation, i.e. op (op b a₁) a₂ = op (op b a₂) a₁.

• right_comm : ∀ (b : β) (a₁ a₂ : α), op (op b a₁) a₂ = op (op b a₂) a₁

  A right-commutative operation satisfies op (op b a₁) a₂ = op (op b a₂) a₁.

theorem isSymmOp_of_isCommutative (α : Sort u) (op : α → α → α) [Std.Commutative op] : IsSymmOp op

theorem IsSymmOp.flip_eq {α : Sort u} {β : Sort v} (op : α → α → β) [IsSymmOp op] : flip op = op

theorem instRightCommutativeOfLeftCommutative {α : Sort u} {β : Sort v} {f : α → β → β} [h : LeftCommutative f] : RightCommutative fun (x : β) (y : α) => f y x

theorem instLeftCommutativeOfRightCommutative {α : Sort u} {β : Sort v} {f : β → α → β} [h : RightCommutative f] : LeftCommutative fun (x : α) (y : β) => f y x

theorem instLeftCommutativeOfCommutativeOfAssociative {α : Sort u} {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : LeftCommutative f

theorem instRightCommutativeOfCommutativeOfAssociative {α : Sort u} {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : RightCommutative f