Zulip Chat Archive

Stream: new members

Topic: instantiating meta variales


view this post on Zulip Ken Roe (Jul 24 2018 at 19:06):

Is there a way to instantiate meta variables. Consider the theorem below:

theorem x:  x, x=5 :=
begin existsi _, ..
end

What should the ... be replaced with? In this theorem, we could just change the existsi _ but in more complex theorems, meta variables seem to appear in many other places and it would be nice to instantiate them.

view this post on Zulip Kenny Lau (Jul 24 2018 at 19:07):

what information would you provide in order for the metavariables to be instantiated?

view this post on Zulip Kenny Lau (Jul 24 2018 at 19:07):

replacing .. with refl would prove the theorem, but I don't know if that is what you want

view this post on Zulip Ken Roe (Jul 24 2018 at 19:22):

refl is not what I want. In Coq, you can provide a value using instantiate (meta_var := value). Is there something similar in Lean?

view this post on Zulip Patrick Massot (Jul 24 2018 at 19:23):

Doesn't this meta variable appear as a new goal?

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 19:38):

existsi 7 will instantiate the metavariable. If you use a hole _ then you get a new goal ⊢ ℕ as Patrick says. You can make this the first goal with show ℕ or swap and then instantiate it with exact 7.

view this post on Zulip Ken Roe (Jul 24 2018 at 19:48):

I've seen those new goals as holes--that is how to fill in the holes. Can swap be used beyond the second goal or is there something similar to switch for example the first and third goal?

view this post on Zulip Patrick Massot (Jul 24 2018 at 19:49):

https://github.com/leanprover/mathlib/blob/master/tactic/interactive.lean#L159

view this post on Zulip Patrick Massot (Jul 24 2018 at 19:49):

as explained by Kevin

view this post on Zulip Patrick Massot (Jul 24 2018 at 19:50):

You can also use show if you have only one goal of that type


Last updated: May 12 2021 at 04:19 UTC