## Stream: metaprogramming / tactics

### Topic: Replacing the result

#### Jannis Limperg (Sep 28 2020 at 14:46):

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.

#### Rob Lewis (Sep 28 2020 at 14:52):

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 (Sep 28 2020 at 14:53):

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

#### Jannis Limperg (Sep 28 2020 at 14:55):

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 (Sep 28 2020 at 14:58):

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

#### Gabriel Ebner (Sep 28 2020 at 14:59):

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

#### Rob Lewis (Sep 28 2020 at 15:01):

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

Be careful!

#### Kevin Buzzard (Sep 28 2020 at 15:02):

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

#### Rob Lewis (Sep 28 2020 at 15:03):

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

#### Rob Lewis (Sep 28 2020 at 15:04):

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

#### Jannis Limperg (Sep 28 2020 at 15:04):

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 (Sep 28 2020 at 15:04):

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

#### Patrick Massot (Sep 28 2020 at 15:05):

That sounds like a very honest docstring.

#### Rob Lewis (Sep 28 2020 at 15:06):

I like the ones at docs#module_info.resolve_module_name too

#### Patrick Massot (Sep 28 2020 at 15:08):

Oh, I never noticed the color choice for meta!

#### Rob Lewis (Sep 28 2020 at 15:08):

It's for constant/axiom

#### Patrick Massot (Sep 28 2020 at 15:09):

I see, this makes even more sense.

#### Pedro Minicz (Sep 28 2020 at 16:55):

  -- 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 (Sep 28 2020 at 17:03):

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

#### Jannis Limperg (Sep 28 2020 at 17:12):

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

Last updated: May 09 2021 at 23:10 UTC