Aesop RuleTac restricted to a particular pattern

Stream: metaprogramming / tactics

[Geoffrey Irving]

Is there a way to make an Aesop tactic rule that participates in DiscrTree filtering, so that it only costs significant time if the goal matches a certain pattern? As an example, is it possible to make decide fire exactly if the goal looks like a < b where a b : Interval (a computational interval analysis type)?

[Jannis Limperg]

Yes, see here for an example that fires on goals of the form _ = _ (up to reducible defeq). For your use case, I guess the annotation would be (index := [target (_ : Interval) < (_ : Interval)]).

[Geoffrey Irving]

Perfect, thank you!

[Jannis Limperg]

You can also do this as a simproc, which would probably be even more efficient. Here's a similar simproc I wrote to run decide on equations of string literals:

import Std.Tactic.OpenPrivate
import Std.Logic
import Lean

open Lean Lean.Meta

theorem eq_true_intro {a : Prop} (h : a) : a = True :=
  propext (iff_true_intro h)

theorem eq_false_intro {a : Prop} (h : ¬a) : a = False :=
  propext (iff_false_intro h)

open private preprocessPropToDecide in Lean.Elab.Tactic.evalDecide

/--
Attempt to decide the proposition `prop`. If `prop` is decidable, return a proof
of either `prop` or `¬ prop`.
-/
-- Inspired by Lean.Elab.Tactic.evalDecide
private def decide (prop : Expr) : MetaM (Option (Sum Expr Expr)) := do
  let (prop, _) ←
    try
      preprocessPropToDecide prop |>.run
    catch _ =>
      return none
  if let some decInst ← synthInstance? (mkConst ``Decidable |>.app prop) then
    let d := mkApp2 (.const ``Decidable.decide []) prop decInst
    let r ← whnfD d
    if r.isConstOf ``true then
      let rflPrf ← mkEqRefl (.const ``true [])
      let prf := mkApp3 (Lean.mkConst ``of_decide_eq_true) prop decInst rflPrf
      return some $ .inl prf
    else if r.isConstOf ``false then
      let rflPrf ← mkEqRefl (.const ``false [])
      let prf := mkApp3 (Lean.mkConst ``of_decide_eq_false) prop decInst rflPrf
      return some $ .inr prf
  return none


private def isStrLitEq (prop : Expr) : MetaM Bool :=
  withNewMCtxDepth do
    let stringType := .const ``String []
    let lhs ← mkFreshExprMVar (some stringType)
    let rhs ← mkFreshExprMVar (some stringType)
    let pat ← mkEq lhs rhs
    if ← isDefEq prop pat then
      let lhs ← whnfD lhs
      let rhs ← whnfD rhs
      return lhs.isStringLit && rhs.isStringLit
    else
      return false

open Lean Lean.Meta in
/--
Decide equality between string literals.
-/
simproc decideStrLitEq (@Eq String _ _) := λ prop => do
  if ← isStrLitEq prop then
    match ← decide prop with
    | .none => return .continue
    | .some (.inl propPrf) =>
      let prf := mkApp2 (.const ``eq_true_intro []) prop propPrf
      return .visit { expr := .const ``True [], proof? := prf }
    | .some (.inr notPropPrf) =>
      let prf := mkApp2 (.const ``eq_false_intro []) prop notPropPrf
      return .visit { expr := .const ``False [], proof? := prf }
  return .continue

[Jannis Limperg]

This might need a more recent Aesop than is currently in mathlib though.

[Geoffrey Irving]

Hmm, actually I may need something more than this, since I also want to produce nice error messages: if I fail to prove a < b using interval arithmetic I want to report what the intervals were, so that it's more obvious what went wrong.

Is there some way to report error messages from inside Aesop, if I run a tactic and I know its failure means the rest of the search has to fail? I think if I fail out of a RuleTac it'll bury any error message in the search, but possibly there is a way out of that?

[Jannis Limperg]

No, I'm afraid this is not currently supported. I'll note it down as a feature request.

[Geoffrey Irving]

I may just be doing something that is inappropriate for Aesop, and better for a custom DiscrTree thing.

[Jannis Limperg]

aesop#109

[Jannis Limperg]

I don't dislike this request. With another project, I've been exploring how Aesop could be used to build automation that doesn't necessarily close the goal but just makes some progress and then hands the reigns over to the user again. This feature fits nicely into that program.