Zulip Chat Archive

Stream: new members

Topic: redefining nat


view this post on Zulip Thorsten Altenkirch (Sep 21 2020 at 15:45):

Actually I just wanted to define my own pred which is already defined. Hence I thought I just redefine nat but I ran into some problems. First of all it still seems to use succ from the prelude nat. What have I done wrong? Second how do I tell it to use decimal notation for my nat? I am looking at the prelude file but now clue...

namespace mynat

inductive nat : Type
| zero : nat
| succ : nat  nat

local notation `ℕ` := nat

open nat

example :  n : , zero  succ n :=
begin
  assume n h,
  contradiction,
end

def pred :   
| zero := zero
| (succ n) := n

#reduce (pred 7)

end mynat

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:00):

I think open nat opened the global nat

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:00):

try open mynat.nat

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:01):

To get numbers, you need to implement 0 and 1 and +

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:02):

But that is only for parsing. For printing succ (succ zero) as 2 I think the printer support for that is hardcoded for nat

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:04):

namespace mynat

inductive nat : Type
| zero : nat
| succ : nat  nat

local notation `ℕ` := nat

open mynat.nat

example :  n : , zero  succ n :=
begin
  assume n h,
  contradiction,
end

def pred :   
| zero := zero
| (succ n) := n

def add :     
| zero b := b
| (succ a) b := succ (add a b)

instance : has_zero  := zero
instance : has_one  := succ zero
instance : has_add  := add

#reduce pred 7

end mynat

(I implemented add backwards for you :stuck_out_tongue_wink: )

view this post on Zulip Yakov Pechersky (Sep 21 2020 at 16:04):

Wouldn't that be giving bit0 and bit1lemmas?

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:06):

Lean has some magic to print sequences of succs in decimal notation. I think it is a misfeature, because it makes it easy to confuse with the "official" bit0/bit1 representation

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:06):

but it makes sense if you are using #reduce instead of #eval to evaluate numbers

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:09):

If you use #eval to evaluate numbers, you can print the result using a has_repr instance:

...

def to_root_nat :   _root_.nat
| zero := _root_.nat.zero
| (succ n) := _root_.nat.succ (to_root_nat n)

instance : has_repr  := nat.repr  to_root_nat

#eval pred 7 -- 6

end mynat

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:10):

Here I'm piggybacking on the implementation of has_repr for the root nat, but you can also implement it directly

view this post on Zulip Mario Carneiro (Sep 21 2020 at 16:10):

you just have to go through the trouble of turning numbers into strings in base 10 by repeated division

view this post on Zulip Thorsten Altenkirch (Sep 21 2020 at 16:12):

(deleted)

view this post on Zulip Thorsten Altenkirch (Sep 21 2020 at 16:14):

Mario Carneiro said:

namespace mynat

inductive nat : Type
| zero : nat
| succ : nat  nat

local notation `ℕ` := nat

open mynat.nat

example :  n : , zero  succ n :=
begin
  assume n h,
  contradiction,
end

def pred :   
| zero := zero
| (succ n) := n

def add :     
| zero b := b
| (succ a) b := succ (add a b)

instance : has_zero  := zero
instance : has_one  := succ zero
instance : has_add  := add

#reduce pred 7

end mynat

(I implemented add backwards for you :stuck_out_tongue_wink: )

Thanks a lot. However, I stick with the official lean definition of + to avoid confusion...

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 16:37):

I'm afraid you should only be accessing nat through its API, so you can't tell what the official definition is :-)

view this post on Zulip Thorsten Altenkirch (Sep 21 2020 at 16:47):

People tell me what I should do. I just had my 58th birthday yesterday and I was hoping that I am now old enough that people stop telling me how to behave.

I already got told off for saying brain damaged and destructive logic and now I am not allowed to redefine the natural numbers???

view this post on Zulip Johan Commelin (Sep 21 2020 at 16:49):

Too bad for you... this is the internet.

view this post on Zulip Johan Commelin (Sep 21 2020 at 16:49):

(Also, congrats with your birthday)

view this post on Zulip Thorsten Altenkirch (Sep 21 2020 at 17:01):

Johan Commelin said:

Too bad for you... this is the internet.

I am not sure what exactly it is. My impression is it is contemporary culture. People are easily offended these days.

view this post on Zulip Mario Carneiro (Sep 21 2020 at 17:05):

I thought giving people recommendations of what they should do (in a particular area) is the role of experts :shrug: You don't have to follow advice if you don't want to

view this post on Zulip Johan Commelin (Sep 21 2020 at 17:06):

I think people have been telling each other what to do since Adam and Eve (-;

view this post on Zulip Johan Commelin (Sep 21 2020 at 17:06):

But the internet is a very convenient place to do so :grinning:

view this post on Zulip Mario Carneiro (Sep 21 2020 at 17:10):

Regarding redefining nat: I wouldn't even call it inadvisable, at least for teaching purposes (consider that the natural numbers game is built around the idea of redefining nat), but you have to understand that some aspects of nat are baked into lean C++ (which is why they are defined in the lean core library and not in mathlib) so you won't be able to perfectly replicate all aspects with your own definition

view this post on Zulip Mario Carneiro (Sep 21 2020 at 17:12):

However, the kernel doesn't have any special support for nat, so from a foundational point of view your own mynat will be just as good. It's just in stuff around elaboration, printing and so on where you see nat being favored over its identical twins


Last updated: May 11 2021 at 22:14 UTC