nat.rec?

Stream: Is there code for X?

[Chase Norman]

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]

nat.rec is the primitive recursor for nat

[Mario Carneiro]

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

[Mario Carneiro]

it's basically one of peano's axioms

[Mario Carneiro]

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]

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]

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

[Chase Norman]

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

[Mario Carneiro]

you can use change, as well as exact or apply or just ignoring the difference and using nothing

[Mario Carneiro]

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

[Mario Carneiro]

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]

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