how do the natural numbers work in Lean?

Stream: new members

[Emily Riehl]

I'm familiar with how the natural numbers work in dependent type theory (as an inductive type generated by 0 and succ). I understand how to use the elimination rule to define addition and multiplication and so on and prove the two redundant Peano axioms (that 0 is not a successor and that the successor function is injective).

What I don't understand is why I can prove so many things about natural numbers using rfl. Examples include:

rfl : 5 * (3 + 4) = (4 + 3) * 5
fun _ => rfl : ∀ n : Nat, succ n = n + 1
fun _ => rfl : ∀ n : Nat, n + 0 = n
fun _ _ => rfl : ∀ m n : Nat, m + succ n = succ (m + n)

The last two of these I'd expect from the definition of addition using induction in the second variable, and I suppose this explains the second equality as well. The equalities like the first involving explicit numerals are the most mysterious to me.

Can someone explain when an equality of natural numbers is provable using rfl? I think the answer may have something to do with normal forms (but I don't really understand what these are).

[Aaron Liu]

what about

• rfl : 0 = Nat.zero
• rfl : 1 = Nat.succ 0
• rfl : 2 = Nat.succ 1

etc.

Is this understandable to you?

[Rado Kirov]

What I don't understand is why I can prove so many things about natural numbers using rfl

Not an expert at all, but my understanding is that at the core there is a lambda calculus evaluator, that does reduction by default (weak head normal form more specifically, which I forget exactly what it means). So when you have explicit numerals, it can run the reducer (which it can't do when it has variables like x). What happens is that both 5 * (3 + 4) and (4 + 3) * 5 turn into 35 first (internally this is 35 succ in a row, but actually likely represented more efficiently), and then rfl closes with 35 = 35.

[Rado Kirov]

The second example also works like that because 1 is alias for succ zero, and the definition of + can be reduced when it has something with succ _ in the second argument. But note that succ n = 1 + n doesn't reduce on the RHS hence rfl can't solve it, one needs to use some theorems to rewrite it.

[Emily Riehl]

Aaron Liu said:

what about

• rfl : 0 = Nat.zero
• rfl : 1 = Nat.succ 0
• rfl : 2 = Nat.succ 1

etc.

Is this understandable to you?

My guess is that this is how 0, 1, and 2 are defined.

So I guess your point is that 3 + 4 is defined to be

0.succ.succ.succ + 0.succ.succ.succ.succ

which is definitionally equal to

(3 + 0).succ.succ.succ.succ

which is definitionally equal to

0.succ.succ.succ.succ.succ.succ.succ

and I can do a similar reduction of 4 + 3. Because both reduce to the same numeral they are equal by rfl?

[Emily Riehl]

Is there an upper bound for how high the explicit numerals in Lean go?

[Aaron Liu]

Emily Riehl said:

Is there an upper bound for how high the explicit numerals in Lean go?

Well eventually it's gonna run out of memory I guess

[Aaron Liu]

Lean actually has special support for reducing common operations on numeric literals

[Aaron Liu]

your reasoning justifies this reduction in theory so in practice since we know it's gonna reduce anyways why don't we just replace it with a more efficient implementation

[Aaron Liu]

so you can see the implementation of docs#Lean.Meta.reduceNat? has a list of special-cased operations

[Rado Kirov]

Is there an upper bound for how high the explicit numerals in Lean go?

https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nat has a comment about this

GMP would mean there is no limit (other than your computer memory), similarly to say Python, or BigInt in JS.

[Rado Kirov]

Custom Nats like if you write inductive MyNat ... likely don't have that optimization and will quickly make Lean grind to a halt.

[Emily Riehl]

Thanks. This is helpful.

[Kevin Buzzard]

In NNG3 this behaviour confused users; I would get bug reports saying "the goal was n+0=n and I know I'm supposed to rw add_zero, next but I put rfl and it worked". So in NNG4 I define addition as an undefined function and define add_zero and add_succ as axioms.