leanprover-community
chore(algebra/order/monoid_lemmas_zero_lt): move all positivity assumptions to the first place
Actually, I am now trying out to remove duplicate lemmas from algebra.order.ring and i think that the guiding principle should be that the order of explicit assumptions in this file should match the order of the corresponding lemma in algebra.order.ring.
Actually, I am now trying out to remove duplicate lemmas from
algebra.order.ringand i think that the guiding principle should be that the order of explicit assumptions in this file should match the order of the corresponding lemma inalgebra.order.ring.
The order of the arguments in lemmas from algebra.order.ring also seems to be inconsistent, and I would prefer to change them to be consistent. In fact, I was going to replace the proof of ordered_ring lemmas with zero_lt lemmas first, and then try to delete ordered_ring lemmas and use zero_lt lemmas directly.
Many of the lemmas in zero_lt still have stronger assumptions at the moment, mainly because zero_le_one_class and zero_lt_one_class (which is not even in the mathlib yet) are not used in zero_lt yet. So I haven't moved forward with such an attempt.
Here is how I view this. Changing the order of hypotheses in "well-established" lemmas (e.g. the lemmas in algebra.order.ring) is something which involves touching a lot of files for a relatively small gain. It is also going to generate some discussion with people preferring one order over another (even I had an alternative convention to the one you has proposed and I have close to no opinion on this).
Replacing lemmas with lemmas with weaker assumptions is probably less controversial, has a bigger impact and involves changing a probably much smaller number of files.
For these reasons, I prefer to do the higher-gain change first (remove the duplicate lemmas, maintaining inconsistent names and order of hypotheses) and then going with the inconsistencies, rather than the other way around.
What do you think?
I agree with this approach. On the other hand, I'm a bit worried that the lemmas in zero_lt are not fully completed and it may be too early to export and replace lemmas. Of course I agree that such changes have to be made eventually, and it seems to work currently.
I agree that the lemmas where 0 and 1 both appear are still work in progress. However, the zero_le_one class was introduced very recently, and there were some doubts as to whether the zero_lt_one class would actually be useful. I suspect (though I have not really thought carefully about this), that we will probably have to make something ad hoc for these interactions. For instance, in a semiring (+ typeclasses) it is equivalent to have some positive element to having 0 < 1:
import algebra.order.ring
lemma zero_lt_one_of_pos {α} [semiring α] [partial_order α] [pos_mul_reflect_lt α]
{a : α} (a0 : 0 < a) : (0 : α) < 1 :=
lt_of_mul_lt_mul_left ((mul_zero _).le.trans_lt (a0.trans_le (mul_one _).ge)) a0.le
lemma exists_pos_iff_zero_lt_one {α} [semiring α] [partial_order α] [pos_mul_reflect_lt α] :
(∃ a, (0 : α) < a) ↔ (0 : α) < 1 :=
begin
refine ⟨_, λ h, ⟨_, h⟩⟩,
rintro ⟨a, ha⟩,
exact zero_lt_one_of_pos ha,
end
However, there is always the (very pathological) case in which 0 is a maximal element of the order...
@negiizhao @adomani Do I understand correctly that this PR should be put on hold till another refactor is done? If so, can this maybe be reflected by a depends on: #prnr?
If I had to choose between all first and all last, I would put the 0 ≤ and 0 < arguments all last, so that we can make them opt_params using positivity.
I will change this PR to move the positivity assumption to the last, it seems better.
This PR/issue depends on:
- ~~leanprover-community/mathlib#16172~~
- ~~leanprover-community/mathlib#16189~~ By Dependent Issues (🤖). Happy coding!
