Having nat as a goal

Stream: new members

[Johannes C. Mayer]

I have :

example : ∀ a b c : ℕ, a = b → b = c → a = c :=
begin
  intros,
  apply eq.trans,
  repeat {assumption}
end

Now the tactic state in the apply eq.trans line is the following:

  3 goals
  a b c : ℕ,
  ᾰ : a = b,
  ᾰ_1 : b = c
  ⊢ a = ?m_1

  a b c : ℕ,
  ᾰ : a = b,
  ᾰ_1 : b = c
  ⊢ ?m_1 = c

  a b c : ℕ,
  ᾰ : a = b,
  ᾰ_1 : b = c
  ⊢ ℕ

Why do we have as the third goal that we need to show that we have a term of type nat? And why does this goal get solved when using (the first) assumption automatically, even though it is never the active goal?

[Kyle Miller]

When you apply eq.trans, it doesn't know what the middle value is supposed to be, so Lean leaves it as a metavariable (pretty printed as ?m_1). In tactics, every goal corresponds to some metavariable, and the type of which is shown in the last line. The third goal corresponds to this metavariable.

When you do assumption, Lean will try unifying the goal with each hypothesis. The a = b hypothesis will succeed, and the metavariable will be set to b. Lean notices that the third goal's metavariable has been set, and it's automatically removed.

[Kyle Miller]

Metavariables are "holes" in an expression, and Lean is very eager to fill them.

[Kyle Miller]

Here's an example for how you can tell Lean what the middle value's supposed to be:

example : ∀ a b c : ℕ, a = b → b = c → a = c :=
begin
  intros,
  apply @eq.trans _ _ b,  -- only two goals after this line
  repeat {assumption}
end

[Kyle Miller]

There's a tactic for (generalized) transitivity. Rather than apply eq.trans you can do transitivity b or transitivity. tactic#transitivity

[Kyle Miller]

I didn't know about tactic#assumption', which can replace repeat {assumption} here

[Kyle Miller]

This example might also be illuminating:

example : ∀ a b c : ℕ, a = b → b = c → a = c :=
begin
  intros,
  apply eq.trans,
  show ℕ,
  exact b,
  assumption',
end

[Johannes C. Mayer]

So we have these meta-variables that are generated by the tactics, because they are actually not part of the actual type theory of LEAN, but are something additional that we use in the tactic mode, which allows us to create a sort of program that generates a proof term? And the idea is that this is more flexible, and allows inspection of state, I guess.

But so you are saying, that the goal of nat is actually the goal to show that ?m_1 is of type nat? It just seems a bit strange to me, because there is no annotation that this is what it is about. It seems that I could switch (how do you do that I only know swap) to the 3rd goal and apply any of a, b or c. And I guess based on what I use to close the goal, I would replace all ?m_1 with that.

You can also have multiple goals of nat and then it is not clear what meta variable it refers to. (Although all of this is in practice probably never an issue possibly.)

example : ∀ a b c : ℕ, a = b → b = c → a = c :=
begin
  intros,
  apply eq.trans,
  apply eq.trans,
end

Gives you:

5 goals
  a b c : ℕ,
  ᾰ : a = b,
  ᾰ_1 : b = c
  ⊢ a = ?m_1

  a b c : ℕ,
  ᾰ : a = b,
  ᾰ_1 : b = c
  ⊢ ?m_1 = ?m_2

  a b c : ℕ,
  ᾰ : a = b,
  ᾰ_1 : b = c
  ⊢ ℕ

  a b c : ℕ,
  ᾰ : a = b,
  ᾰ_1 : b = c
  ⊢ ?m_1 = c

  a b c : ℕ,
  ᾰ : a = b,
  ᾰ_1 : b = c
  ⊢ ℕ

But here I would guess that the first nat refers to ?m_2 as it does not appear after that the first nat goal.

[Scott Morrison]

Yes, this is all correct. "Under the hood" there is no ambiguity, of course, although it is true that there could be nicer labelling of goals that appear as metavariables in other goals. Very often proofs will avoid ever having exposed metavariables like this: e.g. through use of have and suffices and other structured proof tactics.

[Kyle Miller]

Johannes C. Mayer said:

But so you are saying, that the goal of nat is actually the goal to show that ?m_1 is of type nat?

To be a little more precise with the language here, the goal is ?m_1 : nat, and you're trying to fill in the ?m_1. Lean already knows that ?m_1 has type nat.

A bit more about the mechanics of it: when you do apply eq.trans, what Lean effectively does is exact @eq.trans ?M1 ?M2 ?M3 ?M4 ?M5 ?M6 where ?M1 through ?M6 are metavariables. It's immediately able to figure out that ?M1 is nat, ?M2 is a, and ?M4 is c. The remaining metavariables become the three goals.

[Kyle Miller]

Johannes C. Mayer said:

It seems that I could switch (how do you do that I only know swap) to the 3rd goal and apply any of a, b or c. And I guess based on what I use to close the goal, I would replace all ?m_1 with that.

Try out the last example I gave, which uses show to select the nat goal and then uses exact to close it.

[Kyle Miller]

Also, metavariables are actually used for all of typechecking/elaboration, as I understand it, not just in tactics. This is how Lean solves for things like implicit variables. For example, the id function has the type Π {α : Sort*}, α → α. If you do

#check id

then Lean's not able to solve for the metavariable for α and you get id : ?M_1 → ?M_1.

Lean doesn't allow metavariables to go unfilled. For example,

def my_id := id

results in the error

don't know how to synthesize placeholder
context:
⊢ Sort ?

This is referring to the fact it's not able to solve for ?M_1 : Sort* with some actual expression. (I guess "placeholder" is a synonym for "metavariable.")

It's able to solve for this metavariable in the following, though:

def my_nat_id : ℕ → ℕ := id

[Mario Carneiro]

Johannes C. Mayer said:

It seems that I could switch (how do you do that I only know swap) to the 3rd goal and apply any of a, b or c.

By the way the swap tactic takes an optional argument, and will bring the specified goal to the front, i.e. swap 3 will move goal 3 to the front. rotate can also be used for a similar effect.

[Johannes C. Mayer]

Thanks all, that's all very informative.