Natural Number Game definition of +

Stream: new members

[Liam Axon]

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]

If I am not mistaken, is is not + : mynat -> mynat. It should be + : mynat -> mynat -> mynat instead.

[Martin Dvořák]

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]

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]

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]

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]

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]

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

[Martin Dvořák]

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

[Liam Axon]

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]

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]

Yeah, that makes sense to me.

[Martin Dvořák]

Good. Suppose you want to compute 3 + 2.

[Martin Dvořák]

Syntactically, this expresses mynat.add 3 2 to be clear.

[Liam Axon]

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

[Martin Dvořák]

Yes.

[Martin Dvořák]

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]

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

[Liam Axon]

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

[Martin Dvořák]

Finally we have succ (succ (succ(succ(succ(zero))) )).

[Martin Dvořák]

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

[Liam Axon]

Yeah, I guess I am asking about other models.

[Eric Rodriguez]

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]

they're guaranteed to be sufficient but only just

[Eric Rodriguez]

no non-standard number nonsense

[Martin Dvořák]

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]

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

[Liam Axon]

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

[Martin Dvořák]

You're always welcome!