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

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


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

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?

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