mathlib
mathlib copied to clipboard
leanprover-community
refactor(algebra/order/floor): Relax lemmas to remove `linear_order` requirement
There is a TODO in algebra/order/floor.lean which notes that many lemmas do not require the linearly ordered part of their hypothesis and these could be relaxed. This commit actions this TODO.
Reviewers should make sure:
- No lemmas have disappeared in this refactor.
- There are no lemmas that could be loosened, but haven't been.
Note that I haven't changed any proofs unless strictly necessary - in one place (floor_mono') I have added a lemma where there was an obvious loosening of both conclusion and hypothesis. There may be others like this. There may also be lemmas which are true under looser hypotheses, but whose proofs currently use stronger lemmas than necessary. These are difficult to find, and important to spot if we can find any: I cannot.
Cool - I wonder if some sort of poll is appropriate to get a sense of community opinion on this? I can see both cases.
In my opinion, the work is done, let's merge it, but let's remove the todo so that extra work isn't done. (I'm still not convinced that the work is unnecesary, but anyways...). Generalising always is a benefit when formalising, in my experience, regardless of the mathematicality and the usefulness of it. You can do a poll in the zulip.
@YaelDillies Do I understand correctly from Zulip that you are no long opposed to this PR?
My understanding is that @YaelDillies wants to actually see the example that was cited - but there's no reason it has to be Yael who gives the OK here; that's why I asked for a vote. I thought the outcome of that was that people were happy to see it added.
I am not opposed anymore, but I still want to see that prod.floor_ring instance, be it on this PR or on a branch depending on #16172. I just want to make sure the example actually works.
I will note that we only have one instance of floor_semiring currently, which feels... off.
nnrat was added recently and it is a floor_semiring (even though I forgot to prove it). But even without that the docs say we have four instances.
Oh yes, sorry. I wasn't counting the two in the floor.lean file itself because I'd already fixed them! nnrat is derivable like nnreal from the nonneg instance so I'll just slip that in while I'm here.
If you think that's best.
On Wed, 12 Oct 2022, 07:04 Yaël Dillies, @.***> wrote:
@.**** commented on this pull request.
In counterexamples/map_floor.lean https://github.com/leanprover-community/mathlib/pull/16352#discussion_r993029923 :
- rw [←neg_lt_neg_iff, ←map_neg, ←cast_neg, ←floor_neg_eq_neg_ceil, ←floor_neg_eq_neg_ceil,
- ←map_neg, neg_add', ←cast_neg],
Can you rename your floor_neg/floor_neg' to floor_neg_iff and revert that name change?
— Reply to this email directly, view it on GitHub https://github.com/leanprover-community/mathlib/pull/16352#discussion_r993029923, or unsubscribe https://github.com/notifications/unsubscribe-auth/AIDTA6CQCWTS4DMHAIUDI7LWCZIGXANCNFSM6AAAAAAQDJJPAQ . You are receiving this because you authored the thread.Message ID: @.***>
Added some more generalisations. I feel like ceil_add_nat should be able to be proved without the linearity, but I cannot see how.
Sorry, I've not had the time to work on this as much. Mistake I think.
On Wed, 19 Oct 2022, 16:44 Yaël Dillies, @.***> wrote:
@.**** commented on this pull request.
In counterexamples/map_floor.lean https://github.com/leanprover-community/mathlib/pull/16352#discussion_r999643033 :
- rw [←neg_lt_neg_iff, ←map_neg, ←cast_neg, ←floor_neg_eq_neg_ceil, ←floor_neg_eq_neg_ceil,
- ←map_neg, neg_add', ←cast_neg],
It still hasn't disappeared from the diff.
— Reply to this email directly, view it on GitHub https://github.com/leanprover-community/mathlib/pull/16352#discussion_r999643033, or unsubscribe https://github.com/notifications/unsubscribe-auth/AIDTA6AEQKLQ2OO534SHTDTWEAJOPANCNFSM6AAAAAAQDJJPAQ . You are receiving this because you authored the thread.Message ID: @.***>
I have a bunch of improvements to this PR that rely on char_zero lemmas being available for strict_ordered_semirings, so I will change strict_ordered_semiring to extend nontrivial to turn strict_ordered_semiring.to_char_zero into an instance.
This PR/issue depends on:
- ~~leanprover-community/mathlib#17394~~ By Dependent Issues (🤖). Happy coding!
It is sadly way under the tide, so I think it'd be better to wait after the port, especially given that nothing urgently depends on it.