# Zulip Chat Archive

## Stream: new members

### Topic: zero not 0?

#### Robert Watson (Apr 05 2022 at 12:42):

The following code doesn't work, and I don't understand why? (data.tactics and data.nat.basic)

```
def foo_hlp : ∀m : nat, (2 * m + 1 = 2 * 0 -> false) :=
begin
intro m,
norm_num
end
def foo : ∀ (n : nat), ∀ (m : nat), (2 * m + 1 = 2 * n -> false)
| zero := foo_hlp
```

#### Kevin Buzzard (Apr 05 2022 at 12:44):

(can you add the correct imports to the code so that it just works? there is no `data.tactics`

AFAIK) (I also don't understand why it doesn't work BTW)

#### Robert Watson (Apr 05 2022 at 12:47):

```
import tactics -- oops!
import data.real.basic -- this should be incidental, right?
import data.nat.basic
noncomputable theory -- this should be incidental, right?
open_locale classical -- this should be incidental, right?
def foo_hlp : ∀m : nat, (2 * m + 1 = 2 * 0 -> false) :=
begin
intro m,
norm_num
end
def foo : ∀ (n : nat), ∀ (m : nat), (2 * m + 1 = 2 * n -> false)
| zero := foo_hlp
```

#### Kevin Buzzard (Apr 05 2022 at 12:47):

Aah -- now I do:

```
import tactic
import data.nat.basic
def foo_hlp : ∀m : nat, (2 * m + 1 = 2 * 0 -> false) :=
begin
intro m,
norm_num
end
def foo : ∀ (n : nat), ∀ (m : nat), (2 * m + 1 = 2 * n -> false)
| zero m h := foo_hlp m begin exact h end
```

gives the more useful information that `zero`

is being interpreted as a variable. You will want to `open nat`

or use `nat.zero`

#### Robert Watson (Apr 05 2022 at 13:06):

I haven't added open.nat as I don't understand what it would do here. But just copying this code I get the following error:

invalid type ascription, term has type

2 * m + 1 = 2 * zero

but is expected to have type

2 * m + 1 = 2 * 0

Also, I don't get why h has to be exacted like that? why not foo_hlp m h , since h is already given ?

#### Riccardo Brasca (Apr 05 2022 at 13:08):

What Kevin is saying is that the natural number 0 is called `nat.zero`

not `zero`

#### Reid Barton (Apr 05 2022 at 13:08):

`zero`

isn't `0`

. `nat.zero`

is `0`

. If you `open nat`

, then `zero`

means `nat.zero`

#### Riccardo Brasca (Apr 05 2022 at 13:09):

Note that you can write `0`

and Lean will understand it

#### Riccardo Brasca (Apr 05 2022 at 13:11):

`open nat`

means that if something is called `nat.foo`

you can just write `foo`

.

#### Reid Barton (Apr 05 2022 at 13:13):

It can be confusing that there is no syntactic distinction between constants and variables in pattern matching.

#### Robert Watson (Apr 05 2022 at 13:14):

I didn't know there was such a thing as 'variable' zero for pattern matching!

#### Kevin Buzzard (Apr 05 2022 at 13:14):

Sorry for the confusion. I mean this:

```
import tactic
import data.nat.basic
def foo_hlp : ∀m : nat, (2 * m + 1 = 2 * 0 -> false) :=
begin
intro m,
norm_num
end
def foo : ∀ (n : nat), ∀ (m : nat), (2 * m + 1 = 2 * n -> false)
| nat.zero := foo_hlp
```

#### Reid Barton (Apr 05 2022 at 13:15):

Your

```
def foo : ∀ (n : nat), ∀ (m : nat), (2 * m + 1 = 2 * n -> false)
| zero := foo_hlp
```

is exactly the same as

```
def foo : ∀ (n : nat), ∀ (m : nat), (2 * m + 1 = 2 * n -> false)
| x := foo_hlp
```

as far as Lean is concerned

#### Kevin Buzzard (Apr 05 2022 at 13:15):

In pattern matching you can use variables. You used a variable called `zero`

.

#### Robert Watson (Apr 05 2022 at 13:17):

Right, it could have been any string...and name of some variable

#### Robert Watson (Apr 05 2022 at 13:18):

I thought it was being a bit too clever working out my succ x for me!

Last updated: Dec 20 2023 at 11:08 UTC