Matching generic Goals with Qq

Stream: metaprogramming / tactics

[Francisco Lima]

I am writing a generic theorem solver, like aesop, for a research project, in the process I need to match the type of the main goal to get certain information, through another discussion, in there @Aaron Liu  mentioned Qq, from there I started using it

Now I am in the process of applying diferent basic operations

so I have this piece of code

let ⟨1, ~q(Prop), e⟩ ← inferTypeQ type
match e with
| ~q($a = $b) => ...
| ~q(True) => ...
| ~q(¬$a) => ...
| _ => ...

now I want to parse goals of the form α → β

but when added it says that the u level is 2 instead of 1, ok I make the selection happen on the match to make it more modular

like this:

match ← inferTypeQ type with
| ⟨1, ~q(Prop), ~q($a = $b)⟩ => ...
| ⟨1, ~q(Prop), ~q(True)⟩ => ...
| ⟨1, ~q(Prop), ~q(¬$a)⟩ => ...
| ⟨2, ~q(Type), ~q($a → $b)⟩ => ...
| _ => ...

but it says it cannot collapse the universe levels to a singular one big enough for everything.

Is there any better way to make the matching? Or am I missing something crucial that makes it that much easier?

[Eric Wieser]

Can you provide a #mwe?

[Francisco Lima]

For the working example

import Lean
import Qq

open Lean Elab Tactic Meta
open Qq

syntax (name := endSorry) "sorry?" : tactic

-- number and String are for tracking suggestions and intro names
partial def loop (n := 0) : TacticM (String)  :=
  withMainContext do
    let goal ← getMainGoal
    let type ← goal.getType
    let ⟨1, ~q(Prop), e⟩ ← inferTypeQ type | throwError "Don't know how to handle yet"
    match e with
    | ~q($a = $b) =>
      admitGoal goal
      return ""
    | ~q(True) =>
      admitGoal goal
      return ""
    | ~q(¬$a) =>
      admitGoal goal
      return ""
    | _ =>
      admitGoal goal
      return ""

elab_rules : tactic
  | `(tactic| sorry?) => do
    let ref ← getRef
    let raw ← loop
    -- let text := SuggestionText.string raw
    -- let suggestion : Suggestion := {suggestion := text}
    -- addSuggestion ref suggestion
    return

for the example with error simply change the body

partial def loop (n := 0) : TacticM (String) :=
  withMainContext do
    let goal ← getMainGoal
    let type ← goal.getType

    match ← inferTypeQ type with
    | ⟨1, ~q(Prop), ~q($a = $b)⟩ =>
      admitGoal goal
      return ""
    | ⟨1, ~q(Prop), ~q(True)⟩ =>
      admitGoal goal
      return ""
    | ⟨1, ~q(Prop), ~q(¬$a)⟩ =>
      admitGoal goal
      return ""
    | ⟨2, ~q(Type), ~q($a → $b)⟩ =>
      admitGoal goal
      return ""
    | _ =>
      admitGoal goal
      return ""

[Francisco Lima]

another thing, eventually loop will be recursive (as should be obvious) but at this point it is not yet

[Eric Wieser]

Unfortunately it's pretty hard to match on function types with Qq, because of the universes involved

[Eric Wieser]

If you're happy staying in universe 0, this works:

    match ← inferTypeQ type with
    | ⟨1, ~q(Prop), ~q($a = $b)⟩ => sorry
    | ⟨1, ~q(Prop), ~q(True)⟩ => sorry
    | ⟨1, ~q(Prop), ~q(¬$a)⟩ => sorry
    | ⟨2, ~q(Type), ~q((_ : ($a : Type)) → ($b : Type))⟩ => sorry
    | _ => sorry

[Francisco Lima]

It compiles but when using it fails

theorem a_true : α → True := by
  sorry?
  sorry?

this one falls into the default case and not the function type

[Eric Wieser]

Right, that's not Type -> Type

[Eric Wieser]

That's Type -> Prop

[Francisco Lima]

simply changing (_ : ($a : Type)) → ($b : Type) to (_ : ($a : Type)) → ($b : Prop) does not seem to work, at least on the Type universe

[Francisco Lima]

And also does not work on the Prop universe, though it parses at least

[Francisco Lima]

(_ : ($a : Prop)) → ($b : Prop) also parses but does not work for the matching

[Eric Wieser]

mwe?

[Francisco Lima]

open Lean Elab Tactic Meta
open Qq

syntax (name := endSorry) "sorry?" : tactic

partial def loop (n := 0) : TacticM (String)  :=
  withMainContext do
    let goal ← getMainGoal
    let type ← goal.getType
    match ← inferTypeQ type with
    | ⟨1, ~q(Prop), ~q($a = $b) ⟩ =>
      admitGoal goal
      Lean.logInfo "rfl"
      return ""
    | ⟨1, ~q(Prop), ~q(True) ⟩ =>
      admitGoal goal
      Lean.logInfo "apply True.intro"
      return ""
    | ⟨1, ~q(Prop), ~q((_ : ($a : Prop)) → ($b : Prop))⟩ =>
      admitGoal goal
      Lean.logInfo "lam Prop → Prop"
      return ""
    | ⟨1, ~q(Prop), ~q((_ : ($a : Type)) → ($b : Prop))⟩ =>
      admitGoal goal
      Lean.logInfo "lam Type → Prop"
      return ""
    | ⟨2, ~q(Type), ~q((_ : ($a : Type)) → ($b : Type))⟩ =>
      admitGoal goal
      Lean.logInfo "lam Type → Type"
      return ""
    | ⟨1, ~q(Prop), ~q(¬$a) ⟩ =>
      admitGoal goal
      Lean.logInfo "Not"
      return ""
    | ⟨1, ~q(Prop), a⟩ =>
      admitGoal goal
      Lean.logInfo "default"
      return ""

elab_rules : tactic
  | `(tactic| sorry?) => do
    let ref ← getRef
    let raw ← loop
    return

