6
$\begingroup$

There are two related questions that I expound on below. It might seem like these aren't quite related, but they are both about how to deal with meta-variables that appear when working through a proof.

  1. How do we "fill in" meta-variables that appear in hypotheses in targets.

  2. Do meta-variables appearing in hypotheses act like universal quantifiers and meta-variables appearing in targets act like existential quantifiers?

Here are some details.

Let's consider the following bit of lean proof code. (This is taken from this repository of Kevin Buzzard's that deals with equivalence relations. This is not really relevant to the question; this is used as an example of some of the difficulties I sometimes run into.)

import tactic
variables {α : Type} (R : α → α → Prop) --(a b : α)

def cl (a : α) := {b : α | R b a}

variables {R} (hR : equivalence R)
include hR

example {a b : α} :
  a ∈ cl R b →
  cl R a ⊆ cl R b :=
begin
  intros a_in_cl_b c c_in_cl_a,
  rcases hR with ⟨R_refl, R_sym, R_trans⟩,
  apply R_trans,
  exact c_in_cl_a,
  exact a_in_cl_b,
end

This proof works fine, except that at the point where we have applied the rule R_trans, this creates goals with meta-variables. For instance,

enter image description here

This seems to mean that Lean isn't able to infer the type that should go in the ?m_1 slot, much less infer what variable (in this case, a) should go there. Now, in this case, we can resolve the issue by using exact c_in_cl_a, at which point Lean understands what needs to go in the place of ?m_1, it is able to automatically close some remaining goals, and we can finish the proof off with one more exact _.

Now, in this case, if we unfold transitive at R_trans, we can see that there are some weakly inserted implicit arguments:

∀ ⦃x y z : α⦄, R x y → R y z → R x z

Perhaps this is the issue, but I don't think so.

