Zulip Chat Archive

Stream: Is there code for X?

Topic: nat.rec?


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:14):

nat.rec is the primitive recursor for nat

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:15):

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

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:15):

it's basically one of peano's axioms

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Chase Norman (Oct 31 2020 at 21:19):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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