Unbundled algebra classes

These classes are part of an incomplete refactor described here on the github Wiki. However a subset of them are widely used in mathlib3, and it has been tricky to clean this up as this file was in core Lean 3.

By themselves, these classes are not good replacements for the Monoid / Group etc structures provided by mathlib, as they are not discoverable by simp unlike the current lemmas due to there being little to index on. The Wiki page linked above describes an algebraic normalizer, but it was never implemented in Lean 3.

Porting notes:

This file is ancient, and it would be good to replace it with a clean version that provides what mathlib4 actually needs.

I've omitted all the @[algebra] attributes, as they are not used elsewhere.

The section StrictWeakOrder has been omitted, but I've left the mathport output in place. Please delete if cleaning up.

I've commented out some classes which we think are completely unused in mathlib.

I've added many of the declarations to nolints.json. If you clean up this file, please add documentation to classes that we are keeping.

Mario made the following analysis of uses in mathlib3:

• is_symm_op: unused except for some instances
• is_commutative: used a fair amount via some theorems about folds (also assuming is_associative)
• is_associative: ditto, also used in noncomm_fold
• is_left_id, is_right_id: unused except in the mathlib class is_unital and in mono (which looks like it could use is_unital)
• is_left_null, is_right_null: unused
• is_left_cancel, is_right_cancel: unused except for instances
• is_idempotent: this one is actually used to prove things not directly about is_idempotent
• is_left_distrib, is_right_distrib, is_left_inv, is_right_inv, is_cond_left_inv, is_cond_right_inv: unused
• is_distinct: unused (although we reinvented this one as nontrivial)
• is_irrefl, is_refl, is_symm, is_trans: significant usage
• is_asymm, is_antisymm, is_total, is_strict_order: a lot of uses but all in order theory and it's unclear how much could not be transferred to another typeclass
• is_preorder: unused except for instances (except antisymmetrization, maybe it could be transferred)
• is_total_preorder, is_partial_order: unused except for instances
• is_linear_order: unused except for instances
• is_equiv: unused except for instances (most uses can use equivalence instead)
• is_per: unused
• is_incomp_trans: unused
• is_strict_weak_order: significant usage (most of it on rbmap, could be transferred)
• is_trichotomous: some usage
• is_strict_total_order: looks like the only usage is in rbmap again

class IsSymmOp (α : Type u) (β : Type v) (op : α → α → β) : Prop

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

class IsCommutative (α : Type u) (op : α → α → α) : Prop

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

A commutative binary operation.

instance instIsCommutative {α : Type u_1} {op : α → α → α} [IsCommutative α op] : Lean.IsCommutative op

Equations

• instIsCommutative = { comm := (_ : ∀ (a b : α), op a b = op b a) }

instance isSymmOp_of_isCommutative (α : Type u) (op : α → α → α) [IsCommutative α op] : IsSymmOp α α op

Equations

• isSymmOp_of_isCommutative = isSymmOp_of_isCommutative.proof_1

class IsAssociative (α : Type u) (op : α → α → α) : Prop

• assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)

An associative binary operation.

instance instIsAssociative {α : Type u_1} {op : α → α → α} [IsAssociative α op] : Lean.IsAssociative op

Equations

• instIsAssociative = { assoc := (_ : ∀ (a b c : α), op (op a b) c = op a (op b c)) }

class IsLeftId (α : Type u) (op : α → α → α) (o : outParam α) : Prop

• left_id : ∀ (a : α), op o a = a

A binary operation with a left identity.

class IsRightId (α : Type u) (op : α → α → α) (o : outParam α) : Prop

• right_id : ∀ (a : α), op a o = a

A binary operation with a right identity.

instance instIsNeutral {α : Type u_1} {o : α} {op : α → α → α} [IsLeftId α op o] [IsRightId α op o] : Lean.IsNeutral op o

Equations

• instIsNeutral = { left_neutral := (_ : ∀ (a : α), op o a = a), right_neutral := (_ : ∀ (a : α), op a o = a) }