In other cases, (for instance, this happened while completing the Natural Number Game, although I can't for the life of me find which level it was), I wasn't able to resolve the issue by telling Lean to look at a particular hypothesis. In addition, I've run into situations$^1$ where the meta-variable appears in a hypothesis, and at that point I definitely don't know how to deal with it.

So, the primary question is: Is there a way to directly tell Lean to fill in meta-variables with values from the hypothesis-space? It might be that this isn't allowed, mathematically or type-theoretically or tactically, but I don't have enough of a handle on things to know if that's true or not. It seems like the meta-variables showing up in this way sort of implies the existence of some sort of universal quantifier (in the case of hypotheses, so that they can be filled in) or existential quantifier (in the case of the meta-variable showing up in the target, so that we can use a particular value from the hypothesis-space to fill it in).

$^1$ I moved on from these and likewise can't find any examples anymore, unfortunately. If someone understand the problem and can edit this question with an example where this happens, please feel free to do that!


Note 1: this question is likely relevant to proof assistants other than Lean, but I've added the lean tag because that's the one I'm familiar with and the one I'm using as the example above. In addition, there is a related question alluded to in the text above, which is basically, "Have I done something 'wrong' if I've reached a state in which metavariables are appearing in the target (or in a hypothesis)?"

Note 2: Instead of

apply R_trans,
exact c_in_cl_a,
exact a_in_cl_b,

we can also close the goal using

exact R_trans c_in_cl_a a_in_cl_b,

so of course this whole situation can be avoided (see Note 1 above). Nonetheless, I'd still like to know how to deal with these situations.

$\endgroup$

2 Answers 2

6
$\begingroup$

Arguably, the most direct way (type theoretically or tactically) to do this is to find the goal that corresponds to ?m_1 and fill it. In your example, the goals look like this after apply R_trans (condensing the local contexts for brevity):

3 goals
α : Type,
R : α → α → Prop,
a b : α,
a_in_cl_b : a ∈ cl R b,
c : α,
c_in_cl_a : c ∈ cl R a,
R_refl : reflexive R,
R_sym : symmetric R,
R_trans : transitive R
⊢ R c ?m_1

...
⊢ R ?m_1 b

...
⊢ α

In Lean, every goal is an unfilled metavariable. It does not show the names of the metavariables normally, only the types, but the third goal, ⊢ α, is in fact ?m_1, as you can observe by switching to it and filling it:

example {a b : α} :
  a ∈ cl R b →
  cl R a ⊆ cl R b :=
begin
  intros a_in_cl_b c c_in_cl_a,
  rcases hR with ⟨R_refl, R_sym, R_trans⟩,
  apply R_trans,
  swap 3, -- move ⊢ α to the front
  exact a, -- set ?m_1 := a
  -- goals are now:
  -- ⊢ R c a
  -- ⊢ R a b
end

The other goals are metavariables too, in the proof term being constructed, but they don't usually show up in the types of other metavariables unless you are working with a function that has proof arguments (aka a partial function) like list.last.

However, these kinds of goals are usually solved "en passant" by applying something that unifies the type, like your exact c_in_cl_a example. You can also do the unification without solving the goal directly in this case using change R c a, which is what I would probably do instead of selecting the third goal and exact a like I did here.


To your other questions:

  • "Have I done something wrong?" No, not really, although it is good style to avoid these transient goals when possible, by using something like transitivity a to pin it down at the point you create the subgoals, or refine R_trans c_in_cl_a _ which solves enough of the goal to avoid the term metavariables. Most tactics are just fine with these metavariables existing, although you might get suboptimal results (for example, ring can solve a + b = b + a but not a + b = b + ?m_1).

  • "What if metavariables appear in the hypotheses?" The change trick works there as well, you just use change T at h instead, as well as solving the relevant auxiliary goal, as well as eliminating the metavariable before it pops up.

$\endgroup$
3
  • $\begingroup$ in my defence... $\endgroup$ Feb 18 at 15:03
  • $\begingroup$ @KevinBuzzard. I knew I'd seen that somewhere! I've been going back and forth between a bunch of these tutorials, and I thought I'd seem something like that somewhere, but just couldn't find it. Of course it was part of your solutions in these problem sets. :/ $\endgroup$
    – march
    Feb 18 at 16:41
  • $\begingroup$ Thanks for answering and for showing me swap. We can actually use a, b, or c there, and we can still close all of the goals (of course, because this is an equivalence relation, and a, b, and c are all equivalent). However, generally, it seems like this is one of those places where we can get stuck in the proof (analogous to where we use left where we should have used right on the goal) by choosing the wrong variable to take the place of ?m_1. This is in part what I meant by going "wrong" in the proof. Lean allows it, but it could lead to a dead-end. $\endgroup$
    – march
    Feb 18 at 16:47
3
$\begingroup$

It's possible to write a tactic that will assign to meta-variables. This tactic is incomplete but works in your example:

meta def tactic.interactive.set_meta (e : interactive.parse interactive.types.texpr) :=
  tactic.target >>= tactic.to_expr ∘ to_pexpr >> tactic.swap >> `[exact %%e]

After

example {a b : α} :
  a ∈ cl R b →
  cl R a ⊆ cl R b :=
begin
  intros a_in_cl_b c c_in_cl_a,
  rcases hR with ⟨R_refl, R_sym, R_trans⟩,
  apply R_trans,

The main goal is ⊢ R c ?m_1. Adding this line:

  set_meta a,

Transforms the goal into ⊢ R c a.

$\endgroup$
2
  • $\begingroup$ That's great thanks! I'm not yet at the tactic-writing stage, but it seems like this is an automated version of Mario's post? $\endgroup$
    – march
    Feb 18 at 16:48
  • $\begingroup$ Yes, it is similar to swap 3, exact a. However it also works for metavariables that have no associated goals. For example : 0 ≠ _ := by { set_meta 1, simp } $\endgroup$ Feb 18 at 18:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.