New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: Move OrderDual
action instances to their own file
#8840
Conversation
Also add a few missing ones.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please list the new instances in the PR description, since they're not obvious from the diff.
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Also add a few missing ones: * `OrderDual.instSMulWithZero` * `OrderDual.instMulAction` * `OrderDual.instMulActionWithZero` * `OrderDual.instDistribMulAction` In every case, we prime the originally unprimed/unnamed version.
Pull request successfully merged into master. Build succeeded: |
OrderDual
action instances to their own fileOrderDual
action instances to their own file
This PR introduces eight typeclasses for monotonicity of left/right scalar multiplication by nonnegative elements: * `PosSMulMono`: If `a ≥ 0`, then `b₁ ≤ b₂` implies `a • b₁ ≤ a • b₂`. * `PosSMulStrictMono`: If `a > 0`, then `b₁ < b₂` implies `a • b₁ < a • b₂`. * `PosSMulReflectLT`: If `a ≥ 0`, then `a • b₁ < a • b₂` implies `b₁ < b₂`. * `PosSMulReflectLE`: If `a > 0`, then `a • b₁ ≤ a • b₂` implies `b₁ ≤ b₂`. * `SMulPosMono`: If `b ≥ 0`, then `a₁ ≤ a₂` implies `a₁ • b ≤ a₂ • b`. * `SMulPosStrictMono`: If `b > 0`, then `a₁ < a₂` implies `a₁ • b < a₂ • b`. * `SMulPosReflectLT`: If `b ≥ 0`, then `a₁ • b < a₂ • b` implies `a₁ < a₂`. * `SMulPosReflectLE`: If `b > 0`, then `a₁ • b ≤ a₂ • b` implies `a₁ ≤ a₂`. The design is heavily inspired to the corresponding one for multiplication (see `Algebra.Order.Ring.Lemmas`). Note however the following differences: * The new typeclasses are custom typeclasses instead of abbreviations for the correct `CovariantClass`/`ContravariantClass` invokations. This has the following benefits: * They get displayed as classes in the docs. In particular, one can see their list of instances, instead of their instances being invariably dumped to the `CovariantClass`/`ContravariantClass` list. * They don't pollute other typeclass searches. Having many abbreviations of the same typeclass for different purposes always felt like a performance issue to me (more instances with the same key, for no added benefit), and indeed a previous version of this PR hit timeouts due to the higher number of `CovariantClass`/`ContravariantClass` instances. * `SMulPosReflectLT`/`SMulPosReflectLE` did not fit in the framework since they relate `≤` on two different types. So I would have had to generalise `CovariantClass`/`ContravariantClass` to three types and two relations. * Very minor, but the constructors let you work with `a : α`, `h : 0 ≤ a` instead of `a : {a : α // 0 ≤ a}`. This actually makes some instances surprisingly cleaner to prove. * The `CovariantClass`/`ContravariantClass` framework was only used to automate very simple logic anyway. It was easily copied over. * We replace undocumented lemmas stating the equivalence of the four typeclasses mentioning nonnegativity with their positivity version by motivated constructors. * We abandon series of lemmas of dubious utility. Those were already marked as such in `Algebra.Order.Ring.Lemmas` (by myself). * `...MonoRev` is replaced by `...ReflectLE` in the hope of being more understandable. * Some lemmas about commutativity of multiplication don't make sense for scalar multiplication. This PR links the new typeclasses to `OrderedSMul` and makes all old lemmas in `Algebra.Order.SMul` one-liners in terms of the new lemmas (except when they have the same name, in which case the lemma is simply moved) but doesn't delete the old ones to reduce churn. What remains to be done afterwards is thus: * finish the transition by deleting the duplicate lemmas from `Algebra.Order.SMul` * rearrange the non-duplicate lemmas into new files * generalise (most of) the lemmas from `Algebra.Order.Module` to `Algebra.Order.Module.Defs` * rethink `OrderedSMul` This PR also: * deletes `instModuleOrderDual`, which was accidentally duplicated in #8840. * fixes the dead links to Wikipedia in `Algebra.Order.SMul` and `Algebra.Order.Module`.
https://en.wikipedia.org/wiki/Ordered_module doesn't exist but https://en.wikipedia.org/wiki/Ordered_vector_space does. Also delete `instModuleOrderDual`, which was accidentally duplicated in #8840.
https://en.wikipedia.org/wiki/Ordered_module doesn't exist but https://en.wikipedia.org/wiki/Ordered_vector_space does. Also delete `instModuleOrderDual`, which was accidentally duplicated (with a more general statement) as `OrderDual.instModule'` in #8840.
Also add a few missing ones: * `OrderDual.instSMulWithZero` * `OrderDual.instMulAction` * `OrderDual.instMulActionWithZero` * `OrderDual.instDistribMulAction` In every case, we prime the originally unprimed/unnamed version.
https://en.wikipedia.org/wiki/Ordered_module doesn't exist but https://en.wikipedia.org/wiki/Ordered_vector_space does. Also delete `instModuleOrderDual`, which was accidentally duplicated (with a more general statement) as `OrderDual.instModule'` in #8840.
Also add a few missing ones:
OrderDual.instSMulWithZero
OrderDual.instMulAction
OrderDual.instMulActionWithZero
OrderDual.instDistribMulAction
In every case, we prime the originally unprimed/unnamed version.