Calling `finiteness` in meta code

Stream: metaprogramming / tactics

[Yury G. Kudryashov]

Recently, finiteness tactic (a wrapper around aesop) was added to Mathlib. How do I call it from meta code? #xy : I want to make positivity handle x¯¹ on ENNReal by proving x ≠ ∞ using finiteness.

[Kim Morrison]

finiteness is only written as a macro wrapper around aesop, so there is no MetaM or TacticM interface.

[Kim Morrison]

You can fake it using docs#Lean.Elab.runTactic.

[Kim Morrison]

e.g. as in Mathlib.Tactic.Bound:

-- Plain `bound` elaboration, with no hypotheses
elab_rules : tactic
  | `(tactic| bound) => do
    let tac ← `(tactic| aesop (rule_sets := [Bound, -default]) (config := Bound.boundConfig))
    liftMetaTactic fun g ↦ do return (← Lean.Elab.runTactic g tac.raw).1

[Yury G. Kudryashov]

Is there a *M interface to aesop?

[Kim Morrison]

docs#Aesop.search

[Kim Morrison]

and see docs#Aesop.evalAesop for how it prepares the arguments from the surface syntax.

[Yury G. Kudryashov]

I'll look into this over the weekend.

[Yaël Dillies]

Yury, I suggest you read how docs#Mathlib.Meta.Positivity.evalFinsetCard calls aesop through docs#Mathlib.Meta.proveFinsetNonempty

[Kyle Miller]

I think an easier interface is evalTactic. This can be written like

open Lean.Elab.Tactic

elab_rules : tactic
  | `(tactic| bound) => do
    let tac ← `(tactic| focus aesop (rule_sets := [Bound, -default]) (config := Bound.boundConfig))
    evalTactic tac

The added focus makes sure that aesop sees only the current goal. Not necessary here, but it can be useful when you write tactics this way.

[Patrick Massot]

Adding focus is a very good habit that will prevent extremely weird behavior for users.