Commit 2021-05-15 16:28 172195bb

View on Github →

feat(algebra/{ordered_monoid, ordered_monoid_lemmas}): split the ordered_[...] typeclasses (#7371) This PR tries to split the ordering assumptions from the algebraic assumptions on the operations in the ordered_[...] hierarchy. The strategy is to introduce two more flexible typeclasses, covariant_class and contravariant_class.

  • covariant_class models the implication a ≤ b → c * a ≤ c * b (multiplication is monotone),
  • contravariant_class models the implication a * b < a * c → b < c. Since co(ntra)variant_class takes as input the operation (typically (+) or (*)) and the order relation (typically (≤) or (<)), these are the only two typeclasses that I have used. The general approach is to formulate the lemma that you are interested in and prove it, with the ordered_[...] typeclass of your liking. After that, you convert the single typeclass, say [ordered_cancel_monoid M], to three typeclasses, e.g. [partial_order M] [left_cancel_semigroup M] [covariant_class M M (function.swap (*)) (≤)] and have a go at seeing if the proof still works! Note that it is possible (or even expected) to combine several co(ntra)variant_class assumptions together. Indeed, the usual ordered typeclasses arise from assuming the pair [covariant_class M M (*) (≤)] [contravariant_class M M (*) (<)] on top of order/algebraic assumptions. A formal remark is that normally covariant_class uses the (≤)-relation, while contravariant_class uses the (<)-relation. This need not be the case in general, but seems to be the most common usage. In the opposite direction, the implication [semigroup α] [partial_order α] [contravariant_class α α (*) (≤)] => left_cancel_semigroup α holds (note the co*ntra* assumption and the (≤)-relation). Zulip:

Estimated changes

deleted theorem le_mul_iff_one_le_left'
deleted theorem le_mul_iff_one_le_right'
deleted theorem le_mul_of_le_mul_left
deleted theorem le_mul_of_le_mul_right
deleted theorem le_mul_of_le_of_one_le
deleted theorem le_mul_of_one_le_left'
deleted theorem le_mul_of_one_le_of_le
deleted theorem le_mul_of_one_le_right'
deleted theorem le_of_mul_le_mul_left'
deleted theorem le_of_mul_le_mul_right'
deleted theorem lt_mul_iff_one_lt_left'
deleted theorem lt_mul_iff_one_lt_right'
deleted theorem lt_mul_of_le_of_one_lt
deleted theorem lt_mul_of_lt_mul_left
deleted theorem lt_mul_of_lt_mul_right
deleted theorem lt_mul_of_lt_of_one_le'
deleted theorem lt_mul_of_lt_of_one_le
deleted theorem lt_mul_of_lt_of_one_lt'
deleted theorem lt_mul_of_lt_of_one_lt
deleted theorem lt_mul_of_one_le_of_lt'
deleted theorem lt_mul_of_one_le_of_lt
deleted theorem lt_mul_of_one_lt_left'
deleted theorem lt_mul_of_one_lt_of_le
deleted theorem lt_mul_of_one_lt_of_lt'
deleted theorem lt_mul_of_one_lt_of_lt
deleted theorem lt_mul_of_one_lt_right'
deleted theorem lt_of_mul_lt_mul_left'
deleted theorem lt_of_mul_lt_mul_right'
deleted theorem monotone.const_mul'
deleted theorem monotone.mul'
deleted theorem monotone.mul_const'
deleted theorem mul_eq_one_iff'
deleted theorem mul_le_iff_le_one_left'
deleted theorem mul_le_iff_le_one_right'
deleted theorem mul_le_mul'
deleted theorem mul_le_mul_iff_left
deleted theorem mul_le_mul_iff_right
deleted theorem mul_le_mul_left'
deleted theorem mul_le_mul_right'
deleted theorem mul_le_mul_three
deleted theorem mul_le_of_le_of_le_one'
deleted theorem mul_le_of_le_of_le_one
deleted theorem mul_le_of_le_one_left'
deleted theorem mul_le_of_le_one_of_le'
deleted theorem mul_le_of_le_one_of_le
deleted theorem mul_le_of_le_one_right'
deleted theorem mul_le_of_mul_le_left
deleted theorem mul_le_of_mul_le_right
deleted theorem mul_le_one'
deleted theorem mul_lt_iff_lt_one_left'
deleted theorem mul_lt_iff_lt_one_right'
deleted theorem mul_lt_mul'''
deleted theorem mul_lt_mul_iff_left
deleted theorem mul_lt_mul_iff_right
deleted theorem mul_lt_mul_left'
deleted theorem mul_lt_mul_of_le_of_lt
deleted theorem mul_lt_mul_of_lt_of_le
deleted theorem mul_lt_mul_right'
deleted theorem mul_lt_of_le_of_lt_one
deleted theorem mul_lt_of_le_one_of_lt'
deleted theorem mul_lt_of_le_one_of_lt
deleted theorem mul_lt_of_lt_of_le_one'
deleted theorem mul_lt_of_lt_of_le_one
deleted theorem mul_lt_of_lt_of_lt_one'
deleted theorem mul_lt_of_lt_of_lt_one
deleted theorem mul_lt_of_lt_one_of_le
deleted theorem mul_lt_of_lt_one_of_lt'
deleted theorem mul_lt_of_lt_one_of_lt
deleted theorem mul_lt_of_mul_lt_left
deleted theorem mul_lt_of_mul_lt_right
deleted theorem mul_lt_one'
deleted theorem mul_lt_one
deleted theorem one_le_mul
deleted theorem one_lt_mul'
deleted theorem one_lt_mul_of_le_of_lt'
deleted theorem one_lt_mul_of_lt_of_le'
deleted theorem pos_of_gt
modified theorem with_zero.mul_le_mul_left
modified theorem with_zero.zero_lt_coe
added def contravariant
added def covariant
added theorem le_mul_of_le_mul_left
added theorem le_mul_of_le_mul_right
added theorem le_mul_of_le_of_one_le
added theorem le_mul_of_one_le_left'
added theorem le_mul_of_one_le_of_le
added theorem le_of_mul_le_mul_left'
added theorem lt_mul_of_le_of_one_lt
added theorem lt_mul_of_lt_mul_left
added theorem lt_mul_of_lt_mul_right
added theorem lt_mul_of_lt_of_one_le
added theorem lt_mul_of_lt_of_one_lt
added theorem lt_mul_of_one_le_of_lt
added theorem lt_mul_of_one_lt_left'
added theorem lt_mul_of_one_lt_of_le
added theorem lt_mul_of_one_lt_of_lt
added theorem lt_of_mul_lt_mul_left'
added theorem monotone.const_mul'
added theorem monotone.mul'
added theorem monotone.mul_const'
added theorem mul_eq_one_iff'
added theorem mul_le_mul'
added theorem mul_le_mul_iff_left
added theorem mul_le_mul_iff_right
added theorem mul_le_mul_left'
added theorem mul_le_mul_right'
added theorem mul_le_mul_three
added theorem mul_le_of_le_of_le_one
added theorem mul_le_of_le_one_left'
added theorem mul_le_of_le_one_of_le
added theorem mul_le_of_mul_le_left
added theorem mul_le_of_mul_le_right
added theorem mul_le_one'
added theorem mul_lt_mul'''
added theorem mul_lt_mul_iff_left
added theorem mul_lt_mul_iff_right
added theorem mul_lt_mul_left'
added theorem mul_lt_mul_of_le_of_lt
added theorem mul_lt_mul_of_lt_of_le
added theorem mul_lt_mul_right'
added theorem mul_lt_of_le_of_lt_one
added theorem mul_lt_of_le_one_of_lt
added theorem mul_lt_of_lt_of_le_one
added theorem mul_lt_of_lt_of_lt_one
added theorem mul_lt_of_lt_one_of_le
added theorem mul_lt_of_lt_one_of_lt
added theorem mul_lt_of_mul_lt_left
added theorem mul_lt_of_mul_lt_right
added theorem mul_lt_one'
added theorem mul_lt_one
added theorem one_le_mul
added theorem one_lt_mul'