# Zulip Chat Archive

## Stream: new members

### Topic: Natural Number Game definition of +

#### Liam Axon (Aug 23 2021 at 17:17):

I have been going through the Natural Numbers Game in order to get into LEAN, but I came across the definition of + in the natural numbers and I am a bit confused. Why can we define this operation inductively? Using only the three "properties" given to me by the game so far (0 : mynat, succ : mynat -> mynat, induction), I don't get why + : mynat -> mynat must exist, or even why it is well-defined.

I guess my question is: Given only these three "properties" of mynat, are inductively defined functions like + well-defined, and if not, what else must be added to mynat in order to define/create/prove-to-exist a function like + in LEAN?

#### Martin Dvořák (Aug 23 2021 at 17:21):

If I am not mistaken, is is not `+ : mynat -> mynat`

. It should be `+ : mynat -> mynat -> mynat`

instead.

#### Martin Dvořák (Aug 23 2021 at 17:30):

You can see the full definition of the operation `+`

on the type `mynat`

here:

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/mynat/add.lean

#### Martin Dvořák (Aug 23 2021 at 17:33):

If you want to understand why the operation `+`

is well-defined, focus on these three lines:

```
def add : mynat → mynat → mynat
| m 0 := m
| m (succ n) := succ (add m n)
```

The syntactic sugar for replacing `add x y`

by `x + y`

is done somewhere else; it is not important here.

#### Martin Dvořák (Aug 23 2021 at 17:37):

By being "well-defined", you mean that the expansion (the chain of substitutions according to the definition) ends somewhere? Or are you asking about why the formal definition (`mynat.definition`

) corresponds to our notion of adding natural numbers correctly?

#### Martin Dvořák (Aug 23 2021 at 17:55):

In order to understand how `mynat`

work, start with the definition here:

https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/mynat/definition.lean

```
inductive mynat
| zero : mynat
| succ (n : mynat) : mynat
```

You can see that the following terms all satisfy the definition of `mynat`

:

`zero`

, `succ(zero)`

, `succ(succ(zero))`

, `succ(succ(succ(zero)))`

The crucial thing is that every term of the type `mynat`

is either `zero`

or `succ n`

for some `n : mynat`

. Therefore, you can patternmatch on them in the definition of any operation on `mynat`

. If you cover both cases (i.e., that the argument is either `zero`

or `succ n`

), then nothing will surprise you. The result will be well-defined as long as the right side of the definition is written well.

#### Eric Rodriguez (Aug 23 2021 at 17:57):

basically, this is guaranteed by `rec`

, a function on all inductive types. handwavily, `rec`

guarantees that if you cover all constructors, you can make an inductive definition of not only properties, but data.

for example, think of this inductive type:

```
inductive Enum
| Blue : Enum
| Red : Enum
| Yellow : Enum
```

If you have `f Blue`

, `f Red`

and `f Yellow`

then definitely you have `f x`

for any `x : Enum`

. this is pretty much the signature for `Enum.rec`

:

```
protected eliminator Enum.rec : Π {motive : Enum → Sort l}, motive Enum.Blue → motive Enum.Red → motive Enum.Yellow → Π (n : Enum), motive n
```

Now, on top of that, if you have a `self-referential`

type, like `mynat`

, you also get given the value at that point. that's because the function was "already defined there" - how could you have constructed the value if not?*. So for example, for the standard definition of `ℕ`

, this is `rec`

:

```
protected eliminator nat.rec : Π {motive : ℕ → Sort l}, motive 0 → (Π (n : ℕ), motive n → motive n.succ) → Π (n : ℕ), motive n
```

Now, say `motive`

is `ℕ → (ℕ → ℕ)`

(like addition - remember that → is right-associative in Lean), then you need `addition 0`

