detecting terminal goals

Stream: general

[Scott Morrison]

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

[Scott Morrison]

Unfortunately it is not working at the moment.

[Scott Morrison]

(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.)

[Scott Morrison]

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."))

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Q1. Is this already implemented somewhere, better?

[Scott Morrison]

Q2. Any suggestions how I fix it?

[Scott Morrison]

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

[Simon Hudon]

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?

[Scott Morrison]

@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.

[Simon Hudon]

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

[Scott Morrison]

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. :-)

[Simon Hudon]

Thanks :)

[Scott Morrison]

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.

[Scott Morrison]

Is it just an app of an mvar?

[Scott Morrison]

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."))

[Simon Hudon]

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.

[Scott Morrison]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Scott Morrison]

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

[Simon Hudon]

I can try to demystify if you like

[Simon Hudon]

Have you used get_goals and set_goals?

[Scott Morrison]

Yes, many times!

[Simon Hudon]

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

[Scott Morrison]

Yes!

[Scott Morrison]

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

[Simon Hudon]

(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.

[Scott Morrison]

Great!

[Simon Hudon]

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.

[Simon Hudon]

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?

[Simon Hudon]

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.

[Simon Hudon]

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.

[Scott Morrison]

I see.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

phew! :-)

[Scott Morrison]

(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.)

[Simon Hudon]

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

[Simon Hudon]

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!