Replacing the result

Stream: metaprogramming / tactics

[Jannis Limperg]

Is there a way to set the result of a tactic (i.e. the term that the tactic produces to inhabited the target type)? We can inspect the result with tactic.result, but is there a way to replace this term?

Use case: I want to clean up the result term produced by one of my tactics, to see if this fixes a strange interaction with the equation compiler.

[Patrick Massot]

docs#tactic.interactive.show_term?

[Rob Lewis]

More low-level: you probably want to get the goal metavariable before calling your tactic, and then call instantiate_mvars on it after.

[Rob Lewis]

Patrick's suggestion is better if you're in interactive mode/want a pretty-printed statement.

[Jannis Limperg]

This allows me to view the result term, but I want to replace it from within a tactic, telling Lean, "use this result term regardless of what happened earlier."

Actually, maybe I can execute a tactic, get the produced result, roll back the tactic and 'refine' with the cleaned-up result term.

[Rob Lewis]

Yep. docs#tactic.retrieve and variants can help with rolling back. But this does sound slightly convoluted...

[Gabriel Ebner]

You might want to take inspiration from docs#tactic.dsimp_result

[Rob Lewis]

Oh, nice, I didn't know about docs#tactic.intercept_result

[Kevin Buzzard]

Be careful!

[Kevin Buzzard]

(that was a slightly unnerving quote from the docstring, by the way!)

[Rob Lewis]

Hmm, is the implementation of intercept_result right in the case where a metavariable appears in the goal?

[Rob Lewis]

It copies the goal metavariables for some reason, but if there are metavariables in their types those could still get assigned.

[Jannis Limperg]

Yes, that's exactly what I was looking for. Thanks all! Of course this is highly unsafe, but I promise to be careful. ;)

[Rob Lewis]

(I'm just glancing at it on GitHub, didn't look carefully at what it's doing.)

[Patrick Massot]

That sounds like a very honest docstring.

[Rob Lewis]

I like the ones at docs#module_info.resolve_module_name too

[Patrick Massot]

Oh, I never noticed the color choice for meta!

[Rob Lewis]

It's for constant/axiom

[Patrick Massot]

I see, this makes even more sense.

[Pedro Minicz]

From docs#tactic.intercept_result:

  -- and assign to the original goals.
  -- (We have to use `assign` here, as `unify` and `exact` are apparently
  -- unreliable about which way they do the assignment!)
  unsafe.type_context.run $ unsafe.type_context.assign g g''),

Since the author used "apparently," maybe someone with a deep understanding of unify could rewrite this tactic making is safer.

[Rob Lewis]

Maybe if @Jannis Limperg runs into issues with it, but I don't think this is any kind of priority.

[Jannis Limperg]

No issues in my use case, though that was just some simple debugging.