ordered_comm_group unnecessary field

Stream: general

[Mario Carneiro]

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]

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]

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]

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]

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]

And ordered_semiring of course

[Anton Lorenzen]

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

[Kevin Buzzard]

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]

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

[Anton Lorenzen]

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

[Anton Lorenzen]

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

[Anton Lorenzen]

Fix the new errors = new 3.8 branch

[Bryan Gin-ge Chen]

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]

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]

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]

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