Natural number game question - mul_left_cancel

Stream: new members

[Zbigniew Fiedorowicz]

Hi, I am a newbie to lean. I am starting out by playing Kevin Buzzard's Natural number game. I have gotten to level 4 in the Advanced multiplication world and I have gotten stuck at what should be the final step of the induction.
My current state of the game is the following:

a : mynat,
ha : a ≠ 0,
d : mynat,
hd : ∀ (b : mynat), a * b = a * d → b = d,
g : mynat,
gd : a + a * g = a + a * d
⊢ succ g = succ d

It seems to me that all I need to do is to apply add_left_cancel at gd which should imply ag=ad and by induction hypothesis hd obtain g=d and hence succ g = succ d. However when I do that I get the following error message:

rewrite tactic failed, lemma lhs is a metavariable

What am I missing?
I apologize if this question has been previously answered.
Thanks in advance,
Zig Fiedorowicz

[Eric Wieser]

Would you mind editing your question to use #backticks?

[Eric Rodriguez]

what is your full code? are you trying to write apply add_left_cancel at gd? because that doesn't work, apply is only for the goal state

[Eric Rodriguez]

you may be thinking maybe more along the lines of have h := add_left_cancel _ _ _ gd

[Zbigniew Fiedorowicz]

No I am using

rw add_left_cancel at gd,

and also

rw add_left_cancel(a) at gd,

Both give the same result. I have also applied add_comm and tried add_right_cancel. That does not produce an error message, but expands the goal to 4 different goals with some strange metasymbols like ?m1

[Eric Rodriguez]

ahh, but rw deals with equalities or iffs; add_left_cancel is an implication

[Eric Rodriguez]

so Lean gets very confused what you mean

[Eric Rodriguez]

do you understand what I mean?

[Zbigniew Fiedorowicz]

Thanks.

rw add_right_cancel_iff at gd,

did the trick. Now my state is

case mynat.succ
a : mynat,
ha : a ≠ 0,
d : mynat,
hd : ∀ (b : mynat), a * b = a * d → b = d,
g : mynat,
gd : a * g = a * d
⊢ succ g = succ d

I now want to set b=g in hd. How do I do that?

[Zbigniew Fiedorowicz]

By a sequence of random guesses I found that

rw hd(g),

does the trick. However I don't understand the logic/syntax behind this trick. Can anyone enlighten me?

[Huỳnh Trần Khanh]

It's pretty simple actually. When you type hd g (this is exactly the same as hd(g), but hd g is the preferred syntax), you get this hypothesis: a * g = a * d → g = d. Let's call that hypothesis h. Without Lean's guessing superpowers, you'd have to apply the hypothesis gd to h to get g = d, and to close the goal you'd need to type rw hd g gd. But for some reason, Lean guessed the gd part so rw hd g closes the goal.

[Eric Rodriguez]

@Zbigniew Fiedorowicz , the crucial intuition that is good in these cases is to treat foralls and implications as functions

[Eric Rodriguez]

for example, hd : ∀ b : mynat, a * b = a * d → b = d, is a function that takes in a natural number b, and a proof that a * b = a * d, and turns it into a proof of b = d

[Zbigniew Fiedorowicz]

I am still confused about the rewrite tactic. Why does

rw add_right_cancel at gd,

applied to

gd : a * g + a = a * d + a,

produce a weird and unhelpful change of goals? And why does

rw add_left_cancel,

applied to

gd: a + a*g = a + a*d,

produce an obscure error message?

Is there some succinct description with examples on the proper use of rewrite?

[Hanting Zhang]

add_right_cancel is an implication; on the other hand, rw takes hypotheses of the form a = b or a \iff b and changes P a to P b (whatever P may be).

My guess is that in your use of rw add_right_cancel, Lean sees a + b = c + b → a = c and tries to pattern match it against a = b or a \iff b, which fails because you've only given it an implication. Then Lean sees that a = c, so it tries to find a hypothesis h : a + b = c + b in the local context and then rw using add_right_cancel h. But Lean can't find any h so it fails.

[Hanting Zhang]

Similarly, this is the problem with add_left_cancel

[Hanting Zhang]

You've used add_right_cancel_iff and it worked -- which is because now Lean sees the \iff instead of just → and rw knows what to do

[Zbigniew Fiedorowicz]

You seem to be saying that rw needs to be followed by some statement of equality or an iff statement. How does this square with the use

rw hd g,

where hd was a quantified implication, which I used successfully later in the proof?

Presumably if add_right_cancel had the form

add_right_cancel (a t b : mynat) :  ∀ (a t b), a + t = b + t → a = b

then

rw add_right_cancel a*g a a*d,

would have the desired result.

[Yakov Pechersky]

For your original problem, the rewrite you're looking for is "rw hd _ (add_left_cancel _ _ _ gd)". I think there is some confusion here. When you say "rw add_left_cancel at gd", that doesn't mean "utilize add_left_cancel to substitute a * g for a * d, using the proof named gd." It instead means "find the first thing I can rewrite in the expression named gd, which is the variable a. And to do such a rewrite (to some arbitrary x) , I need a proof that a + y = x + y, for some arbitrary y." That is why you got an unhelpful goal

[Yakov Pechersky]

The metavariable ?m_1 is that arbitrary x.

[Yakov Pechersky]

If you want to stick to single rewrites, you can look at what your goal is after "rw hd". Can you solve the goal after that?

[Yakov Pechersky]

Basically, your

lemma add_right_cancel (a t b : mynat) :  ∀ (a t b), a + t = b + t → a = b := sorry
[...]
rw add_right_cancel a*g a a*d -- <-- is missing the actual proof of "a * g + a = a * d + a" that is needed for the implication

[Zbigniew Fiedorowicz]

I am still having trouble with the rewrite tactic. I have the following state:

k : b + a * b = 0
⊢ b = 0

I am trying to apply

rw add_right_eq_zero k _ _ ,

and I get the error message

function expected at
  add_right_eq_zero k
term has type
  b = 0

I am guessing that rw is expecting an argument of type Prop. However when I attempt to coerce the type to Prop, I get an additional error message that there are too many arguments.

[Zbigniew Fiedorowicz]

OK, I found that

rw add_right_eq_zero k,

i.e. omitting the meta-variables, does the trick. I am still confused as to when I need to use meta-variables in rw.

Indeed imitating Yakov's answer to my previous question, I expected that

rw add_right_eq_zero _ _  k ,

would be the right approach. However this produced an obscure error message involving meta-variables. I then tried

rw add_right_eq_zero k _ _,

which produced a friendlier error message. Finally I found that omitting the meta-variables altogether was the right approach, but I don't understand why.

[Kevin Buzzard]

If you look at the type of add_right_eq_zero in Theorem Statements -> Advanced Addition World you'll see it's

add_right_eq_zero
  {a b : mynat} : a + b = 0 → a = 0

and the {} means "omit a and b, but the proof of a+b=0 need not be omitted.

What is going on is that the input of type a + b = 0 is enough to figure out what the earlier inputs were. This is a phenomenon which you see when you allow dependent functions. If you have a function from A x B to C and I tell you what element of B we're going to use, then obviously you can't tell what element of A we're going to use. But if you have a function from a collection of dependent pairs (a,b) where b is in B(a) and B(a) depends on a, then if you know what b is then you know what B(a) is and so maybe you can figure out a from this. To make people's lives easier in this situation Lean has this {} bracket thing which means that you don't need to supply a at all and the unification system will work it out.