Qq matching on -> error: cannot quote level mvar

Stream: lean4

[Bob Rubbens]

Hi all, another metaprogramming question.

I've been succesfully using Qq, and it's been very nice. However somehow I can't get it to pattern match on an implication. Here's an example:

import Lean
import Qq

open Lean Elab Tactic Term Meta PrettyPrinter Qq

def simplifyLocalDecl (g : MVarId) (localDecl : LocalDecl): TacticM (Option (List MVarId)) := do
  let h := localDecl.fvarId
  let xx ← inferTypeQ (.fvar h)
  let res ← match xx with
  | ⟨0, ~q(_ → _), _⟩ => return some []
  | _ => return none

I get an error on the match keyword: cannot quote level mvar ?u.817. For the and, or, and not operators this worked just fine.

As a side question, is there some documentation somewhere on using Qq? The readme in the quote4 repo is pretty clear, but it says pattern matching doesn't work yet, yet it clearly does for me, so I'm guessing the readme is out of date a bit?

Edit: Writing it with a universal quantifier gives the same error: | ⟨0, ~q(∀ t, $b t), _⟩ => return none. Pretty sure I'm not reading some fine print somewhere again...

[Bob Rubbens]

I worked around it for now by just using plain pattern matching:

    | .forallE _ binderType body _ =>
      let binderTypeType ← inferType binderType
      let anteProp ← isDefEq binderTypeType q(Prop)
      let bodyType ← inferType body
      let conseProp ← isDefEq bodyType q(Prop)
      if anteProp ∧ conseProp
        then return some (← localRewrite g localDecl ``imp_or)
        else return none

I was rewriting -> to or expressions. I'm guessing dependent arrows are a fundamental thing in lean/its kernel so that might make pattern matching on it difficult?

[Eric Wieser]

Qq pattern matching on functions is pretty difficult right now, @Yaël Dillies has been struggling with this too

[Bob Rubbens]

Okay, then if my workaround isn't too silly I'm happy :smiley:

[Notification Bot]

Bob Rubbens has marked this topic as resolved.

[Eric Wieser]

Here's a mwe in case anyone wants to fiddle around with it:

import Lean
import Qq

open Lean Elab Tactic Term Meta PrettyPrinter Qq

def isImp (p : Q(Prop)) : MetaM Bool := do
  let res ← match p with
  | ~q((_ : Prop) → _) => return true
  | _ => return false

#eval isImp q(True → True) -- wrong answer!

[Eric Wieser]

Oh, this works!

def isImp (p : Q(Prop)) : MetaM <| Option (Q(Prop) × Q(Prop)) := do
  match p with
  | ~q((($P) : Prop) → $Q) => do
    return some (P, Q)
  | _ =>
    return none

#eval isImp q(True → False)
#eval isImp q(True ∧ False)

[Eric Wieser]

Those ()s around $P are the trick

[Yaël Dillies]

Stealing it immediately for my positivity extensions

[Yaël Dillies]

Wait, I have one more complication in my use case: not all universes are Prop

[Yaël Dillies]

How do I get the universes to work out? If I want to destructure π : Sort w into α → β where α : Sort u and β : Sort v I somehow need to unify w with imax u v.

[Eric Wieser]

I guess you'll need ~q((($P) : Sort u) → (($Q) : Sort v))

[Eric Wieser]

Is Type ok for you?

[Eric Wieser]

Yaël Dillies said:

How do I get the universes to work out? If I want to destructure π : Sort w into α → β where α : Sort u and β : Sort v I somehow need to unify w with imax u v.

This was discussed already in another thread of yours, please link it here when you find it!

[Yaël Dillies]

Eric Wieser said:

Is Type ok for you?

Yes in fact I'm only dealing with Type _ in my use case

[Eric Wieser]

I think imax would have caused you a lot more pain than max

[Yaël Dillies]

Eric Wieser said:

I guess you'll need ~q((($P) : Sort u) → (($Q) : Sort v))

But how do I get u and v?

[Yaël Dillies]

They don't exist in my context before the match

[Eric Wieser]

You create them as metavariables

[Eric Wieser]

... as discussed in the previous thread you made somewhere

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Yaël Dillies]

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Positivity.20extension.20for.20Finset.2Ecard ?

[Eric Wieser]

Yes, this message

[Yaël Dillies]

Something is wrong here

import Lean
import Qq

open Lean Elab Tactic Term Meta PrettyPrinter Qq

def isFun {u : Level} (π : Q(Type $u)) :
    MetaM (Option (Σ (v w : Level),  Q(Type v) × Q(Type w))) := do
  let v ← mkFreshLevelMVar
  let w ← mkFreshLevelMVar
  let _ : u =QL max v w := ⟨⟩
  match π with
  | ~q((($α) : Type v) → (($β) : Type w)) => return .some ⟨v, w, q($α), q($β)⟩
  | _ => return none

#eval isFun q(Unit → Unit) -- none

[Eric Wieser]

Yeah, I think the universe variables don't unify properly

[Eric Wieser]

You could #print the resulting isFun, and reduce the failing meta code to a ~q-free mwe

[Yaël Dillies]

This seems to work?

