[Merged by Bors] - feat(algebra/ordered_sub): define truncated subtraction in general #8503
Conversation
fpvandoorn
added
awaiting-review
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
| @@ -467,166 +468,137 @@ end | |||
| @[simp] lemma pred_one_add (n : ℕ) : pred (1 + n) = n := | |||
| by rw [add_comm, add_one, pred_succ] | |||
|
|
|||
| /-! ### `sub` -/ | |||
There was a problem hiding this comment.
What is the motivation for deleting some lemmas and keeping some with a new proof?
There was a problem hiding this comment.
The goal is to remove (basically) all of them, and only use the lemmas that are proven for general types. But I'll do that in future PRs (that is what I meant by "Remove the lemmas specific to each individual type").
I currently replace the proof to show that we have the general lemma.
I have already removed a couple of lemmas, but I'll do the rest in future PRs
| section ordered_add_comm_monoid | ||
| variables {a b c d : α} [partial_order α] [add_comm_monoid α] [has_sub α] [has_ordered_sub α] | ||
|
|
||
| @[simp] lemma sub_le_iff_right : a - b ≤ c ↔ a ≤ c + b := |
There was a problem hiding this comment.
Could you explain how you selected this set of lemmas for the remainder of the file? Is it based on what we have already proven for ℕ + any intermediate results needed for them?
There was a problem hiding this comment.
It was mostly the stuff proven for nat;
Some of it was proven for another specific type like ennreal;
Some of the lemmas were variations on already existing lemmas (for example: for nat and iff was proven, and contravariant_class is needed for one direction. That results in 3 lemmas: the direction that always holds without assumptions, the iff under an add_le_cancellable assumption and the iff under an contravariant_class assumption);
Some of the lemmas are analogues of subtraction lemmas from ordered_group (often with additional assumptions in this file).
Vierkantor
added
awaiting-author
|
Thanks for the review! |
fpvandoorn
added
awaiting-review
src/algebra/ordered_monoid.lean
Outdated
|
|
||
|
|
|
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
…8503) * Define and prove properties of truncated subtraction in general * We currently only instantiate it for `nat`. The other types (`multiset`, `finsupp`, `nnreal`, `ennreal`, ...) will be in future PRs. Todo in future PRs: * Provide `has_ordered_sub` instances for all specific cases * Remove the lemmas specific to each individual type Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
nat. The other types (multiset,finsupp,nnreal,ennreal, ...) will be in future PRs.Todo in future PRs:
has_ordered_subinstances for all specific cases