class IsLeftCancel (α : Type u) (op : α → α → α) : Prop

• left_cancel : ∀ (a b c : α), op a b = op a c → b = c

class IsRightCancel (α : Type u) (op : α → α → α) : Prop

• right_cancel : ∀ (a b c : α), op a b = op c b → a = c

class IsIdempotent (α : Type u) (op : α → α → α) : Prop

• idempotent : ∀ (a : α), op a a = a

instance instIsIdempotent {α : Type u_1} {op : α → α → α} [IsIdempotent α op] : Lean.IsIdempotent op

Equations

• instIsIdempotent = { idempotent := (_ : ∀ (a : α), op a a = a) }

class IsIrrefl (α : Type u) (r : α → α → Prop) : Prop

• irrefl : ∀ (a : α), ¬r a a

IsIrrefl X r means the binary relation r on X is irreflexive (that is, r x x never holds).

class IsRefl (α : Type u) (r : α → α → Prop) : Prop

• refl : ∀ (a : α), r a a

IsRefl X r means the binary relation r on X is reflexive.

class IsSymm (α : Type u) (r : α → α → Prop) : Prop

• symm : ∀ (a b : α), r a b → r b a

IsSymm X r means the binary relation r on X is symmetric.

instance isSymmOp_of_isSymm (α : Type u) (r : α → α → Prop) [IsSymm α r] : IsSymmOp α Prop r

The opposite of a symmetric relation is symmetric.

Equations

• isSymmOp_of_isSymm = isSymmOp_of_isSymm.proof_1

class IsAsymm (α : Type u) (r : α → α → Prop) : Prop

• asymm : ∀ (a b : α), r a b → ¬r b a

IsAsymm X r means that the binary relation r on X is asymmetric, that is, r a b → ¬ r b a.

class IsAntisymm (α : Type u) (r : α → α → Prop) : Prop

• antisymm : ∀ (a b : α), r a b → r b a → a = b

IsAntisymm X r means the binary relation r on X is antisymmetric.

class IsTrans (α : Type u) (r : α → α → Prop) : Prop

• trans : ∀ (a b c : α), r a b → r b c → r a c

IsTrans X r means the binary relation r on X is transitive.

instance instTrans {α : Type u} {r : α → α → Prop} [IsTrans α r] : Trans r r r

Equations

• instTrans = { trans := fun {a b c} => IsTrans.trans a b c }

instance instIsTrans {α : Type u} {r : α → α → Prop} [Trans r r r] : IsTrans α r

Equations

• @instIsTrans = @instIsTrans.proof_1

class IsTotal (α : Type u) (r : α → α → Prop) : Prop

• total : ∀ (a b : α), r a b ∨ r b a

IsTotal X r means that the binary relation r on X is total, that is, that for any x y : X we have r x y or r y x.

class IsPreorder (α : Type u) (r : α → α → Prop) extends IsRefl , IsTrans : Prop

IsPreorder X r means that the binary relation r on X is a pre-order, that is, reflexive and transitive.

class IsTotalPreorder (α : Type u) (r : α → α → Prop) extends IsTrans , IsTotal : Prop

IsTotalPreorder X r means that the binary relation r on X is total and a preorder.

instance isTotalPreorder_isPreorder (α : Type u) (r : α → α → Prop) [s : IsTotalPreorder α r] : IsPreorder α r

Every total pre-order is a pre-order.

Equations

• isTotalPreorder_isPreorder = isTotalPreorder_isPreorder.proof_1

class IsPartialOrder (α : Type u) (r : α → α → Prop) extends IsPreorder , IsAntisymm : Prop

IsPartialOrder X r means that the binary relation r on X is a partial order, that is, IsPreorder X r and IsAntisymm X r.

class IsLinearOrder (α : Type u) (r : α → α → Prop) extends IsPartialOrder , IsTotal : Prop

IsLinearOrder X r means that the binary relation r on X is a linear order, that is, IsPartialOrder X r and IsTotal X r.

class IsEquiv (α : Type u) (r : α → α → Prop) extends IsPreorder , IsSymm : Prop

