Matching compositions with Qq

Stream: mathlib4

[Adam Topaz]

Does anyone know of any examples of meta code which uses Qq to match compositions of morphisms in a category?
Ideally I want something of type Expr -> MetaM (Expr x Expr) which will split out f and g (as exprs) given f ≫ g as input.

[Scott Morrison]

I did this long long ago, but I'm sure I've lost the branch. :-(

[Adam Topaz]

In the meantime, I'm using

import Mathlib

open Lean Elab Meta Term Command Qq

open CategoryTheory

-- Given an expression of the composition `f ≫ g`, return `f` and `g`.
def Lean.Expr.matchCategoryStructComp (e : Expr) : MetaM (Expr × Expr) :=
  match e with
  | .app (.app (.app (.app (.app (.app (.app
      (.const ``CategoryStruct.comp [_v, _u]) _obj) _inst) _X) _Y) _Z) f) g =>
      return (f, g)
  | _ => failure

elab "foo" t:term : command => Elab.Command.runTermElabM fun _ => do
  let e ← withSynthesize <| Elab.Term.elabTerm t none
  let e ← instantiateMVars e
  let (f,g) ← e.matchCategoryStructComp
  logInfo m!"{f}, {g}"

variable (C : Type*) [Category C] (X Y Z : C) (f : X ⟶ Y) (g : Y ⟶ Z)

foo f ≫ g

I would love to see how to Qq can be used for this. Are there any other tricks I'm missing?

[Kyle Miller]

Here's a trick I've been meaning to contribute eventually:

import Mathlib

open Lean Elab Meta Term Command Qq

open CategoryTheory

@[inherit_doc mkAppN]
macro_rules
  | `(mkAppN $f #[$xs,*]) =>(xs.getElems.foldlM (fun x e => `(Expr.app $x $e)) f : MacroM Term)

-- Given an expression of the composition `f ≫ g`, return `f` and `g`.
def Lean.Expr.matchCategoryStructComp (e : Expr) : MetaM (Expr × Expr) :=
  match e with
  | mkAppN (.const ``CategoryStruct.comp [_v, _u]) #[_obj, _inst, _X, _Y, _Z, f, g] =>
      return (f, g)
  | _ => failure

elab "foo" t:term : command => Elab.Command.runTermElabM fun _ => do
  let e ← withSynthesize <| Elab.Term.elabTerm t none
  let e ← instantiateMVars e
  let (f,g) ← e.matchCategoryStructComp
  logInfo m!"{f}, {g}"

variable (C : Type*) [Category C] (X Y Z : C) (f : X ⟶ Y) (g : Y ⟶ Z)

foo f ≫ g

This way mkAppN is both a function and a pattern (so long as the pattern uses an explicit array).

[Kyle Miller]

Without that trick, you can also do

