## 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