Zulip Chat Archive

Stream: new members

Topic: Metavariables?


view this post on Zulip Kristaps John Balodis (Feb 02 2021 at 05:59):

I have 3 related questions about metavariables, but allow me to set the stage, so you know where I'm coming from.
I'm trying to do Level 1/4 of Advanced Multiplication World from The Natural Number Game, which is asking to prove

theorem mul_pos (a b : mynat) : a  0  b  0  a * b  0 :=

So far, I've come up with

begin
intro a_zero,
intro b_zero,
cases b,
rw mul_zero,
apply b_zero,

intro h,
rw mul_succ at h,

sorry
end

which leaves me with a goal state of

case mynat.succ
a : mynat,
a_zero : a  0,
b : mynat,
b_zero : succ b  0,
h : a * b + a = 0
 false

Now one thing I'm trying at this point, is to force a to be zero, however when I try writing

rw eq_zero_of_add_right_eq_self at h,

Lean is telling me it won't apply the tactic because the lhs is a "metavariable".
1) What is a metavariable?
2) Why can't I use this tactic on metavariables?
3) How should I proceed?

view this post on Zulip Thomas Browning (Feb 02 2021 at 06:03):

The lemma eq_zero_of_add_right_eq_self is an implication. You can only use rw with equalities and iffs

view this post on Zulip Thomas Browning (Feb 02 2021 at 06:04):

Also, I think that you want to use add_left_eq_zero rather than eq_zero_of_add_right_eq_self

view this post on Zulip Kristaps John Balodis (Feb 02 2021 at 06:08):

That seems to give me the same error about metavariables, as does add_right_eq_zero

view this post on Zulip Thomas Browning (Feb 02 2021 at 06:09):

You can't use rw with add_right_eq_zero, since it is an implication

view this post on Zulip Thomas Browning (Feb 02 2021 at 06:10):

Instead, maybe start with have key := add_right_eq_zero h

view this post on Zulip Thomas Browning (Feb 02 2021 at 06:10):

That directly feeds h into add_right_eq_zero

view this post on Zulip Kristaps John Balodis (Feb 02 2021 at 06:21):

That seemed to work. The only issue is, have key has not been introduced in The Natural Number Game yet, so there ought to be some other way of making this work.

view this post on Zulip Kristaps John Balodis (Feb 02 2021 at 06:22):

Ah, but have has been introduced, and that seems to work without writing key , thanks!

view this post on Zulip Alex J. Best (Feb 02 2021 at 06:24):

key is just an optional name you can give the hypothesis, if you don't give a name have will call it this by default which becomes annoying if you have more than one thing, they end up all called this!

view this post on Zulip Kyle Miller (Feb 02 2021 at 06:38):

@Kristaps John Balodis Roughly speaking, a metavariable is what Lean uses to fill in missing details automatically, and Lean solves for metavariables in a process called unification. I think what's happening here is that it wasn't sure what b was supposed to be.


Last updated: May 15 2021 at 02:11 UTC