# Zulip Chat Archive

## 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,
contradiction,
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,
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: )

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

Wouldn't that be giving `bit0`

and `bit1`

lemmas?

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

#### Thorsten Altenkirch (Sep 21 2020 at 16:12):

(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, 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...

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

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

(Also, congrats with your birthday)

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