Stream: Mtac2

Topic: Clarification on mrun

view this post on Zulip Michael Soegtrop (Aug 29 2020 at 15:27):

A question on mrun - just to make sure I understood it correctly: mrun can be called with an argument which:

In the first case, if the tactic needs anything from the context, this must be passed explicitly to the term called with mrun as arguments. Also in the first case the tactic must solve the goal completely.

In the second case the tactic may inspect the context and may solve the goal partially by creating new goals.

This are the only ways in which mrun can be used.

Is this about correct?

view this post on Zulip Beta Ziliani (Aug 29 2020 at 15:39):

In a M. t A tactic you can still inspect the context (the list of hypotheses). You don't get explicitly the goal, but that's the only difference in terms of inputs. When it comes to the solution, the difference is that the goals in the M.t tactic are shelved, while in the tactic one those returned in the list are unshelved.

view this post on Zulip Michael Soegtrop (Aug 29 2020 at 15:43):

I see. But I guess in case I have a M.t A tactic where A is parametric, I get the parameters of A, so i can still be quite flexible in the goal type and inspect it via the parameters.

How do I inspect hypothesis with a M.t A tactic?

view this post on Zulip Beta Ziliani (Aug 29 2020 at 19:16):

Not sure what you mean. Say t : forall {A}, M A and you need to prove P. When you do mrun t the following happens:

  1. A's meta-variable (created when typechecking t) is unified with P.
  2. t is executed, say obtaining value v.
  3. The current goal is proved using v.

In every of these steps, the current context (that is, P's dependencies) is part of the process. These can be obtain with the M.hyps construct.

view this post on Zulip Michael Soegtrop (Aug 30 2020 at 08:37):

Not sure what you mean. Say t : forall {A}, M A and you need to prove P. When you do mrun t the following happens:

  1. A's meta-variable (created when typechecking t) is unified with P.
  2. t is executed, say obtaining value v.
  3. The current goal is proved using v.

yes this is what I meant. As a response to your previous statement "You don't get explicitly the goal" I just wanted to say that one still can get complete information about the goal.

In every of these steps, the current context (that is, P's dependencies) is part of the process. These can be obtain with the M.hyps construct.

Thanks - I somehow missed M.hyps.

Last updated: Feb 06 2023 at 06:29 UTC