Best way to write proof automation?

Stream: metaprogramming / tactics

[Qiancheng Fu]

I am currently learning Lean4 metaprogramming by translating the Certified Programming with Dependent Types chapter on proof by reflection. I was able to define an "obvious" tactic for proving tautologies in Prop. However, the code for closing the main goal required manually constructing an Expr denoting the final proof. Is this the correct approach in Lean or are there better ways to apply theorems and close goals in tactics?

inductive Reflect (P : Prop) : Bool -> Prop
  | reflectT : P -> Reflect P true
  | reflectF : ¬ P -> Reflect P false

theorem Reflect.iff {P b} : Reflect P b -> (P <-> b = true)
  ...

inductive BExp where
  | bool : Bool -> BExp
  | and  : BExp -> BExp -> BExp
  | or   : BExp -> BExp -> BExp
  | impl : BExp -> BExp -> BExp

def BExp.toExpr : BExp -> Expr
  ...

def BExp.reify : Expr -> MetaM BExp
  ...

def BExp.denote : BExp -> Prop
  ...

theorem BExp.spec (m : BExp) : Reflect m.denote m.eval
  ...

open Lean.Elab.Tactic in
elab "obvious" : tactic =>
  withMainContext do
    let goal <- getMainTarget
    let t := toExpr (<- BExp.reify goal)
    let iff <- mkAppM ``Reflect.iff #[<-mkAppM ``BExp.spec #[t]]
    let rfl <- mkEqRefl (.const ``true [])
    closeMainGoal `obvious (<- mkAppM ``Iff.mpr #[iff, rfl])


theorem ex1: True ∧ True  := by obvious
theorem ex2: True ∨ False := by obvious
theorem ex3: True -> True := by obvious

[Soundwave]

You're in good company:

@[builtin_tactic «exact»] def evalExact : Tactic := fun stx => do
  match stx with
  | `(tactic| exact $e) => closeMainGoalUsing `exact fun type _ => elabTermEnsuringType e type
  | _ => throwUnsupportedSyntax

You have Lean.Elab.Tactic.evalTactic to use tactic-style reasoning inside other tactics, which isn't uncommon for more complicated "solver" style tactics in order to simplify development and interoperate, but it all boils down to elaborating a proof term; emitting an explicit expr is perfectly normal.

[Siddhartha Gadgil]

You generally have to construct an expression, but it is common to use liftMetaTactic as a function taking the goal MVar to a list of MVars. In this case you assign the expression to the goal MVar and then return the empty list.

[Siddhartha Gadgil]

You generally have to construct an expression, but it is common to use liftMetaTactic as a function taking the goal MVar to a list of MVars. In this case you assign the expression to the goal MVar and then return the empty list.

[Kyle Miller]

@Qiancheng Fu I'd write this using the closeMainGoalUsing combinator:

open Lean.Elab.Tactic in
elab "obvious" : tactic =>
  closeMainGoalUsing `obvious fun goal _ => do
    let goal <- instantiateMVars goal
    let t := (<- BExp.reify goal).toExpr
    let iff <- mkAppM ``Reflect.iff #[<- mkAppM ``BExp.spec #[t]]
    let rfl <- mkEqRefl (.const ``true [])
    mkAppM ``Iff.mpr #[iff, rfl]

This makes sure that you're not introducing any new metavariables, and it does an occurs check before assignment. This is something liftMetaTactic-defined tactics tend to overlook...

Notice also the added instantiateMVars. You may consider changing that to (<- instantiateMVars goal).consumeTypeAnnotations if obvious is going to be used in contexts that prove an optParam/autoParam.

Core Lean uses these mkAppM-and-friends, though you'll find in downstream projects (like Mathlib) uses of the Qq library, which lets you write in a way that checks types of Exprs at compile time.

[Qiancheng Fu]

@Kyle Miller Thanks for the recommendations! I was originally really concerned with getting the types of mkAppM and Exprs to line up correctly in more complicated proofs. If Qq helps with that then I will definitely look into it.

[Kyle Miller]

At least mkAppM gives runtime errors, and at worst the kernel will catch any remaining problems, so you aren't going to end up with invalid theorems. It's good writing a comprehensive test suite!

[Qiancheng Fu]

Oh I wasn't worried about invalid theorems, I was worried about debugging tactics which is quite a pain in Coq.