repeating instances from variable command

Stream: mathlib4

[Jovan Gerbscheid]

I noticed some lemmas like Matrix.diagonal_neg, Matrix.scalar_commute_iff, Matrix.scalar_commute have an instance hypothesis that is written down explicitly, while the same instance is also available from a variable statement. Should there be a linter that warns you about this?

variable [DecidableEq n] [Fintype n]
...
theorem scalar_commute_iff [Fintype n] [DecidableEq n] {r : α} {M : Matrix n n α} :
  ...

It may seem like this is only a problem of redundant text, but it can be more problematic if type class synthesis picks the instance from the variable command instead of the locally bound one, because then we get a duplicate hypothesis. This happened when I removed the definition Matrix.instMulMatrix in that file, and this caused an error further down the line.

[Yaël Dillies]

Isn't there a linter that warns you about duplicated hypotheses already?

[Ruben Van de Velde]

If you look at docs#Matrix.scalar_commute_iff, you'll see only one of each survived into the actual theorem, so there's no actual duplication. It does make the infoview somewhat confusing within the proof, though, so you should feel free to remove the redundant ones

[Jovan Gerbscheid]

I went ahead and removed many more of this kind of redundant instance hypotheses. https://github.com/leanprover-community/mathlib4/pull/11551

[Jovan Gerbscheid]

Can I get permission to make a branch in Mathlib? My Github is JovanGerb

[Johan Commelin]

@Jovan Gerbscheid Voila: https://github.com/leanprover-community/mathlib4/invitations

[Jovan Gerbscheid]

In this definition:

noncomputable def gramSchmidt [IsWellOrder ι (· < ·)] (f : ι → E) (n : ι) : E :=
  f n - ∑ i : Iio n, orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
termination_by n
decreasing_by exact mem_Iio.1 i.2

It is required to have the [IsWellOrder ι (· < ·)] argument explicitly, even if it is also given in a variable command, because the definition doesn't need the instance, but decreasing_by doesn't work without the instance. Is this intended?

[Jovan Gerbscheid]

I suppose it makes sense to require this instance explicitly, but the error message is quite confusing:

noncomputable def gramSchmidt (f : ι → E) (n : ι) : E :=
  f n - ∑ i : Iio n, orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
termination_by n
decreasing_by exact mem_Iio.1 i.2
/-
type mismatch
  mem_Iio.mp i.property
has type
  ↑i < n : Prop
but is expected to have type
  (invImage (fun a ↦ a) instWellFoundedRelation).1 (↑i) n : Prop
-/

[Patrick Massot]

This is probably a question for @Joachim Breitner.

[Joachim Breitner]

Not exactly a part of the code that I touched yet, but I wouldn’t be surprised if whatever logic decides which instances to pull in from variables won't know much about what happens after elaborating the def, but before it gets compiled WellFounded.fix.

Is it really the decreasing_by that doesn’t work, or is it the termination_by?
I wonder which well-founded relation it uses without the instance. Maybe run simp_wf after decreasing_by to see the goal better.

[Jovan Gerbscheid]

It is indeed decreasing_by that fails. The goal (with pp.explicit set to true) is

(@invImage ι ι (fun a ↦ a) (@instWellFoundedRelation ι (instSizeOf ι))).1 (↑i) n

the invImage (fun a ↦ a) doesn't do anything at all. The well-founded relation instance that it picks up is @instWellFoundedRelation ι (instSizeOf ι)), and this is just the trivial preorder.

[Jovan Gerbscheid]

simp_wf turns the goal into False :)

[Jovan Gerbscheid]

I think there could be some clearer error message when this instance is picked up, because proving False is quite hard.

[Joachim Breitner]

because proving False is quite hard.

but worth it, afterwards all your other theorems are much easier to prove!

[Joachim Breitner]

I wonder how useful this “every type has a trivial sizeOf instance” is. Maybe it was needed before we inferred sensible lexicographic orders? It might be possible to catch this explicitly; I'll keep an ear open if this is something that happens often.