## Behind the curtain

`Nat`

is not alone. Inductive constructions can model a vast amount of mathematics.

We can create the propositions `True`

and `False`

using them.

As you can see both `False`

and `True`

are more basic than `Nat`

. With `False`

you have *no* ways of building it. With `True`

, you have exactly one: `intro`

.

When building a function `f : Nat → α`

, recursion told us we needed to specify a value of `f`

for each way we construct a `Nat`

: one for `zero`

and one for each `succ n`

. What does recursion look like here?

`False.elim`

allows us to prove anything from a proof of a `False`

. Why? Because when using recursion on `False`

, there is nothing to recurse over. This is exactly the same reasoning that exhibits a function $\varnothing \to X$ for any set. (The `match`

syntax expects terms so the proof uses the recursor `rec`

underlying it.)

We can also build `And`

and `Or`

using inductive types.

Here are proofs of `And.left`

and `And.right`

.

`Or.elim`

becomes just another name for recursion.

We can also model existential propositions using inductive types.

Even equality fits into a inductive construction.

As we know from shopping, lists are also built recursively.

We start with an empty list `nil`

and we build via `cons`

our list by adding one thing, `a:α`

, at a time.

As this is cumbersome, Lean allows for familiar notation for lists.

We have the `[]`

for the empty list and `a::as`

to append `a`

to the list `as`

.

We can build useful functions on `List`

using recursion

And we can prove results, like the additivity of length, under join.