[Merged by Bors] - feat(algebra/order/interval): Interval arithmetic#16761
[Merged by Bors] - feat(algebra/order/interval): Interval arithmetic#16761YaelDillies wants to merge 15 commits intomasterfrom
Conversation
|
This PR/issue depends on:
|
Vierkantor
left a comment
There was a problem hiding this comment.
There are still a few TODOs in the code, are you planning to deal with them yourself or would you like suggestions?
src/algebra/order/interval.lean
Outdated
| rw [pure_mul_pure, h, pure_one] } | ||
| end | ||
|
|
||
| -- @[to_additive] |
There was a problem hiding this comment.
Are you planning on adding the corresponding additive instance (I assume manually, based on the comments on subtraction)?
There was a problem hiding this comment.
Whoops, I completely forgot about those.
There was a problem hiding this comment.
Btw, the reason we need this duplication is because interval.has_div (purposefully) doesn't match interval.has_sub. I guess if we had has_ordered_div, the problem would also be fixed, but the consensus is that we don't need it.
|
I fixed the ones I could, and I don't know whether the last one is fixable. |
| /-! | ||
| # Interval arithmetic | ||
|
|
||
| This file defines arithmetic operations on intervals and prove their correctness. Note that this is |
There was a problem hiding this comment.
As for correctness: are you planning to prove results like a ∈ s → b ∈ t → a + b ∈ s + t?
There was a problem hiding this comment.
I am split between showing these and defining an "interval operation" as something like
structure interval_hom (f : α → β) :=
(to_fun : interval α → interval β)
(mem_map' := ∀ a s, a ∈ s → f a ∈ to_fun s)
and then bundling operations as interval_homs. I guess both is an answer.
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
bors merge |
Define arithmetic operations on `interval`/`nonempty_interval` and prove their correctness.
|
Build failed: |
|
bors d+ |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
Define arithmetic operations on `interval`/`nonempty_interval` and prove their correctness.
|
Pull request successfully merged into master. Build succeeded:
|
|
Pull request successfully merged into master. Build succeeded:
|
Define arithmetic operations on
interval/nonempty_intervaland prove their correctness.