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