missing instance in CategoryTheory.GlueData

Stream: mathlib4

[Moritz Firsching]

In mathlib4#3099, I'm stumbling across

failed to synthesize instance
  HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F)))

Seems that lean4 is not able get that instance whie lean4 was? How should I add it?

[Adam Topaz]

haveI. We’ve had to do this elsewhere as well in some of the category theory files that have been ported

[Kevin Buzzard]

I thought that Lean 3 haveI is lean 4 have?

[Kevin Buzzard]

have works fine:

def gluedIso : F.obj D.glued ≅ (D.mapGlueData F).glued :=
  have : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))) := inferInstance
  preservesColimitIso F D.diagram.multispan ≪≫ Limits.HasColimit.isoOfNatIso (D.diagramIso F)

[Kevin Buzzard]

Lean 4 haveI means something else (I for inline, not instance)

[Adam Topaz]

Yeah, I know. But i was under the impression that inlining is still preferable in such cases. Maybe a TC expert can chime in

[Kevin Buzzard]

oh lol sorry for adding to the confusion then :-) I have no idea what inline even means.

[Yaël Dillies]

It means not creating a let binding.

[Kevin Buzzard]

The terms produced are indeed different with have and haveI (at least with pp.all on)

[Kevin Buzzard]

yeah but the problem is that I don't know what a let binding is either :-/

[Kevin Buzzard]

indeed with pp.all off the diff is

>   let_fun this := (_ : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))));

[Kevin Buzzard]

So if have adds some random junk to the term, is there ever a use case where have is better than haveI?

[Yaël Dillies]

You can think of it as a local definition. let y := f x in (y, y) is defeq to (f x, f x) but only after inlining the let binding. So the difference is not about defeq but about computation. I'm not actually sure what Lean 4 does here, but a reasonable thing to expect would be that (f x, f x) computes f x twice, while let y := f x in (y, y) computes it only once.

[Kevin Buzzard]

Wait -- are you saying they're not defeq?

[Yaël Dillies]

