lean 3 unification magic

Stream: general

[Kevin Buzzard]

I'm porting a file and a proof is_sheaf_for.is_amalgamation _ _ which works in Lean 3, is giving me errors on the underscores in lean 4. So I figured that if Lean 3 is solving the underscores with unification then they can't be too hard to solve! But assumption, library_search, and apply_instance don't solve them. What am I missing? Here's a mwe:

import category_theory.sites.cover_lifting

-- set-up
universes w v v₁ v₂ v₃ u u₁ u₂ u₃
noncomputable theory

open category_theory
open opposite
open category_theory.presieve.family_of_elements
open category_theory.presieve
open category_theory.limits

namespace category_theory

variables {C D : Type u} [category.{v} C] [category.{v} D]
variables {A : Type w} [category.{max u v} A] [has_limits A]
variables {J : grothendieck_topology C} {K : grothendieck_topology D}

namespace Ran_is_sheaf_of_cover_lifting
variables {G : C ⥤ D}  (hu : cover_lifting J K G) (ℱ : Sheaf J A)
variables {X : A} {U : D} {S : sieve U} (hS : S ∈ K U)

variables {x : S.arrows.family_of_elements ((Ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X))}
variables (hx : x.compatible)

-- the declaration
lemma get_section_is_amalgamation' (Y : structured_arrow (op U) G.op) :
  (pulledback_family ℱ S x Y).is_amalgamation (get_section hu ℱ hS hx Y) :=
is_sheaf_for.is_amalgamation _ _

end Ran_is_sheaf_of_cover_lifting
end category_theory

The challenge is to explicitly fill in the two underscores. If it helps, their types are

is_sheaf_for ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)) (functor_pullback G ⇑(sieve.pullback Y.hom.unop S))

and

⊢ (pulledback_family ℱ S x Y).compatible

[Yaël Dillies]

I assume you've already tried using (_) to force Lean 4 to find the instances via unification?

[Scott Morrison]

#print get_section_is_amalgamation'

[Scott Morrison]

It gives you a usable term, but with auto-generated names that won't be the same in Lean 4.

[Scott Morrison]

But possibly you can just find their names using whatsnew in on the definition of getSection.

[Kevin Buzzard]

Yaël Dillies said:

I assume you've already tried using (_) to force Lean 4 to find the instances via unification?

nice idea, but doesn't work.

[Kevin Buzzard]

Hmm. In Lean 3, #print prefix category_theory.Ran_is_sheaf_of_cover_lifting.get_section just after the def of get_section gives me category_theory.Ran_is_sheaf_of_cover_lifting.get_section._proof_n for 1<=n<=6, and in Lean 4 whatsnew in just before the def of getSection gives me CategoryTheory.RanIsSheafOfCoverLifting.getSection.proof_n for a meagre 1 <= n <= 2, so we're being short changed by Lean 4 here. The declaration in Lean 3 is

def get_section (Y : structured_arrow (op U) G.op) : X ⟶ ℱ.val.obj Y.right :=
begin
  let hom_sh := whisker_right ((Ran.adjunction A G.op).counit.app ℱ.val) (coyoneda.obj (op X)),
  have S' := (K.pullback_stable Y.hom.unop hS),
  have hs' := ((hx.pullback Y.3.unop).functor_pullback G).comp_presheaf_map hom_sh,
  exact (ℱ.2 X _ (hu.cover_lift S')).amalgamate _ hs'
end

and it seems to me that the lets and haves are being turned into hidden proofs in the namespace in lean 3 but not lean 4. I've filled in one of the holes by pasting the definition of hs' and hom_sh into the hole.

[Kevin Buzzard]

ha ha no it seems like Lean 3 is in fact just over-excited:

example : @category_theory.Ran_is_sheaf_of_cover_lifting.get_section._proof_1 =
  @category_theory.Ran_is_sheaf_of_cover_lifting.get_section._proof_2 := rfl

example : @category_theory.Ran_is_sheaf_of_cover_lifting.get_section._proof_1 =
  @category_theory.Ran_is_sheaf_of_cover_lifting.get_section._proof_3 := rfl

example : @category_theory.Ran_is_sheaf_of_cover_lifting.get_section._proof_1 =
  @category_theory.Ran_is_sheaf_of_cover_lifting.get_section._proof_4 := rfl

[Mauricio Collares]

Indeed, the two holes can be filled with ℱ.2 X _ (hu.cover_lift S') and hs' if the appropriate definitions are in context (i.e. copy and pasting the contents of def get_section and replacing amalgamate by is_amalgamation in the last line is a valid proof of get_section_is_amalgamation)

[Kevin Buzzard]

Thanks! We've got it working locally now. The remaining question is why lean 4 can't solve the goals via unification.

[Mauricio Collares]

It can solve them, it you replace the let and haves in amalgamate by letI and haveIs

[Mauricio Collares]

Curiously, if you print the Lean 3 term for amalgamate, you can see the haves are inlined but the let is not, and yet unification does not care.

[Kevin Buzzard]

Should I inline the let and haves in the declaration in Lean 4 then? I have no idea about this kind of internal representation stuff.

[Eric Wieser]

This is partly a mathport translation issue; tactichave in Lean3 is Lean4's haveI, but mathport translates it to lean4's have which is Lean3's term have.