def Lean.Expr.matchCategoryStructComp (e : Expr) : MetaM (Expr × Expr) :=
  match e.getAppFnArgs with
  | (``CategoryStruct.comp, #[_obj, _inst, _X, _Y, _Z, f, g]) =>
      return (f, g)
  | _ => failure

[Adam Topaz]

Thanks Kyle! That is indeed a nice trick. And I should have remembered about getAppFnArgs as I’ve used it in the past.

[Eric Wieser]

Here's the Qq version:

def Lean.Expr.matchCategoryStructComp (e : Expr) : MetaM (Expr × Expr) := do
  let ⟨Level.succ _,
    ~q(@Quiver.Hom _ (@CategoryStruct.toQuiver $C $instCat) $X $Y),
    ~q(@CategoryStruct.comp _ _ _ $Y _ $f $g)⟩ ← inferTypeQ e | failure
  return (f, g)

[Eric Wieser]

inferTypeQ is pretty much always the Qq tool you need if you started with an Expr, though unfortunately the match syntax fights you every step of the way

[Adam Topaz]

Thanks @Eric Wieser . Yes, that works, but do you know of any way to do this without every typing the character @? Ideally I would like to just use the category theoretic notation \hom and \gg

[Eric Wieser]

You'd need to somehow turn on the "turn instance arguments into metavariables" flag, which I don't remember the spelling of

[Eric Wieser]

We have that for apply, right?

[Adam Topaz]

oh maybe.

[Adam Topaz]

let me try something out

[Eric Wieser]

I think Qq does need fixing here so that what you want to write just works

[Adam Topaz]

I mean, I want to be able to write

def Lean.Expr.matchCategoryStructComp' (e : Expr) : MetaM (Expr × Expr) :=
  match e with
    | ~q($f ≫ $g) => return (f,g)
    | _ => failure

[Adam Topaz]

But maybe that's too optimistic

[Eric Wieser]

I think you should still be forced to write inferTypeQ, but you should be allowed to put underscores almost everywhere and drop all the @s

[Adam Topaz]

This works, but it's quite verbose:

def Lean.Expr.matchCategoryStructComp (e : Expr) : MetaM (Expr × Expr) := do
  let u ← mkFreshLevelMVar
  let v ← mkFreshLevelMVar
  let C : Q(Type u) ← mkFreshExprMVarQ q(Type u)
  let _inst : Q(Category.{v} $C) ← mkFreshExprMVarQ q(Category.{v} $C)
  let X : Q($C) ← mkFreshExprMVarQ q($C)
  let Y : Q($C) ← mkFreshExprMVarQ q($C)
  let Z : Q($C) ← mkFreshExprMVarQ q($C)
  let f : Q($X ⟶ $Y) ← mkFreshExprMVarQ q($X ⟶ $Y)
  let g : Q($Y ⟶ $Z) ← mkFreshExprMVarQ q($Y ⟶ $Z)
  let _h ← assertDefEqQ q($f ≫ $g) e
  return (f,g)

elab "foo" t:term : command => Elab.Command.runTermElabM fun _ => do
  let e ← withSynthesize <| Elab.Term.elabTerm t none
  let e ← instantiateMVars e
  let (f,g) ← e.matchCategoryStructComp
  logInfo m!"{f}, {g}"

variable (C : Type*) [Category C] (X Y Z : C) (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ Z)

foo f ≫ g

[Adam Topaz]

and also the infoview craps out near the let _h line.

[Eric Wieser]

Eric Wieser said:

We have that for apply, right?

Do you remember the spelling of this "turn TC into subgoals" version of apply?

[Adam Topaz]

No, I don't

[Eric Wieser]

Do you have any memory of something like it existing, or am I imagining?

[Adam Topaz]

It existed in Lean3 for sure as apply_with ... { instances := false }, but I've never used something similar in Lean4.

[Adam Topaz]

Aha I think it's apply (config := { allowSynthFailures := true }).

[Adam Topaz]

And it looks like this is just part of apply itself now: https://github.com/leanprover-community/mathlib4/blob/52199f53d887e390b8433f0866c1bad71d571357//Mathlib/Tactic/ApplyWith.lean#L7-L13

[Eric Wieser]

I was hoping this would lead to some kind of no_synth% foo x y elaborator that would just work out of the box with Qq, but I don't see it

[Adam Topaz]

Oh that’s a good idea though

[Eric Wieser]

I certainly think that the current "failed to synthesize instance" behavior of Qq is a good thing, just not all the time

[Eric Wieser]

E.g. if I'm matching nat addition, I probably want it to be defeq to the real instance

[Adam Topaz]

Adam Topaz said:

and also the infoview craps out near the let _h line.

This error is strange.... does anyone understand why this happens? I can't find any way around it.

[Adam Topaz]

Error updating: Error fetching goals: Rpc error: InternalError: failed. Try again.

[Scott Morrison]

@Kyle Miller, could we please have your macro trick PR'd? It is life changing. :-) I would love it in Std or even Lean.

[Adam Topaz]

I’ll second that!