zero not 0?

Stream: new members

[Robert Watson]

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]

(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]

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]

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]

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]

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

[Reid Barton]

zero isn't 0. nat.zero is 0. If you open nat, then zero means nat.zero

[Riccardo Brasca]

Note that you can write 0 and Lean will understand it

[Riccardo Brasca]

open nat means that if something is called nat.foo you can just write foo.

[Reid Barton]

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

[Robert Watson]

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

[Kevin Buzzard]

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]

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]

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

[Robert Watson]

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

[Robert Watson]

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