reassoc_of% misleading error

Stream: mathlib4

[Robert Maxton]

So, I appreciate the recent-ish movement to add more informative error messages throughout Lean/Mathlib on the whole. In the specific case of reassoc_of%, however, I think the changed error is a bit of a regression.

[Robert Maxton]

reassoc_of% now reports that
`reassoc` can only be used on terms about equality of (iso)morphisms
any time it fails to fully elaborate, but a very common reason for reassoc_of% to fail isn't because you're using it on the wrong type, but rather because it can't infer the category you're in. This was an existing issue, but at least before it would simply tell you that fairly directly.

[Joël Riou]

I have used reassoc_of% very extensively, and I never encountered any such error. Could you share a MWE?

[Robert Maxton]

Huh, really? I get it absolutely constantly.

#mwe:

import Mathlib.CategoryTheory.Limits.Shapes.Products

open CategoryTheory Limits

variable {C : Type u} [Category.{v, u} C]
         {β : Type w} {f : β → C} [HasCoproduct f] {P : C}
         (p : (b : β) → f b ⟶ P) (b : β)

--fails
example {Q : C} (g : P ⟶ Q) : Sigma.ι f b ≫ Sigma.desc p ≫ g = p b ≫ g := by
  rw [reassoc_of% Sigma.ι_desc]

--succeeds
example {Q : C} (g : P ⟶ Q) : Sigma.ι f b ≫ Sigma.desc p ≫ g = p b ≫ g := by
  rw [reassoc_of% Sigma.ι_desc (C := C)]

[Robert Maxton]

(unrelatedly, Sigma.ι_desc really should just have a reassoc...)

[Joël Riou]

It is not "unrelatedly": the solution is to add the reassoc attribute to Sigma.ι_desc.

[Joël Riou]

In my own code, I use reassoc_of% only in two situations:

• I have an assumption like fac : f ≫ g = h and I want to rewrite this in a goal or in another assumption;
• I want to use a lemma foo (which may have an assoc variant), but the term produced by foo exactly matches a subexpression in my goal only after doing dsimp, then I do have := foo ...; dsimp at this; rw [reassoc_of% this].

Otherwise, the automatically generated _assoc lemmas should be enough, but some of these are missing.

[Robert Maxton]

Perhaps it's not truly unrelated, but I generally use reassoc_of% precisely to avoid having to recompile some large number of files after having to change something early in the import tree. For something like Sigma.ι_desc that I use frequently it makes sense to just take the hit, but if it's a lemma I only use once, I'd rather not wait the twenty minutes until the end of the project.

[Kyle Miller]

Robert Maxton said:

I appreciate the recent-ish movement to add more informative error messages

Just to clarify this point, the recent change to reassoc_of% was not for the sake of changing the error messages, but to add isomorphism support.

The way it works is that it tries both the isomorphism and morphism handlers, and if both handlers fail, it gives a somewhat generic error message. This can be improved, but I figured it was better to get isomorphism support sooner than to reengineer the PR to try to expose errors during construction.

It's possible that what needs more work here isn't primarily the error, but getting this elaborator to postpone if it doesn't know the category yet. (Maybe it can work out the category from the expected type if it waits longer? Or maybe it could tolerate not finding instances by adding extra instance arguments?)

[Robert Maxton]

Roughly speaking, these errors are occurring in places where rw or simp could otherwise do the job, i.e. if you add @[reassoc] to the original lemma then the rw goes through. So in principle, the type information should be there; I don't know how to communicate it to reassoc_of%, but I'll take a look at it later today.

[Kyle Miller]

It looks like the issue is roughly that reassoc_of% uses Term.elabTerm, which for constants means to add in metavariables for each implicit argument.

It could copy rw/simp and treat constants as a special case.

[Kyle Miller]

That might be a little strange for a term elaborator though...

[Robert Maxton]

Mm. It can't use one of the mapFooTelescopings to just generate a quantified lemma?

[Robert Maxton]

Ah, I think I was thinking of docs#Lean.Meta.mapForallTelescope'

[Kyle Miller]

No, most uses of reassoc_of% are applied to a term, not a constant, so the elaborator has to be involved somehow.

[Kyle Miller]

The problem is that if you do reassoc_of% Sigma.ι_desc, then it's seeing Sigma.ι_desc, not @Sigma.ι_desc.

[Kyle Miller]

I suppose this does suggest a workaround for you: have you tried putting @ in front of this lemma?

[Robert Maxton]

... Ahhhh. I see now. Interesting.

Lemme try the @.

[Kyle Miller]

Just tried it, it works:

example {Q : C} (g : P ⟶ Q) : Sigma.ι f b ≫ Sigma.desc p ≫ g = p b ≫ g := by
  rw [reassoc_of% @Sigma.ι_desc]

[Kyle Miller]

I think another approach here would be to modify these handlers to not use mkAppM, but rather some elaborator functions (and possibly also to wrap elabTerm in withSynthesizeLight)

[Robert Maxton]

Beat me to it. Given that I do ultimately agree that the 'correct' final solution for PRs should be "just apply @[reassoc] at the source whenever possible", I think it's probably fine if the solution looks like:

• Check to see if the error is because the target actually isn't a relation of morphisms/isomorphisms, or because of synthesis failure/unbound metavariables
  • Even if the term given is the body of an function with un-solved-for implicits, the body should still match against Quiver.Hom _ _ or Iso _ _ right?
• If it's because of unbound metavariables, then say so and suggest prepending @, otherwise use the current error.

But I certainly won't say no to a more sophisticated elaboration handler!

[Kyle Miller]

Right now it's relying on mkAppM to do the defeq check you mention, but the big problem with using mkAppM is that it insists on synthesizing the Category theory instance itself, but it's in MetaM, so it has no concept of deferring synthesis.

It would certainly help though if the handlers were broken into two phases, one to check if it should commit to applying, and another to build the proof. These are lumped into one step, which means any failure anywhere causes it to move on to the next handler.

[Kyle Miller]

#26130 implements a new elaboration scheme, and it makes the MWE work.

Haven't waited to see if all of mathlib builds yet though.