Specializing function at unknown point (and univese issues)

Stream: metaprogramming / tactics

[Calle Sönne]

I have a term of type ∀ ..., η = θ, where the ... is an unknown amount of arguments. I want to specialize this function at a specific argument, but I don't know in general at what point this argument appears. However, I should be able to find it by analysing the equality η = θ. Here is my specific situation: the equality η = θ will be an equality of 2-morphisms in some bicategory B. This bicategory B will be an argument to the function, and I want to specialize B to the bicategory Cat. However, there may be multiple bicategories appearing as arguments to the function, so I have to find B by looking at the equality η = θ. Here is an example of a type for which I want to do this:

(∀ {B : Type u₁} [inst : Bicategory B] {C : Type u₂} [inst_1 : Bicategory C] (F : Pseudofunctor B C) {a b c d : B}
    (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    (F.mapComp f (g ≫ h)).hom ≫ F.map f ◁ (F.mapComp g h).hom =
      F.map₂ (α_ f g h).inv ≫
        (F.mapComp (f ≫ g) h).hom ≫ (F.mapComp f g).hom ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom)

In this case I want to specialize C to Cat(which is where the equality is taking place).

I have almost managed to do this, modulo some universe issues which I would like help with. I am also new to metaprogramming, so I am also happy to receive suggestions for completely different approaches to this problem.

To do this specialization I have been using forallMetaTelescope (and then I construct my new, specialized, term using mkLambdaFVars at the end). Say my original term was called e, then I write:

let (args, _, conclusion) ← forallMetaTelescope (← inferType e)

After this, I have successfully extracted the metavariable I want to specialize to Cat (I called it CAT) and assigned it Cat using Qq in the following way:

let u ← Meta.mkFreshLevelMVar
let v ← Meta.mkFreshLevelMVar
CAT.assign q(Cat.{v, u})

I also specialize the bicategory instance [Bicategory B] to Bicategory.{max v u, max v u} Cat.{v u}.

I then update the list of metavariables args to obtain args2. This seems to replace C with Cat, just like I wanted. It also seems to correctly replace occurrences of C in the other types that depend on C by Cat (such as F in the example above). However, it does not seem to do this for universes. This is my problem. So in the example above, F gets updated to have type Pseudofunctor B Cat, but Pseudofunctor B Cat still says it has type Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂). Here u₂, v₂, w₂ appear, and they are the old universe parameter for C and [Bicategory C]. How would I go about updating these types so that they get the correct universes (depending on the new universe metavariables u and v)?

[Jannis Limperg]

Instead of doing this specialisation by hand, can you apply the expression of the given type to the correct arguments (here (B := Cat))? Then you can infer the type of the partially applied expression. This should correctly specialise everything.

[Calle Sönne]

What function would allow me to do this? In general I do not know that the argument will be called B, but I guess I could maybe use forallMetaTelescope to find the index of the argument, and then maybe there is some function which applies the expression with the nth argument being Cat?

[Jannis Limperg]

I was going to say docs#Lean.Meta.mkAppOptM or docs#Lean.Meta.mkAppOptM', but both of these try to infer all instance arguments, which may or may not be a problem for you. It would be possible to make a variant that doesn't do this, and maybe someone has already done this in Batteries or Mathlib.

[Calle Sönne]

I am trying to make this work now (but I also think that I will run into the instance issue later), but I am still stuck with a similar universe issue as before.

Now I still use forallMetaTelescope, I get my list of (metavariable) arguments, instantiate C to Cat.{v, u}, and [Bicategory C] to Bicategory.{max v u, max v u} Cat.{v u}. Here I still define u, v as

let u ← Meta.mkFreshLevelMVar
let v ← Meta.mkFreshLevelMVar

Then I replace all arguments still containing metavariables with none, so I get a list of arguments [none, .., Cat, Category Cat, none, ..., none].

Then I run into the issue that mkAppOptM' complains that Cat does not have the right Type when I try to apply the above list to the function (because of universes).

In the example from the original post it expects Cat to have type Type u₂, but it has type Type ... where ... is some complicated expression involving the level metavariables u, v. Is there any way I can instantiate u, v so that this works (or specialize u₂ somehow)?

[Calle Sönne]

I guess one thing I don't quite understand is that when using forallMetaTelescope, it does not seem like the universes get turned into metavariables, so I am not sure how to deal with them.

[Jannis Limperg]

Could you make a branch with your code? Then I can take a closer look.

[Calle Sönne]

Thanks a lot! I have it on the branch tactic-toCat.

What I'm trying to do on that branch is to make an attribute which specializes a lemma as described above, then applies NatTrans.app to the equality and then simplifies it with some basic Cat lemmas. Everything is in Tactic/CategoryTheory/ToApp.lean, but I am testing the attribute in Tactic/CategoryTheory/TEST.lean (otherwise I am not sure how to get the exact right input). The function that I have been talking about above, and need help with, is to_appExpr. Also most of the code apart from to_appExpr is more or less copied from reassoc.

Let me know if you need to know anything else.

[Jannis Limperg]

I made some progress by replacing the theorem's original universe parameters with universe mvars. But now I need to stop procrastinating writing my paper. :sweat_smile:

[Calle Sönne]

Good luck with the paper, and thanks a lot already!!

[Jannis Limperg]

Thanks! I pushed a final commit just now that fixes a wrong refactoring.

[Calle Sönne]

Thanks a lot for the help again, I managed to get the attribute working now!

[Jannis Limperg]

Nice, very happy to hear that!