Submodule.Quotient.nontrivial_of_lt_top

Stream: mathlib4

[Kevin Buzzard]

I'm getting the following deprecation warning in FLT:

`Submodule.Quotient.nontrivial_of_lt_top` has been deprecated: Use `Submodule.nontrivial_iff` instead

Note: The updated constant has a different type:
  ∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nontrivial (Submodule R M) ↔ Nontrivial M
instead of
  ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M},
    p < ⊤ → Nontrivial (M ⧸ p)

That result seems to be rather different -- how exactly am I supposed to say apply Submodule.Quotient.nontrivial_of_lt_top now? If my goal is Nontrivial (M ⧸ p) and I rw [\l Submodule.nontrivial_iff] then I have Nontrivial (Submodule R (M / p))
and in some sense I feel further away from p < ⊤ not nearer. Am I missing a trick? Why was this deprecated? Can I petition for adding it back?

[Nailin Guan]

I am also confused about this, since the lemma Submodule.Quotient.nontrivial_of_ne_top I added has also been deprecated.

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/blob/0fecc98248f62972b3fc32f83e1966c657fbb658/Mathlib/LinearAlgebra/Quotient/Basic.lean#L86-L90

[Johan Commelin]

The lemma still has a 3 line proof in Mathlib. So I'm not sure it should have been deprecated.

[Johan Commelin]

Aha! @Kevin Buzzard try Submodule.Quotient.nontrivial_iff

[Johan Commelin]

I think @[deprecated] is not picking up the correct nontrivial_iff.
cc @Damiano Testa

[Damiano Testa]

Thanks for the ping! I'm not really sure what else to do, other than qualifying fully the lemma. Also, I think that deprecated is in core, so any possible warning would likely come from there.

[Johan Commelin]

It seems like nontrivial_iff might be ambiguous at the file location. If so, I think Lean should warn about that.

[Kevin Buzzard]

Aha! Let me add this to #32137 ! It's another deprecation glitch in #31198 .

[Johan Commelin]

@Kim Morrison Is this worth an issue on the core repo?

Edit: nope, see #mathlib4 > Submodule.Quotient.nontrivial_of_lt_top @ 💬

[Damiano Testa]

Ah, sorry, I only realised now that the deprecations were generated by my script! :man_facepalming:

I'll have a think of how to improve this, but it probably involves a rewriting of the script in lean.

[Kevin Buzzard]

Ok so in total I found three deprecation issues in #31198 and I think I've fixed them all in #32137.

[Yaël Dillies]

@Kevin Buzzard, the deprecation is indeed broken, but you could have spared yourself going on Zulip by reviewing CFT#119 instead

[Johan Commelin]

But then we wouldn't have learned about this bug in @[deprecated]

[Yaël Dillies]

Yes, I'm just afraid that Kevin is once again trying to fix issues I've already solved for him :wink:

[Junyan Xu]

Is deprecated just using the same routine that Lean normally resolves name(space)s? Does #check nontrivial_iff return Submodule.nontrivial_iff? Why not docs#nontrivial_iff?

[Kevin Buzzard]

Yes I did things in a suboptimal order -- I just reviewed your (Yael's) class field theory bump (which showed how to deal with precisely the changes which had confused me in the FLT bump) and smiled to myself when I realised what had happened :-)

But how come you didn't notice the errors with deprecations yourself?

[Junyan Xu]

Oh, Submodule.Quotient.nontrivial_iff is protected, so it's correct behavior that it doesn't get picked up. Submodule.nontrivial_iff is not protected (it should probably be) so it gets picked up. So there's no Lean bug, only human error adding the deprecation.

[Johan Commelin]

Wow, thanks for investigating! Good to know

[Kevin Buzzard]

I should say that these errors are pretty hard to pick up in e.g. review. This is not the first one I've fixed when I've bumped FLT and found that something which was supposed to be deprecated hadn't been. Both times my first reaction was "grr, someone forgot to deprecate" but on both occasions the truth was that someone had tried and failed to deprecate (or had deprecated incorrectly) because of a namespace issue. We saw both instances of what can go wrong in #32137 : if you do the deprecation at the site of the new lemma then you might get the namespace of the old lemma wrong, and if you do it at the site of the old lemma then you might get the namespace of the new lemma wrong (although in this case it was because of a protected issue).

[Damiano Testa]

It seems also pretty tricky to think of what test could be performed automatically, as often, the deprecation points to a lemma that is different from the one being deprecated.

[Damiano Testa]

Maybe within mathlib, we can enforce that the lemma to which the deprecation points is always fully qualified and in the same file?

[Weiyi Wang]

I think this is where better declaration diff can help in review https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.22Declarations.20diff.22.20for.20PR.20emails.20misses.20namespaces.3F/with/537749453

[Ruben Van de Velde]

Damiano Testa said:

It seems also pretty tricky to think of what test could be performed automatically, as often, the deprecation points to a lemma that is different from the one being deprecated.

Well, if we had type-aware diffs, presumably we'd see that the type of deprecated lemma changed unexpectedly

[Kevin Buzzard]

Weiyi Wang said:

I think this is where better declaration diff can help in review https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.22Declarations.20diff.22.20for.20PR.20emails.20misses.20namespaces.3F/with/537749453

My understanding is that this tool (because it's not written in Lean) doesn't know which namespace you're in, so might struggle to flag these issues. For example the declaration diff in #31198 doesn't report that Submodule.subsingleton_quotient_iff_eq_top was removed and Submodule.Quotient.subsingleton_quotient_iff_eq_top was added (and immediately deprecated), because it didn't notice.