# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: nat.rec?

#### Chase Norman (Oct 31 2020 at 21:14):

I've reached the point in a proof where my goal contains `nat.rec`

. I've looked on the mathlib documentation and can't find any theorems or equations that reference it. I've searched for it's definition and it just takes me back to `nat`

. I've tried to `unfold`

it, also to no avail. `hint`

and `suggest`

don't show relevant theorems. What does `nat.rec`

mean and what options do I have to prove statements using it? I understand it has to do with recursive applications of a function, which may be very useful to my proof.

#### Mario Carneiro (Oct 31 2020 at 21:14):

`nat.rec`

is the primitive recursor for nat

#### Mario Carneiro (Oct 31 2020 at 21:15):

it has no definition as it is part of the axiomatization of nat itself

#### Mario Carneiro (Oct 31 2020 at 21:15):

it's basically one of peano's axioms

#### Mario Carneiro (Oct 31 2020 at 21:16):

To prove statements about it, you should probably do induction on the last argument (the `nat`

), as `nat.rec z s (succ n) = s n (nat.rec z s n)`

and `nat.rec z s 0 = z`

are definitionally true

#### Mario Carneiro (Oct 31 2020 at 21:16):

*However*, it is overwhelmingly more likely that you have unfolded far too much and should step back a couple steps to get unstuck

#### Mario Carneiro (Oct 31 2020 at 21:18):

To properly #xy your problem I would need to see the context in which your nat.rec goal arose. #mwe?

#### Chase Norman (Oct 31 2020 at 21:19):

Thanks for your advice. What tactic could use these definitional truths? `change`

?

#### Mario Carneiro (Oct 31 2020 at 21:19):

you can use change, as well as `exact`

or `apply`

or just ignoring the difference and using nothing

#### Mario Carneiro (Oct 31 2020 at 21:20):

lean's unification works modulo defeq, so if two things are defeq they are essentially interchangeable without any explicit tactic application

#### Mario Carneiro (Oct 31 2020 at 21:21):

The issue with using `change`

is that it's actually somewhat annoying to write a `nat.rec`

term explicitly because there is an implicit argument, the "motive" `C`

, that often can't be inferred from the context of use

#### Mario Carneiro (Oct 31 2020 at 21:22):

one more reason you should do less unfolding and go back to the recursive function you started with

Last updated: May 17 2021 at 15:13 UTC