Bad interaction of Qq with grind

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

While writing a tactic that quotes proofs produced by grind, I came across a nasty interaction with quote4. Here is what happens:

1. A | ~q(..) pattern match expands into auxiliary code. The code defines a tuple that packages together some data and a flag for whether the pattern matched.
2. This tuple persists (as an inaccessible variable) in the local context in which q(by grind) is used to produce a proof term.
3. grind picks up the tuple and matches on it, resulting in a huge and inefficient proof term (the tuple is completely useless for actually proving the goal).

Here is an example:

import Lean
import Qq

open Qq

axiom P : Nat → Prop

def abc (n : Q(Nat)) (pf : Q(P $n)) : Lean.MetaM Q(P $n) := do
  match pf with
  | ~q(_) => return q(by grind) -- q(abc._proof_1 ..)
  | _ => return q($pf)

/- theorem abc._proof_1 :
    ∀ («$n» : Nat) («$x» : Lean.Expr × Bool), P «$n» → P «$n» :=
  fun «$n» «$x» «$x_1» => Prod.casesOn «$x» .. -/
#print abc._proof_1

One possible fix is to manually clear $x_1, but that's quite clearly fragile and suboptimal. I would be grateful for suggestions on how to properly fix this.

• Is this a bug in Qq which should have hidden this variable better (maybe using some of the 'implementation detail' flags)?
• Is it a bug in grind which destructures garbage auxiliary data?

[Kim Morrison]

This should hopefully have been alleviated by lean4#9686

[Kim Morrison]

Oops, sorry, not yet: someone will need to modify quote4 to actually mark its auxiliary hypotheses as isImplementationDetail. Any takers?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Done in quote4#95. I think that's it for the Qq fix, but the core match elaborator doesn't always respect the convention that __x means an impl detail var:

example : True :=
  match 1 with
  | __x => sorry /- ⊢ True -/

example : True :=
  match 1, 2 with
  | __x, _ => sorry /- __x x✝ : Nat ⊢ True-/

I guess this has to be fixed in Lean.

[Eric Wieser]

Where is that convention established?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Sorry, I meant 'implDetail var', not 'inaccessible'. But I guess in docs#Lean.Elab.Term.kindOfBinderName.

[Kyle Miller]

match seems to use withLocalDecl to add pattern variables to the local context in withPatternVars, and withLocalDecl respects __, so maybe there's some other local context transformation that causes it to forget? Or maybe the name of the local variable is temporarily something synthetic somehow?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I don't think withLocalDecl respects that, though; it just takes a LocalDeclKind argument which defaults to .default. Maybe withPatternVars should be using kindOfBinderName? UPDATE: Hm no, that doesn't do it.

[Kyle Miller]

Oh, sorry, I misremembered, you are correct. The kindOfBinderName logic is in the binder elaboration.

I'm not sure why using that logic in withPatternVars wouldn't work, that's weird. I don't know much about the structure of the match elaborator though.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Aha, it's docs#Lean.Elab.Term.ToDepElimPattern.main.unpack.