nontriviality and lemmas for subsingleton

Stream: mathlib4

[Antoine Chambert-Loir]

In #21546, I have proved two trivial lemmas that say that compute the degree and the leading coefficient of a polynomial when the ring is a subsingleton (hence the polynomial is 0). The only reason I added those lemmas is that the nontriviality tactic doesn't conclude if it isn't informed about these lemmas.

https://github.com/leanprover-community/mathlib4/blob/e65ecd800c3065b3f9468cab71b412ca6071f3d1/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean#L508

[Antoine Chambert-Loir]

(In his review, @Yaël Dillies managed to convince me that it is not reasonable to translate any single lemma for the zero object in a ring to a lemma for arbitrary objects on subsingletons, but in this case I need it.)

[Yaël Dillies]

Bringing the conversation back from github.

@Jz Pan said:

There is a problem that we have both Subsingleton.eq_one and Subsingleton.eq_zero. Maybe neither of them should be @[nontriviality] lemmas, as if it has both one and zero, there will be an infinity loop. So maybe @[nontriviality] degree_subsingleton is a reasonable choice.

But then we're back to writing a nontriviality lemma computing f 0 for every single function f

[Jz Pan]

Yaël Dillies said:

But then we're back to writing a nontriviality lemma computing f 0 for every single function f

I don't understand what do you mean.

At least for Polynomial there are already @[nontriviality] lemmas: https://loogle.lean-lang.org/?q=Polynomial%2C+Subsingleton and I don't find reasons why we shouldn't add it. The nontriviality R tactics only searches @[nontriviality] lemmas with Subsingleton R as an assumption, which I think wouldn't slow down if we add MvPolynomial.degree_of_subsingleton as a @[nontriviality] lemma.

They are not @[simp], though. So perhaps we should remove @[simp] from the lemma. Also, for the consistent of the naming, it should be named MvPolynomial.degree_of_subsingleton, i.e. there is an of.

[Yaël Dillies]

In essence, you are arguing that for every function foo : α → β, we should write @[nontriviality] lemma foo_of_subsingleton [Subsingleton α] (a : α) : f a = something_equal_to_f_0

[Jz Pan]

Yaël Dillies said:

In essence, you are arguing that for every function foo : α → β, we should write @[nontriviality] lemma foo_of_subsingleton [Subsingleton α] (a : α) : f a = something_equal_to_f_0

... if and only if f 0 = XXX is already a @[simp] lemma and Nontrivial α use case is common.

Yes I admit that it's a limitation of nontriviality tactics: if there is f x with x : α and [Subsingleton α], it should try to see if there are @[simp] lemmas of form f y = XXX where y is any other term of type α (which must be equal to x). But for now I think add XXX_of_subsingleton as @[nontriviality] lemmas is a useful workaround.