Zulip Chat Archive

Stream: general

Topic: detecting terminal goals


view this post on Zulip Scott Morrison (Apr 26 2018 at 10:52):

I have a little tactic that is meant to determine with the current goal is "terminal", that is, no other goals depend on it.

view this post on Zulip Scott Morrison (Apr 26 2018 at 10:52):

Unfortunately it is not working at the moment.

view this post on Zulip Scott Morrison (Apr 26 2018 at 10:53):

(The idea is just that if you know your current goal is terminal, you can be much more aggressive in discharging it, because nothing can go wrong later.)

view this post on Zulip Scott Morrison (Apr 26 2018 at 10:54):

I currently have

meta def metavariables : tactic (list expr) :=
do r  result,
   pure (r.fold [] $ λ e _ l,
     match e with
     | expr.mvar _ _ _ := insert e l
     | _ := l
     end)

meta def terminal_goal : tactic unit :=
  do goals  get_goals,
     let current_goal := goals.head,
     other_goals  metavariables,
     let other_goals := other_goals.erase current_goal,
     other_goals.mmap' $ λ g, (do t  infer_type g, d  kdepends_on t current_goal,
                                  monad.whenb d $ pp t >>= λ s, fail ("This is not a terminal goal: " ++ s.to_string ++ " depends on it."))

view this post on Zulip Scott Morrison (Apr 26 2018 at 10:54):

And this works great detecting when the current goal appears in the form ?m_1 in a later goal.

view this post on Zulip Scott Morrison (Apr 26 2018 at 10:54):

But fails to detect that the current goal appears as something like ?m_1[_] in a later goal.

view this post on Zulip Scott Morrison (Apr 26 2018 at 10:55):

Q1. Is this already implemented somewhere, better?

view this post on Zulip Scott Morrison (Apr 26 2018 at 10:55):

Q2. Any suggestions how I fix it?

view this post on Zulip Scott Morrison (Apr 26 2018 at 11:00):

Here's a MWE:

private structure D :=
 ( w : ℕ → Type )
 ( x : list (w 0) )

 private def test_terminal_goal : D :=
 begin
    split,
    swap,
    success_if_fail { terminal_goal }, -- succeeds, because terminal_goal correctly fails
    intros,
    success_if_fail { terminal_goal }, -- fails, because terminal_goal incorrectly succeeds
    exact ℕ,
    exact []
 end

view this post on Zulip Simon Hudon (Apr 26 2018 at 13:49):

I think I would do it as:

meta def terminal_goal' : tactic unit :=
do g :: gs ← get_goals,
   gs.for_each $ λ g', guard (g'.occurs g)

It works with your example but does it work with your use cases?

view this post on Zulip Scott Morrison (Apr 27 2018 at 04:43):

@Simon Hudon, this doesn't seem to work in other cases. My tests are here: <https://gist.github.com/semorrison/5188f3c3e508148657be4d66f4875d8d> if you want to have a look. I have to run now, but will try to decipher why your version isn't working on the other tests later.

view this post on Zulip Simon Hudon (Apr 27 2018 at 04:50):

Ok, I'll have a look when I wake up :)

view this post on Zulip Scott Morrison (Apr 27 2018 at 04:52):

I don't really understand the logic of your suggestion: surely you meant guard (¬ g.occurs g') not guard (g'.occurs g)? In any case neither of those work. Sleep well. :-)

view this post on Zulip Simon Hudon (Apr 27 2018 at 04:53):

Thanks :)

view this post on Zulip Scott Morrison (Apr 28 2018 at 02:48):

When I see a goal with a "parametrised metavariable" like ?m_1[0], what does the underlying expr look like? I can't decipher what it should be.

view this post on Zulip Scott Morrison (Apr 28 2018 at 02:50):

Is it just an app of an mvar?

view this post on Zulip Scott Morrison (Apr 28 2018 at 03:29):

Okay --- I've worked this all out. For anyone keeping score:

meta def metavariables : tactic (list expr) :=
do r ← result,
   pure (r.fold [] $ λ e _ l,
     match e with
     | expr.mvar _ _ _ := insert e l
     | _ := l
     end)

meta def propositional_goal : tactic unit :=
do goals ← get_goals,
   let current_goal := goals.head,
   current_goal_type ← infer_type current_goal,
   p ← is_prop current_goal_type,
   guard p

meta def subsingleton_goal : tactic unit :=
do goals ← get_goals,
   let current_goal := goals.head,
   current_goal_type ← infer_type current_goal >>= instantiate_mvars,
   to_expr ``(subsingleton %%current_goal_type) >>= mk_instance >> skip

meta def terminal_goal : tactic unit :=
propositional_goal <|> subsingleton_goal <|>
do goals ← get_goals,
   let current_goal := goals.head,
   other_goals ← metavariables,
   let other_goals := other_goals.erase current_goal,
   other_goals.mmap' $ λ g, (do t ← infer_type g, t ← instantiate_mvars t, trace t, d ← kdepends_on t current_goal,
                                monad.whenb d $ pp t >>= λ s, fail ("This is not a terminal goal: " ++ s.to_string ++ " depends on it."))

view this post on Zulip Simon Hudon (Apr 28 2018 at 04:22):

