Yury G. Kudryashov (Jul 30 2020 at 05:39):
I want to add two typeclasses:
@[to_additive] class weakly_ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α := (mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b) class canonically_weakly_ordered_add_monoid (α : Type*) extends weakly_ordered_add_comm_monoid α, order_bot α := (le_iff_exists_add : ∀a b:α, a ≤ b ↔ ∃c, b = a + c)
The main use cases for the second class are
measure α and
α → enreal. The axiom
(lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)
doesn't work in these cases. E.g., for
bool → ennreal the counterexample is given by
a = λ x, cond x 0 ∞,
b = λ x, cond x 0 1,
c = λ x, cond x 1 0,
a + b = λ x, cond x 0 ∞,
a + c = λ x, cond x 1 ∞.
What do you think about this? Do you have better names for these classes?
Johan Commelin (Jul 30 2020 at 05:46):
I think those are useful. I'm just starting to wonder if we should transition to mixins in the order-meets-algebra part of the library...
Last updated: May 09 2021 at 10:11 UTC