IsEquiv X r means that the binary relation r on X is an equivalence relation, that is, IsPreorder X r and IsSymm X r.

class IsStrictOrder (α : Type u) (r : α → α → Prop) extends IsIrrefl , IsTrans : Prop

IsStrictOrder X r means that the binary relation r on X is a strict order, that is, IsIrrefl X r and IsTrans X r.

class IsIncompTrans (α : Type u) (lt : α → α → Prop) : Prop

• incomp_trans : ∀ (a b c : α), ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a

IsIncompTrans X lt means that for lt a binary relation on X, the incomparable relation fun a b => ¬ lt a b ∧ ¬ lt b a is transitive.

class IsStrictWeakOrder (α : Type u) (lt : α → α → Prop) extends IsStrictOrder , IsIncompTrans : Prop

IsStrictWeakOrder X lt means that the binary relation lt on X is a strict weak order, that is, IsStrictOrder X lt and IsIncompTrans X lt.

class IsTrichotomous (α : Type u) (lt : α → α → Prop) : Prop

• trichotomous : ∀ (a b : α), lt a b ∨ a = b ∨ lt b a

IsTrichotomous X lt means that the binary relation lt on X is trichotomous, that is, either lt a b or a = b or lt b a for any a and b.

class IsStrictTotalOrder (α : Type u) (lt : α → α → Prop) extends IsTrichotomous , IsStrictOrder : Prop

IsStrictTotalOrder X lt means that the binary relation lt on X is a strict total order, that is, IsTrichotomous X lt and IsStrictOrder X lt.

instance eq_isEquiv (α : Type u) : IsEquiv α fun x x_1 => x = x_1

Equality is an equivalence relation.

Equations

• eq_isEquiv = eq_isEquiv.proof_1

theorem irrefl {α : Type u} {r : α → α → Prop} [IsIrrefl α r] (a : α) : ¬r a a

theorem refl {α : Type u} {r : α → α → Prop} [IsRefl α r] (a : α) : r a a

theorem trans {α : Type u} {r : α → α → Prop} [IsTrans α r] {a : α} {b : α} {c : α} : r a b → r b c → r a c

theorem symm {α : Type u} {r : α → α → Prop} [IsSymm α r] {a : α} {b : α} : r a b → r b a

theorem antisymm {α : Type u} {r : α → α → Prop} [IsAntisymm α r] {a : α} {b : α} : r a b → r b a → a = b

theorem asymm {α : Type u} {r : α → α → Prop} [IsAsymm α r] {a : α} {b : α} : r a b → ¬r b a

theorem trichotomous {α : Type u} {r : α → α → Prop} [IsTrichotomous α r] (a : α) (b : α) : r a b ∨ a = b ∨ r b a

theorem incomp_trans {α : Type u} {r : α → α → Prop} [IsIncompTrans α r] {a : α} {b : α} {c : α} : ¬r a b ∧ ¬r b a → ¬r b c ∧ ¬r c b → ¬r a c ∧ ¬r c a

instance isAsymm_of_isTrans_of_isIrrefl {α : Type u} {r : α → α → Prop} [IsTrans α r] [IsIrrefl α r] : IsAsymm α r

Equations

• @isAsymm_of_isTrans_of_isIrrefl = @isAsymm_of_isTrans_of_isIrrefl.proof_1

@[elab_without_expected_type]

theorem irrefl_of {α : Type u} (r : α → α → Prop) [IsIrrefl α r] (a : α) : ¬r a a

@[elab_without_expected_type]

theorem refl_of {α : Type u} (r : α → α → Prop) [IsRefl α r] (a : α) : r a a

@[elab_without_expected_type]

theorem trans_of {α : Type u} (r : α → α → Prop) [IsTrans α r] {a : α} {b : α} {c : α} : r a b → r b c → r a c

@[elab_without_expected_type]

theorem symm_of {α : Type u} (r : α → α → Prop) [IsSymm α r] {a : α} {b : α} : r a b → r b a

