Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Replacing the result


view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 28 2020 at 14:47):

docs#tactic.interactive.show_term?

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Sep 28 2020 at 14:53):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Gabriel Ebner (Sep 28 2020 at 14:59):

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

view this post on Zulip Rob Lewis (Sep 28 2020 at 15:01):

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

view this post on Zulip Kevin Buzzard (Sep 28 2020 at 15:02):

Be careful!

view this post on Zulip Kevin Buzzard (Sep 28 2020 at 15:02):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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. ;)

view this post on Zulip 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.)

view this post on Zulip Patrick Massot (Sep 28 2020 at 15:05):

That sounds like a very honest docstring.

view this post on Zulip Rob Lewis (Sep 28 2020 at 15:06):

I like the ones at docs#module_info.resolve_module_name too

view this post on Zulip Patrick Massot (Sep 28 2020 at 15:08):

Oh, I never noticed the color choice for meta!

view this post on Zulip Rob Lewis (Sep 28 2020 at 15:08):

It's for constant/axiom

view this post on Zulip Patrick Massot (Sep 28 2020 at 15:09):

I see, this makes even more sense.

view this post on Zulip Pedro Minicz (Sep 28 2020 at 16:55):

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.

view this post on Zulip 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.

view this post on Zulip 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