-- does not work
theorem a_true : α → True := by
  sorry?

-- works
theorem a_then_a {α : Prop} : α → α := by
  sorry?

-- does not work
theorem a_b_true : α → β → True := by
  sorry?

-- works
theorem a_b_then_a {α β : Prop} : α → β → α := by
  sorry?

-- works
theorem a_b_then_b {α β : Prop} : α → β → β := by
  sorry?

[Francisco Lima]

Francisco Lima said:

(_ : ($a : Prop)) → ($b : Prop) also parses but does not work for the matching

Correction, works for Prop -> Prop

[Eric Wieser]

The ones that do not work are not about Type, they're about Sort u

[Francisco Lima]

also these don't work, I suspect for the same reason

theorem a_b_then_a {α : Prop} : α → β → α := by
  sorry?

theorem a_b_then_b {β : Prop} : α → β → β := by
  sorry?

[Eric Wieser]

I recommend adding set_option autoImplicit false

[Eric Wieser]

Then the code that causing the trouble will be the bit you write, rather than the bit you don't write

[Eric Wieser]

But really the lesson here is that ~q matching is not useful for matching Expr.forallE

[Eric Wieser]

Where it excels is for matching nested Expr.apps

[Francisco Lima]

Do you know of any other way to match these? I can't even fathom how to march these or

theorem a_a : ∃ α, α  → True := by sorry
theorem a_b : ∀ α, α  → True := by sorry

[Mirek Olšák]

There always is a low-level way (possibly with some whnf, or instantiateMVars)

def Lean.Expr.matchArrow? (e : Expr): Option (Expr × Expr) :=
  match e with
  | .forallE _ a b _ =>
    if b.hasLooseBVars then none
    else (a, b)
  | _ => none

run_meta
  let t1 : Expr := q(∀ α : Type, α → True)
  let t2 : Expr := q(∃ β : Type, β → True)
  if t1.isForall then
    forallBoundedTelescope t1 (some 1) (fun fvars body => do
      logInfo m!"forall {fvars[0]!} : {body}"
      match body.matchArrow? with
      | some (a, b) => logInfo m!"From {a} to {b}"
      | _ => pure ()
    )
  match t2.app2? ``Exists with
  | some (_, p) => lambdaBoundedTelescope p 1 (fun fvars body => do
      logInfo m!"exists {fvars[0]!} : {body}"
      match body.matchArrow? with
      | some (a, b) => logInfo m!"From {a} to {b}"
      | _ => pure ()
    )
  | _ => logInfo "Not exists"

[Eric Wieser]

You can match the exists fairly easily with qq

[Francisco Lima]

Thanks @Mirek Olšák that works really well and solves most of the problems