# Zulip Chat Archive

## Stream: new members

### Topic: Natural number game question - mul_left_cancel

#### Zbigniew Fiedorowicz (Jun 27 2021 at 21:38):

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 a*g=a*d 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 (Jun 27 2021 at 21:52):

Would you mind editing your question to use #backticks?

#### Eric Rodriguez (Jun 27 2021 at 21:59):

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 (Jun 27 2021 at 22:00):

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

#### Zbigniew Fiedorowicz (Jun 27 2021 at 22:02):

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 (Jun 27 2021 at 22:04):

ahh, but `rw`

deals with equalities or iffs; `add_left_cancel`

is an implication

#### Eric Rodriguez (Jun 27 2021 at 22:04):

so Lean gets very confused what you mean

#### Eric Rodriguez (Jun 27 2021 at 22:11):

do you understand what I mean?

#### Zbigniew Fiedorowicz (Jun 28 2021 at 01:04):

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 (Jun 28 2021 at 01:21):

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 (Jun 28 2021 at 01:28):

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 (Jun 28 2021 at 12:04):

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

#### Eric Rodriguez (Jun 28 2021 at 12:05):

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 (Jun 28 2021 at 15:45):

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 (Jun 28 2021 at 16:07):

`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 (Jun 28 2021 at 16:07):

Similarly, this is the problem with `add_left_cancel`

#### Hanting Zhang (Jun 28 2021 at 16:08):

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 (Jun 28 2021 at 16:41):

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 (Jun 28 2021 at 16:56):

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 (Jun 28 2021 at 16:57):

The metavariable ?m_1 is that arbitrary x.

#### Yakov Pechersky (Jun 28 2021 at 16:58):

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 (Jun 28 2021 at 17:14):

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 (Jun 30 2021 at 19:07):

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 (Jun 30 2021 at 19:25):

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 (Jun 30 2021 at 22:19):

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.

Last updated: Dec 20 2023 at 11:08 UTC