Stream: new members

Topic: redefining nat

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,
end

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

#reduce (pred 7)

end mynat


Mario Carneiro (Sep 21 2020 at 16:00):

I think open nat opened the global nat

Mario Carneiro (Sep 21 2020 at 16:00):

try open mynat.nat

Mario Carneiro (Sep 21 2020 at 16:01):

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

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

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,
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⟩

#reduce pred 7

end mynat


(I implemented add backwards for you :stuck_out_tongue_wink: )

Yakov Pechersky (Sep 21 2020 at 16:04):

Wouldn't that be giving bit0 and bit1lemmas?

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

Mario Carneiro (Sep 21 2020 at 16:06):

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

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


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

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

(deleted)

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,
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⟩

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

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 :-)

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

Johan Commelin (Sep 21 2020 at 16:49):

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

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.

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

Johan Commelin (Sep 21 2020 at 17:06):

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

Johan Commelin (Sep 21 2020 at 17:06):

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

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

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