They are defeq! but (potentially, don't quote me) not computationally identical.

[Kevin Buzzard]

yeah this is all a bit CS for me. I'm not sure I have any feeling for how many times something gets computed. Thanks!

[Kevin Buzzard]

Still interested to know why have is ever better than haveI

[Yaël Dillies]

Kevin Buzzard said:

So if have adds some random junk to the term, is there ever a use case where have is better than haveI?

This question can basically be rephrased as "Why do we need definitions in mathematics? Can't we just write strings of symbols from the axioms?"

[Kevin Buzzard]

have v haveI -- Oh I see -- you just answered this

[Kyle Miller]

Kevin Buzzard said:

So if have adds some random junk to the term, is there ever a use case where have is better than haveI?

I wouldn't call it either random or junk. let_fun x := v; w is syntactic sugar for (fun x => w) v. It's how Lean 4 implements have. See how w gets x but not the value of v itself.

haveI is the same as doing beta reduction of let_fun Think about what happens if x appears multiple times and you have multiple levels of haveIs: your proof becomes exponentially big relative to the number of haveIs.

[Kevin Buzzard]

So this is all about implementation issues, basically, which is something I've resolutely ignored ever since I joined this community. I'm just grateful that there are many people here who do understand them!

[Kyle Miller]

Then again, haveI is apparently how Lean 3's have worked (a little experiment)

[Kevin Buzzard]

So in that example I have absolutely no feeling about which is better out of 2 + 2 + (2 + 2) + (2 + 2 + (2 + 2)) and let_fun n := 2; let_fun n' := n + n; let_fun n'' := n' + n'; let_fun n''' := n'' + n''; n'''.

[Kevin Buzzard]

They're just the same thing as far as I can see.

[Kyle Miller]

Yaël Dillies said:

It means not creating a let binding.

To be clear, neither have nor haveI make let expressions. In a let expression, the body has access to the value itself for the variable that's defined. With have/haveI/let_fun, it doesn't.

[Kevin Buzzard]

Does it depend on context as to which is "better"?

[Moritz Firsching]

in any case, I have now fixed it by using have : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))) := inferInstance, in the two lemma where it was needed.
Thanks everybody!

[Kevin Buzzard]

well apparenly you should be using haveI :-)

[Kyle Miller]

Kevin Buzzard said:

They're just the same thing as far as I can see.

Asymptotically the let_fun seems like it's better, since if you keep nesting it you'll otherwise have exponentially many 2's. Whether this matters practice for elaboration I have no idea.

[Moritz Firsching]

have it is then...

[Kevin Buzzard]

With haveI the term gluedIsowhen printed out in full is 16K. With have it is 20K. Is this an argument for haveI?

[Ruben Van de Velde]

Or is it an argument against printing them out?

[Kyle Miller]

Printing can be misleading, since subterms might be re-used, and there's some sort of cache so that things can be computed just once (though I'm not sure how this works or where it applies). As a user it looks like a term is a tree-like structure, but it's actually stored as a directed acyclic graph.

[Eric Wieser]

Kevin Buzzard said:

So in that example I have absolutely no feeling about which is better out of 2 + 2 + (2 + 2) + (2 + 2 + (2 + 2)) and let_fun n := 2; let_fun n' := n + n; let_fun n'' := n' + n'; let_fun n''' := n'' + n''; n'''.

The second one requires you to call dsimp in order to get to the poof state with the 2s

[Eric Wieser]

So for definitions you want to prove things about, inlining everything can save you some cleanup at the start of a proof

[Kevin Buzzard]

Which one has been inlined? (I don't know the meaning of the word)

[Eric Wieser]

The inlined version of let x := 2 in f x is f 2; (the value of) x has been "inlined"

[Kevin Buzzard]

so "inlined" means "substituted in". Thanks!

[Kevin Buzzard]

And I guess presumably the point is that inlining doesn't change things up to definitional equality but does change them up to syntactic equality. Thanks, this has been instructive. The only confusion I have left is why the inlined term in the original example above is far smaller than the outlined one; I would have thought that inlining essentially always makes terms bigger.

[Adam Topaz]

It doesn't really matter in category theory, I guess, since we use dsimp with impunity.

[Moritz Firsching]

A slighlty more mundane argument in favor of haveI over have is that the linter does not complain. It does complain for have
https://github.com/leanprover-community/mathlib4/actions/runs/4521142492/jobs/7962715755?pr=3099
So I changed it back to haveI

[Kevin Buzzard]

That is a surprising error for me! If the have term is not actually used by the main term then typeclass inference wouldn't have complanied when it couldn't find the have term!

[Kevin Buzzard]

@Johan Commelin we were just talking about this over breakfast. Here's a MWE:

import Mathlib.CategoryTheory.GlueData

open CategoryTheory Limits

namespace CategoryTheory.GlueData

variable {C : Type u₁} [Category C] {C' : Type u₂} [Category C']
  (D : GlueData C) (F : C ⥤ C') [H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F]
  [HasMulticoequalizer (diagram D)] [PreservesColimit (MultispanIndex.multispan (diagram D)) F]

attribute [local instance] hasColimit_multispan_comp

attribute [local instance] hasColimit_mapGlueData_diagram

/-- a docstring -/
noncomputable def gluedIso' : F.obj D.glued ≅ (D.mapGlueData F).glued :=
  have : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))) := inferInstance
  preservesColimitIso F D.diagram.multispan ≪≫ Limits.HasColimit.isoOfNatIso (D.diagramIso F)

#lint
/- The `unusedHavesSuffices` linter reports:
THE FOLLOWING DECLARATIONS HAVE INEFFECTUAL TERM MODE HAVE/SUFFICES BLOCKS.
...
#check @gluedIso' /- unnecessary have this : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F)))
-/

The problem goes away with haveI.

[Kevin Buzzard]

If you instead write have foo : HasColimit... then a second linter complains: unused variable foo [linter.unusedVariables]. But if you comment it out the declaration breaks.

[Johan Commelin]

wicked :stuck_out_tongue_wink:

[Gabriel Ebner]

Kyle Miller said:

Asymptotically the let_fun seems like it's better, since if you keep nesting it you'll otherwise have exponentially many 2's. Whether this matters practice for elaboration I have no idea.

Don't try to read too much into the term size. Too much fun makes the performance tank. For example, if you traverse a let-fun you need to create a free variable (this is expensive) and then substitute it for the bound variable (this is even more expensive). Meanwhile, pretty much all operations use caches that make expressions behave daglike in practice. I would recommend to always use haveI/letI over have/let in theorem statements, unless it severely hurts readability (of the goal state).

[Gabriel Ebner]

And if you actually need to construct exponentially-sized terms, I think it's best to introduce a definition for it (where you can control unfolding). Like 2^n.