, (which is the identity function, and given `addition n`

, you need to create `addition (n+1)`

(that is, `λ x, x+1`

).

Now, the reason this is actually well-defined (and why I starred things) is because you do actually have some constraints (I've always seem then referred as "positivity constraints") on inductive types; for example, this isn't valid:

```
inductive bad : Type*
| no : (bad → ℕ) → bad
```

because `rec`

would cause nonsense (I don't have the thinking to cause an explicit contradiction, sadly, but I know some people here know it). But `rec`

is really super cool; for example, see docs#is_solvable_by_rad. Also, for some thinking; what do you think `false.rec`

is? (`false`

is the empty inductive type)

#### Liam Axon (Aug 23 2021 at 17:57):

Thanks @Martin Dvořák , I did mean + : mynat -> mynat -> mynat.

#### Martin Dvořák (Aug 23 2021 at 18:01):

Read also the answer by @Eric Rodriguez. He explains how the inductive types work in general.

#### Liam Axon (Aug 23 2021 at 18:03):

It does looks like rec is what I was looking for :). But, I still have a question about defining the "add" function, though. I guess I'm not seeing why mynat fits the necessary constraints.

#### Martin Dvořák (Aug 23 2021 at 18:04):

Lemme give you an example, ok? Do you understand the representation that e.g. the number 3 is represented by `succ(succ(succ(zero)))`

and so on?

#### Liam Axon (Aug 23 2021 at 18:05):

Yeah, that makes sense to me.

#### Martin Dvořák (Aug 23 2021 at 18:06):

Good. Suppose you want to compute `3 + 2`

.

#### Martin Dvořák (Aug 23 2021 at 18:06):

Syntactically, this expresses `mynat.add 3 2`

to be clear.

#### Liam Axon (Aug 23 2021 at 18:07):

We can do this by 3 + 2 = succ(3 + 1) = succ(succ(3 + 0))...

#### Martin Dvořák (Aug 23 2021 at 18:07):

Yes.

#### Martin Dvořák (Aug 23 2021 at 18:08):

We are starting with `add succ(succ(succ(zero))) succ(succ(zero))`

. This gets replaced by `succ (add succ(succ(succ(zero))) succ(zero))`

.

#### Martin Dvořák (Aug 23 2021 at 18:09):

This in turn gets replaced by `succ (succ (add succ(succ(succ(zero))) zero))`

.

#### Liam Axon (Aug 23 2021 at 18:09):

Thank makes sense, thank you :). But... this only works if every number has only one pre-successor, right?

#### Martin Dvořák (Aug 23 2021 at 18:09):

Finally we have `succ (succ (succ(succ(succ(zero))) ))`

.

#### Martin Dvořák (Aug 23 2021 at 18:10):

Are you interested in other-than-standard model of natural numbers? Or what are you asking about now?

#### Liam Axon (Aug 23 2021 at 18:12):

Yeah, I guess I am asking about other models.

#### Eric Rodriguez (Aug 23 2021 at 18:12):

Liam Axon said:

Thank makes sense, thank you :). But... this only works if every number has only one pre-successor, right?

inductive types aren't like PA where you can have junk

#### Eric Rodriguez (Aug 23 2021 at 18:12):

they're guaranteed to be sufficient but only just

#### Eric Rodriguez (Aug 23 2021 at 18:12):

no non-standard number nonsense

#### Martin Dvořák (Aug 23 2021 at 18:12):

By definition

```
inductive mynat
| zero : mynat
| succ (n : mynat) : mynat
```

every number except zero has exactly one predecessor. The term `t : mynat`

is either `t = zero`

or `t = succ n`

for some `n : mynat`

. It cannot be anything else.

#### Liam Axon (Aug 23 2021 at 18:15):

Thank you! That clears things up. I didn't see that part of the definition

#### Liam Axon (Aug 23 2021 at 18:15):

*And, I wouldn't have known what it meant if I had, so thanks for explaining it to me :)

#### Martin Dvořák (Aug 23 2021 at 18:15):

You're always welcome!

Last updated: Dec 20 2023 at 11:08 UTC