redefining nat

Stream: new members

[Thorsten Altenkirch]

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]

I think open nat opened the global nat

[Mario Carneiro]

try open mynat.nat

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

Wouldn't that be giving bit0 and bit1lemmas?

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Thorsten Altenkirch]

(deleted)

[Thorsten Altenkirch]

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]

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

[Thorsten Altenkirch]

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]

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

[Johan Commelin]

(Also, congrats with your birthday)

[Thorsten Altenkirch]

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]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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