mathlib4#1129

Stream: mathlib4

[Arien Malec]

Could someone look at what the instance issue is with this PR? I can get on hover that Lean 4 thinks we only know 0 < ↑x ^ ?m.1594, I think for the type of the subset, but it's confusing because the type only shows up when I look "between" parameters of zpow_pos_of_pos

[Kevin Buzzard]

instance : Pow { x : K // 0 < x } ℤ :=
  ⟨fun x n => ⟨(x : K) ^ n, zpow_pos_of_pos x.2 _⟩⟩

[Kevin Buzzard]

I am worried about this syntactic tautology stuff. The linter says

-- porting note: syntatic tautology in Lean 4
-- @[simp]
-- theorem coe_zpow (x : { x : K // 0 < x }) (n : ℤ) : ↑(x ^ n) = (x ^ n : K) :=
--   rfl
-- #align positive.coe_zpow Positive.coe_zpow

but the autoporter has not correctly translated this statement from Lean 3 to Lean 4 because of the changes in elaboration which I explained in https://github.com/leanprover/lean4/issues/1915 . What worries me is that people might be thinking "oh a linter is telling me I don't need this lemma any more so I'll ignore it" -- what needs to be done is that the lemma needs to be reformulated so that it actually reflects the lemma which is supposed to be ported. @Mario Carneiro is there anything which the autoporter can do about this?

[Mario Carneiro]

Mathport will notice if you port the wrong theorem, even if you did so on mathport's recommendation. Assuming the syntaut linter wasn't there and we ported this theorem, after performing the #align mathport will tell you about how it's a dubious translation and so you should take another look at it and either fix it or document why it is expected to be a mismatch.

[Kevin Buzzard]

What I'm worried about it users just deleting the lemmas because they're being informed that they're "no longer needed".

[Mario Carneiro]

If you just delete the theorem then mathport will put it back, treating it similarly to a new mathlib theorem

[Mario Carneiro]

the only case where it won't is if you #noalign it

[Mario Carneiro]

We should probably have review standards around #noalign to require documentation or otherwise some kind of indication why it should not be ported

[Kevin Buzzard]

What the lemma should say is ↑(x ^ n) = (↑x) ^ n. In Lean 3 one could write this as ↑(x ^ n : { x : K // 0 < x }) = (x ^ n : K) but in Lean 4 this is being interpreted as a syntactic tautology and one needs to write instead e.g. ↑(x ^ n) = (x : K) ^ n because elaboration is no longer happening from the outside in.

[Mario Carneiro]

right, there's a core lean issue open about this

[Kevin Buzzard]

Mario Carneiro said:

If you just delete the theorem then mathport will put it back, treating it similarly to a new mathlib theorem

I'm talking about human porters deleting the lemma because the autoporter's message is confusing, and making a PR which get hurriedly merged.

[Mario Carneiro]

yes I know

[Mario Carneiro]

what I said will still happen

[Mario Carneiro]

if you just delete stuff from a port file then mathport will think you didn't finish the job and point out everything you missed

[Mario Carneiro]

we need to get in the habit of checking mathport results on already ported files occasionally to incorporate new stuff from mathlib and also catch errors like this, but it's fine if we only do it once in a while since it's usually an order of magnitude easier than the initial port

[Kevin Buzzard]

@Arien Malec you are using Positive.Subtype.hasInv for the inverse instance However the naming convention has changed. You now need to use instInvSubtypeLtToLTToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRingOfNatToOfNat0ToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToLinearOrderedSemifield.

[Mario Carneiro]

we also need to do a diff between mathlib3 and mathlib4 to fix style issues for syntax patterns that are ignored by mathport, but this is also something that we can do in bulk later

[Kevin Buzzard]

Alternatively you might want to change the name of the auto-generated instance.

[Kevin Buzzard]

instance Subtype.hasInv : Inv { x : K // 0 < x } :=
  ⟨fun x => ⟨x⁻¹, inv_pos.2 x.2⟩⟩

I'll let you choose whether you want to go with the auto-generated instance or rename it like the above. Then you can use Positive.Subtype.hasInv as suggested by the autoporter.

[Mario Carneiro]

I think we need to make a "instance with long name" linter to prevent the issue @Floris van Doorn mentioned about exponential growth of instance names

[Arien Malec]

I like that better, but to be clear, that's not where I'm stuck....

[Kevin Buzzard]

namespace Positive

instance Subtype.inv : Inv { x : K // 0 < x } :=
  ⟨fun x => ⟨x⁻¹, inv_pos.2 x.2⟩⟩

@[simp]
theorem coe_inv (x : { x : K // 0 < x }) : ↑x⁻¹ = (x⁻¹ : K) :=
  rfl
#align positive.coe_inv Positive.coe_inv

instance Subtype.pow : Pow { x : K // 0 < x } ℤ :=
  ⟨fun x n => ⟨(x : K) ^ n, zpow_pos_of_pos x.2 _⟩⟩

@[simp]
theorem coe_zpow (x : { x : K // 0 < x }) (n : ℤ) : ↑(x ^ n) = (x : K) ^ n :=
  rfl
#align positive.coe_zpow Positive.coe_zpow

instance : LinearOrderedCommGroup { x : K // 0 < x } :=
  { Positive.Subtype.inv, Positive.linearOrderedCancelCommMonoid with
    mul_left_inv := fun a => Subtype.ext <| inv_mul_cancel a.2.ne' }

end Positive

The final instance still doesn't work but I need to sleep now. The other issues are fixed.

[Arien Malec]

Thx...

[Kevin Buzzard]

Oh no!

set_option maxHeartbeats 2000000

instance : LinearOrderedCommGroup { x : K // 0 < x } :=
  { Positive.Subtype.inv, Positive.linearOrderedCancelCommMonoid with
    mul_left_inv := fun a => Subtype.ext <| inv_mul_cancel a.2.ne' }

works! The default max heartbeats is not enough :-( This does not bode well.

[Arien Malec]

ugh...

[Kevin Buzzard]

set_option maxHeartbeats 304000 works, but 303000 doesn't.

[Arien Malec]

Pushed and credited to @Kevin Buzzard ..

The instance issue that I flagged still persists and the updated lemma is no longer rfl....

[Kevin Buzzard]

Sorry, what are you flagging? For me the file was compiling.

[Arien Malec]

Oh, I see the diff.

[Kevin Buzzard]

I can't guarantee that I've given the instances good names, in afraid I'm still baffled by the naming convention.

[Arien Malec]

Super odd that Lean 4 infers the correct type in the binder fun x n then loses it in the function body.

[Arien Malec]

Probably Positive.Subtype.instInv?

[Kevin Buzzard]

I'm a big fan of the auto-generated instance names but my impression is that I'm in a minority.

[Adam Topaz]

There was a discussion about these recently... search for "exponential blowup" :grimacing:

[Kevin Buzzard]

Yeah I'm also a fan of that.

[Kevin Buzzard]

Move fast and blow up stuff

[Arien Malec]

So:

import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Algebra.Order.Positive.Ring

variable {K : Type _} [LinearOrderedField K]

instance : Pow { x : K // 0 < x } ℤ :=
  ⟨fun x n => ⟨x ^ n, zpow_pos_of_pos x.2 _⟩⟩

Lean fails to infer that x is K in the function body.

[Arien Malec]

Lean needs

instance : Pow { x : K // 0 < x } ℤ :=
  ⟨fun x n => ⟨(x: K) ^ n, zpow_pos_of_pos x.2 _⟩⟩

to typecheck properly.

[Scott Morrison]

Arien Malec said:

Probably Positive.Subtype.instInv?

I think just Positive.Subtype.inv. We haven't been including inst in most of the manually named instances so far.