I don't know if you still need the answer but ?m_1[0] is a regular meta variable. I think [0]signals the context that the variable can see. I don't know how to decode it though.

view this post on Zulip Scott Morrison (Apr 28 2018 at 04:30):

Thanks @Simon Hudon, all sorted out. ?m_1[0] is encoded simply as an application of an mvar on the expressions appearing inside the [ ... ]. It turned out that I was missing an instantiate_mvars, which was preventing successfully detection of these sort of "dependent mvars". I've made a PR for my terminal_goal tactic and some relatives. https://github.com/leanprover/mathlib/pull/125

view this post on Zulip Simon Hudon (Apr 28 2018 at 04:31):

Oh, good! Sorry I couldn't help you any more than that

view this post on Zulip Simon Hudon (Apr 28 2018 at 04:31):

You have to be careful with those variables. They sneak up on you

view this post on Zulip Scott Morrison (Apr 28 2018 at 04:34):

I can't believe that I've written code that successfully uses instantiate_mvars. What it actually means is still voodoo to me.

view this post on Zulip Simon Hudon (Apr 28 2018 at 04:40):

I can try to demystify if you like

view this post on Zulip Simon Hudon (Apr 28 2018 at 04:41):

Have you used get_goals and set_goals?

view this post on Zulip Scott Morrison (Apr 28 2018 at 04:41):

Yes, many times!

view this post on Zulip Simon Hudon (Apr 28 2018 at 04:42):

Good! And do you know that get_goals returns a list of expressions that are in fact unassigned meta variables?

view this post on Zulip Scott Morrison (Apr 28 2018 at 04:43):

Yes!

view this post on Zulip Scott Morrison (Apr 28 2018 at 04:43):

(If I were Kevin, I'd be promising to write documentation in exchange for your explanation. :-)

view this post on Zulip Simon Hudon (Apr 28 2018 at 04:45):

(Haha! Where's Kevin when we need him!)

Good. So think of the proof state as being made of two parts (for the sake of this explanation): list of goals which is an arbitrary list of meta variables and the set of all allowed meta variables, some of which are assigned a value.

view this post on Zulip Scott Morrison (Apr 28 2018 at 04:46):

Great!

view this post on Zulip Simon Hudon (Apr 28 2018 at 04:48):

The relationship between the proof state and whatever you're trying to prove is that, when you enter tactic mode, you create an unassigned variable, put it in the list of goals and that variable is in fact the proof that you're supposed to return. From that point on, the assertion you're trying to prove does not matter. Only the variables and the goals do.

view this post on Zulip Simon Hudon (Apr 28 2018 at 04:49):

I don't know if you've ever had that problem but sometimes, you succeed in leaving a tactic block and when you finish the proof, you're told that your proof contains unassigned variables. Does this ring a bell?

view this post on Zulip Simon Hudon (Apr 28 2018 at 05:08):

Long story short, instantiate_mvar finds all the mvar nodes in your expression and, if the meta variable has a value (or type expr) in the proof state it replaces mvar with it. That means that, if you're pattern matching (using match) on an expression and you're looking for expr.app (expr.app (const eq _) e0) e1 and that you mean mvar instead, even if that variable is assigned to a value that matches exactly what you're looking for, the pattern matching will fail. That's why it's prudent to use instantiate_mvar before matching on a expr` of which you don't know for sure that it doesn't contain meta variables.

view this post on Zulip Simon Hudon (Apr 28 2018 at 05:09):

I realize my explanation was a bit round about. I just needed to introduce the idea that the life span of meta variables is a whole proof and that it doesn't disappear once it's assigned.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:20):

I see.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:20):

I've encountered needing it in another strange place, as well, which I think matches with your explanation.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:20):

I was writing a tool for finding _all_ the possible rewrites of a given expression by a given rule.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:21):

Unfortunately the built-in rewrite has some problems --- once it has matched some of the parameters of your rewrite rule a particular way, it will subsequently only match the parameters the same way, when looking for further places the rule matches.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:22):

This even persists between different invocations of rewrite_core, because this information is actually stored in the tactic state.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:22):

To solve this, I had to write a tactic lock_tactic_state (t : tactic A) : tactic A which just discards any changes to the tactic state after invocation.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:22):

This throws away any information the tactic state was storing about how rewrite parameters had to match.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:23):

Unfortunately, the proofs that rewrite_core produced where suddenly full of metavariables!

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:23):

I understand now that this is because these metavariables were _assigned_, but not _instantiated_, so when I discarded the tactic_state those assignments were being lost.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:24):

Calling instantiate_mvars on the proof term, before discarding the state, saved those assignments.

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:24):

phew! :-)

view this post on Zulip Scott Morrison (Apr 28 2018 at 05:25):

(Sorry I missed the end of your explanation; family things happening at this end. I'm going to ping you @Simon Hudon as I expect you'll find this other example interesting.)

view this post on Zulip Simon Hudon (Apr 28 2018 at 05:31):

I'd be curious to see how you implemented lock_tactic_state. Did you deconstruct the tactic value and extract the expected proof?

view this post on Zulip Simon Hudon (Apr 28 2018 at 05:33):

I'm looking forward to your next example. I'll probably see it when I wake up. Incidentally, Australia is way too far! Someone should move it closer to Europe and America, that way our days would overlap!


Last updated: May 16 2021 at 21:11 UTC