Zulip Chat Archive

Stream: general

Topic: ordered_comm_group unnecessary field


Mario Carneiro (Mar 28 2020 at 02:02):

Just found this comment in algebra.ordered_group:

/--
The `add_lt_add_left` field of `ordered_comm_group` is redundant, but it is in core so
we can't remove it for now. This alternative constructor is the best we can do.
-/
def ordered_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α]
  (add_le_add_left :  a b : α, a  b   c : α, c + a  c + b) :
  ordered_comm_group α :=

does anyone feel like writing a lean PR for this?

Anton Lorenzen (Mar 30 2020 at 09:42):

I could do that. I guess I should remove the field from the class but leave the lemmas in the file as they are and fix lean and Mathlib where necessary?

Mario Carneiro (Mar 30 2020 at 09:47):

Yes. Remove the field, make a theorem with the same name using the proof in this constructor, and then remove this field in any constructions of ordered_comm_group, delete ordered_comm_group.mk' and replace all uses with the regular constructor

Anton Lorenzen (Mar 31 2020 at 15:45):

This also applies to decidable_linear_ordered_comm_group and ordered_ring where mul_nonneg follows from mul_pos and em. Should I remove these fields too?

Anton Lorenzen (Mar 31 2020 at 15:45):

lemma ordered_ring.mul_nonneg {α} [s : ordered_ring α] (a b : α) (h₁ : 0  a) (h₂ : 0  b) : 0  a * b :=
begin
  cases classical.em (a  0), { simp [le_antisymm h h₁] },
  cases classical.em (b  0), { simp [le_antisymm h_1 h₂] },
  exact (le_not_le_of_lt (ordered_ring.mul_pos a b (lt_of_le_not_le h₁ h) (lt_of_le_not_le h₂ h_1))).left,
end

Anton Lorenzen (Mar 31 2020 at 15:54):

And ordered_semiring of course

Anton Lorenzen (Mar 31 2020 at 16:48):

And do you know which branch of mathlib compiles with the current lean master branch?

Kevin Buzzard (Mar 31 2020 at 16:59):

You can always look at leanpkg.toml on any mathlib branch to find out which version of Lean it expects to run with.

Bryan Gin-ge Chen (Mar 31 2020 at 17:06):

I could be wrong, but I don't think we have a 3.8.0c staging branch for mathlib yet.

Anton Lorenzen (Mar 31 2020 at 17:07):

I haven't been able to find one. At least the more recent branches assume 3.7.2

Anton Lorenzen (Mar 31 2020 at 17:07):

Should I try to fix the new errors? Or apply the patch to 3.7? Or just work on the lean compiler?

Anton Lorenzen (Mar 31 2020 at 17:08):

Fix the new errors = new 3.8 branch

Bryan Gin-ge Chen (Mar 31 2020 at 17:10):

I suggest opening a PR to Lean core first. After that's merged we can worry about fixing mathlib. @Gabriel Ebner what do you think?

Gabriel Ebner (Mar 31 2020 at 17:42):

Yes, please open a PR to the lean repo first. I suspect that the 3.8 release is happening soon. It doesn't make much sense to have a 3.8 branch for mathlib long before the release, you'd just spend lots of time keeping up with mathlib.

Gabriel Ebner (Mar 31 2020 at 17:44):

To clarify, there will be a 3.8 branch. It will be be opened around the 3.8 release date. You don't need to fix mathlib before then.

Anton Lorenzen (Mar 31 2020 at 17:47):

Done :) I'll wait for the 3.8 release then..


Last updated: Dec 20 2023 at 11:08 UTC