def isFun {u : Level} (π : Q(Sort $u)) :
    MetaM (Option (Σ (v w : Level),  Q(Sort v) × Q(Sort w))) := do
  match ← whnfR π with
  | Expr.forallE _ α β _ =>
    let .sort v ← inferType α | return none
    let .sort w ← inferType β | return none
    return .some ⟨v, w, α, β⟩
  | _ => return none

#eval isFun q(Unit → Unit)
/-
some ⟨Lean.Level.succ
   (Lean.Level.zero), ⟨Lean.Level.succ (Lean.Level.zero),
(Lean.Expr.const `Unit [], Lean.Expr.const `Unit [])⟩⟩
-/

[Eric Wieser]

Oh, I know it's possible to do without Qq; my question is why Qq's generated code doesn't work

[Eric Wieser]

(that approach doesn't work if π has mdata or is a metavariable though)

[Eric Wieser]

My guess is that the issue is some kind of max u1 v1 =?= max u2 v2 unification failure.

[Yaël Dillies]

Edited to add mdata handling

[Eric Wieser]

I think whnfR is probably the better approach

[Yaël Dillies]

Eric Wieser said:

You could #print the resulting isFun, and reduce the failing meta code to a ~q-free mwe

Am I supposed to do that from the raw expression?

[Eric Wieser]

Hmm, the version I had earlier printed without raw expressions...

[Eric Wieser]

Using return .some ⟨v, w, α, β⟩ instead of ⟨v, w, q($α), q($β)⟩ fixes the printer

[Eric Wieser]

Replacing withNewMCtxDepth _ false with withNewMCtxDepth _ true seems to fix it

[Patrick Massot]

Yaël and Eric, it would be really nice to write Qq documentation with everything you understood.

[Yaël Dillies]

I was contemplating doing that, actually

[Yaël Dillies]

I have already spotted some existing docstrings that are confusing at best

[Yaël Dillies]

It's quite funny reading my messages from a few months ago. I have definitely learned things! but not enough apparently :sad:

[Yaël Dillies]

Okay, so fixing the Qq version and simplifying it, I get

import Lean
import Qq

open Lean Elab Tactic Term Meta PrettyPrinter Qq

def isFun {u : Level} (π : Q(Type $u)) : MetaM (Option (Σ v w : Level, Q(Type v) × Q(Type w))) := do
  let v ← mkFreshLevelMVar
  let w ← mkFreshLevelMVar
  withNewMCtxDepth
    (do
      let α ← mkFreshExprMVar (some (.sort (.succ v)))
      let β ← mkFreshExprMVar (some (.sort (.succ w)))
      match ← withReducible (isDefEq (.forallE .anonymous α β .default) π) with
      | true => pure (some ⟨v, w, ← instantiateMVars α, ← instantiateMVars β⟩)
      | false => pure none)
    true

#eval isFun q(Unit → Nat)

[Yaël Dillies]

It looks pretty similar to the version I came up with by hand, but looks a bit more robust.

[Eric Wieser]

Patrick Massot said:

Yaël and Eric, it would be really nice to write Qq documentation with everything you understood.

All my writing energy is currently directed at a thesis, but this is high on my todo list. Do you think it has a better home in Qq itself, or in the metaprogramming book?

[Eric Wieser]

Presumably withNewMCtxDepth false is fine if the level metavariables are created inside the context

[Eric Wieser]

I think probably Qq is doing the right thing by refusing to unify universe metavariables that it doesn't own; but the problem is that unlike expression metavariables, it doesn't provide the user with any way to pass over ownership

[Eric Wieser]

Perhaps what's missing is a ~ql(max $u $v) match clause

[Eric Wieser]

As a reminder, Qq already has ql:

variable {u v : Level}
#check ql(max u v)

[Yaël Dillies]

Here's a MWE, with all the extra typeclasses stripped away:

import Mathlib.Tactic.Positivity.Core

section IsFun
open Lean Elab Tactic Term Meta PrettyPrinter Qq

def isFun {u : Level} (π : Q(Type $u)) : MetaM (Option (Σ v w : Level, Q(Type v) × Q(Type w))) := do
  let v ← mkFreshLevelMVar
  let w ← mkFreshLevelMVar
  withNewMCtxDepth
    (do
      let α ← mkFreshExprMVar (some (.sort (.succ v)))
      let β ← mkFreshExprMVar (some (.sort (.succ w)))
      match ← withReducible (isDefEq (.forallE .anonymous α β .default) π) with
      | true => pure (some ⟨v, w, ← instantiateMVars α, ← instantiateMVars β⟩)
      | false => pure none)
    true

end IsFun

section Defs
variable {α β : Type*}

def conv (f g : α → β) : α → β := sorry

variable [OrderedAddCommMonoid β] {f g : α → β}

lemma conv_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ conv f g := sorry
lemma conv_nonneg_of_pos_of_nonneg (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ conv f g := conv_nonneg hf.le hg
lemma conv_nonneg_of_nonneg_of_pos (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ conv f g := conv_nonneg hf hg.le
lemma conv_pos (hf : 0 < f) (hg : 0 < g) : 0 < conv f g := sorry

end Defs

namespace Mathlib.Meta.Positivity
open Lean Meta Qq

@[positivity conv _ _] def evalConv : PositivityExt where eval {u π} zπ pπ e := do
  let .some ⟨v, w, ~q($α), ~q($β)⟩ ← isFun π | throwError "not `conv`"
  have : u =QL max v w := ⟨⟩
  have : $π =Q ($α → $β) := ⟨⟩
  match e with
/-
don't know how to synthesize placeholder
context:
case m
«$$v»«$$w»: Level
$$x✝¹$$x✝: Expr × Bool
⊢ Sort ?u.6232
-/
  | ~q(@conv $α $β ($f : Q($α → $β)) ($g : Q($α → $β))) => _
  | _ => throwError "not `conv`"

end Mathlib.Meta.Positivity

section Examples
variable {α β : Type*} [OrderedAddCommMonoid β] {f g : α → β}

-- failed to prove positivity/nonnegativity/nonzeroness
example (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ conv f g := by positivity
example (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ conv f g := by positivity
example (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ conv f g := by positivity
example (hf : 0 < f) (hg : 0 < g) : 0 < conv f g := by positivity

end Examples

[Yaël Dillies]

I have no idea where this error is coming from

[Eric Wieser]

This compiles:

@[positivity conv _ _] def evalConv : PositivityExt where eval {u π} zπ pπ e := do
  let .some ⟨v, w, ~q($α), ~q($β)⟩ ← isFun π | throwError "not `conv`"
  have : u =QL max v w := ⟨⟩
  have : $π =Q ($α → $β) := ⟨⟩
  match q($e) with
  | ~q(@conv.{w,v} _ _ $f $g) => sorry
  | _ => throwError "not `conv`"

[Jannis Limperg]

(FYI, you can write withNewMCtxDepth (allowLevelAssigments := true) do ..., which reads slightly nicer.)

[Yaël Dillies]

In fact,

def evalConv : PositivityExt where eval {u π} zπ pπ e := do
  let .some ⟨v, w, ~q($α), ~q($β)⟩ ← isFun π | throwError "not `conv`"
  have : u =QL max v w := ⟨⟩
  have : $π =Q ($α → $β) := ⟨⟩
  match q($e) with
  | ~q(conv $f $g) => sorry
  | _ => throwError "not `conv`"

works too

[Yaël Dillies]

Why is q($e) not behaving the same as e?

[Yaël Dillies]

Yaël Dillies said:

In fact, [...] works too

No it doesn't, the Qq ascriptions are wrong because new types are introduced.

[Yaël Dillies]

New MWE, exhibiting a different error:

def evalConv : PositivityExt where eval {u π} zπ pπ e := do
  let .some ⟨v, w, ~q($α), ~q($β)⟩ ← isFun π | throwError "not `conv`"
  have : u =QL max v w := ⟨⟩
  have : $π =Q ($α → $β) := ⟨⟩
  match q($e) with
  | ~q(@conv $α $β $f $g) => do
    let _ ← synthInstanceQ q(OrderedAddCommMonoid $β)
    let _ ← synthInstanceQ q(PartialOrder $β)
    match ← core q(inferInstance) q(inferInstance) f with
    | .positive rf => do
      match ← core q(inferInstance) q(inferInstance) g with
      | .positive rg => do
        let rf : Q(0 < $f) := rf
        let rg : Q(0 < $g) := rg
/-
application type mismatch
  conv_pos «$rf»
argument
  «$rf»
has type
  @OfNat.ofNat («$α» → «$β») 0
      (@Zero.toOfNat0 («$α» → «$β») (@Pi.instZero «$α» (fun a ↦ «$β») fun i ↦ AddMonoid.toZero)) <
    «$f» : Prop
but is expected to have type
  @OfNat.ofNat («$α» → «$β») 0
      (@Zero.toOfNat0 («$α» → «$β») (@Pi.instZero «$α» (fun a ↦ «$β») fun i ↦ AddMonoid.toZero)) <
    ?m.21991 : Prop
-/
        return .positive q(@conv_pos $α $β _ _ _ $rf $rg)
      | .nonnegative rg => sorry
      | _ => return .none
    | .nonnegative rf => sorry
    | _ => return .none
  | _ => throwError "not `conv`"

[Yaël Dillies]

The full MWE is available at https://github.com/YaelDillies/LeanAPAP/blob/conv_positivity/LeanAPAP/MWE.lean

[Patrick Massot]

Eric Wieser said:

Patrick Massot said:

Yaël and Eric, it would be really nice to write Qq documentation with everything you understood.

All my writing energy is currently directed at a thesis, but this is high on my todo list. Do you think it has a better home in Qq itself, or in the metaprogramming book?

I would aim for an independent document but this is really up to you.

[Yaël Dillies]

Yaël Dillies said:

New MWE, exhibiting a different error: ...

I would still use some wisdom on this one :grimacing:

[Eric Wieser]

I've added some documentation in Qq itself in leanprover-community/quote4#47

[Eric Wieser]

This is definitely not reaching as far as the stuff in the thread above, but does at least mean that hovering over ~q gives anything at all.