@[elab_without_expected_type]

theorem asymm_of {α : Type u} (r : α → α → Prop) [IsAsymm α r] {a : α} {b : α} : r a b → ¬r b a

@[elab_without_expected_type]

theorem total_of {α : Type u} (r : α → α → Prop) [IsTotal α r] (a : α) (b : α) : r a b ∨ r b a

@[elab_without_expected_type]

theorem trichotomous_of {α : Type u} (r : α → α → Prop) [IsTrichotomous α r] (a : α) (b : α) : r a b ∨ a = b ∨ r b a

@[elab_without_expected_type]

theorem incomp_trans_of {α : Type u} (r : α → α → Prop) [IsIncompTrans α r] {a : α} {b : α} {c : α} : ¬r a b ∧ ¬r b a → ¬r b c ∧ ¬r c b → ¬r a c ∧ ¬r c a

def StrictWeakOrder.Equiv {α : Type u} {r : α → α → Prop} (a : α) (b : α) : Prop

Equations

• StrictWeakOrder.Equiv a b = (¬r a b ∧ ¬r b a)

theorem StrictWeakOrder.erefl {α : Type u} {r : α → α → Prop} [IsStrictWeakOrder α r] (a : α) : StrictWeakOrder.Equiv a a

theorem StrictWeakOrder.esymm {α : Type u} {r : α → α → Prop} {a : α} {b : α} : StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b a

theorem StrictWeakOrder.etrans {α : Type u} {r : α → α → Prop} [IsStrictWeakOrder α r] {a : α} {b : α} {c : α} : StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b c → StrictWeakOrder.Equiv a c

theorem StrictWeakOrder.not_lt_of_equiv {α : Type u} {r : α → α → Prop} {a : α} {b : α} : StrictWeakOrder.Equiv a b → ¬r a b

theorem StrictWeakOrder.not_lt_of_equiv' {α : Type u} {r : α → α → Prop} {a : α} {b : α} : StrictWeakOrder.Equiv a b → ¬r b a

instance StrictWeakOrder.isEquiv {α : Type u} {r : α → α → Prop} [IsStrictWeakOrder α r] : IsEquiv α StrictWeakOrder.Equiv

Equations

• @StrictWeakOrder.isEquiv = @StrictWeakOrder.isEquiv.proof_1

def StrictWeakOrder.«term_≈[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem isStrictWeakOrder_of_isTotalPreorder {α : Type u} {le : α → α → Prop} {lt : α → α → Prop} [DecidableRel le] [IsTotalPreorder α le] (h : ∀ (a b : α), lt a b ↔ ¬le b a) : IsStrictWeakOrder α lt

theorem lt_of_lt_of_incomp {α : Type u} {lt : α → α → Prop} [IsStrictWeakOrder α lt] [DecidableRel lt] {a : α} {b : α} {c : α} : lt a b → ¬lt b c ∧ ¬lt c b → lt a c

theorem lt_of_incomp_of_lt {α : Type u} {lt : α → α → Prop} [IsStrictWeakOrder α lt] [DecidableRel lt] {a : α} {b : α} {c : α} : ¬lt a b ∧ ¬lt b a → lt b c → lt a c

theorem eq_of_incomp {α : Type u} {lt : α → α → Prop} [IsTrichotomous α lt] {a : α} {b : α} : ¬lt a b ∧ ¬lt b a → a = b

theorem eq_of_eqv_lt {α : Type u} {lt : α → α → Prop} [IsTrichotomous α lt] {a : α} {b : α} : StrictWeakOrder.Equiv a b → a = b

theorem incomp_iff_eq {α : Type u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a : α) (b : α) : ¬lt a b ∧ ¬lt b a ↔ a = b

theorem eqv_lt_iff_eq {α : Type u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a : α) (b : α) : StrictWeakOrder.Equiv a b ↔ a = b

theorem not_lt_of_lt {α : Type u} {lt : α → α → Prop} [IsStrictOrder α lt] {a : α} {b : α} : lt a b → ¬lt b a