How do we resolve metavariables that appear in hypotheses and targets in Lean?

Question

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,

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.

Answer 1

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.

Answer 2

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.