Calling aesop from a tactic to obtain an `Expr`

Stream: metaprogramming / tactics

[Anne Baanen]

I'm running into the limits of my understanding of tactics here. I'm in the following situation: in #10538 we have proveFinsetNonempty which attempts to generate a proof. I would like to see if we can do this instead via calling into aesop to do this. However, aesop works on the level of MVarIds (i.e. goals) and here the expected output is an Expr. So do I understand correctly that I have to do something like:

1.Create a new goal, obtain a MVarId

2. Make an Expr with the Prop we want to show
3. Set the goal type to be equal to the Expr we made
4. Call docs#Aesop.search with my parameters
5. Check that aesop doesn't return any unsolved subgoals
6. Get the term that solved the goal with docs#Lean.getExprMVarAssignment?

If this is correct, how do I do steps 1-3?

[Jannis Limperg]

I think this is correct and you should be able to use docs#Lean.Meta.mkFreshExprMVar to create the mvar. Note that this mvar inherits the current local context (as reported by getLCtx); if you want a particular local context, use docs#Lean.Meta.mkFreshExprMVarAt. The local context contains the hypotheses that are allowed to appear in your final Expr.

[Anne Baanen]

I see, thanks! We do want to use the current context for assumption purposes so mkFreshExprMVar sounds good. It returns an Expr, do I then use docs#Lean.Expr.mvarId! on it or is there something I should take into account?

[Anne Baanen]

It seems to work, thanks! One final question: what's the best way to pass rulesets into docs#Aesop.search, for example to do the equivalent of by aesop (rule_sets [-default, Finset.Nonempty])? Should I try to replicate what the frontend code does?

[Jannis Limperg]

Anne Baanen said:

I see, thanks! We do want to use the current context for assumption purposes so mkFreshExprMVar sounds good. It returns an Expr, do I then use docs#Lean.Expr.mvarId! on it or is there something I should take into account?

Yes, the returned Expr is always .mvar mvarId. The return type should really be changed imo, but it would be a big refactor.

[Anne Baanen]

I think I answered my question about rulesets, it would be something like:

  let rulesets ← Aesop.getDefaultRuleSetNames
  let ((mvar, rules), _) ← (Aesop.Frontend.TacticConfig.getRuleSet mvar
    { additionalRules := #[],
      erasedRules := #[],
      enabledRuleSets := (rulesets.erase `default).insert `Finset.Nonempty,
      options := {},
      simpConfig := {},
      simpConfigSyntax? := .none }).run
  let (remainingGoals, _) ← Aesop.search mvar (.some rules)

[Jannis Limperg]

Anne Baanen said:

It seems to work, thanks! One final question: what's the best way to pass rulesets into docs#Aesop.search, for example to do the equivalent of by aesop (rule_sets [-default, Finset.Nonempty])? Should I try to replicate what the frontend code does?

Oh, the handling of rule sets has changed quite a bit on master. Now it's docs#Aesop.Frontend.getGlobalRuleSets into docs#Aesop.mkLocalRuleSet. (There should be a function combining the two.)

[Anne Baanen]

Got it, so it should be:

  let rulesets ← Aesop.Frontend.getGlobalRuleSets #[`builtin, `Finset.Nonempty]
  let rules ← Aesop.mkLocalRuleSet rulesets { terminal := true, generateScript := false }

[Jannis Limperg]

I think so, yes.

[Anne Baanen]

Thanks so much for your quick answers! :D