Induction on pnat

Stream: new members

[Maxime Darrin]

Hi,

I have a function pnat -> pnat and I need to perform an induction to prove a prop on it, however pnat is not an inductive type so I figured I should use a variable in N, and cast it to pnat using nat.to_pnat' but it is actually not easy to work with that function everywhere.

So is there a better way to perform an induction on pnat ?

[Kyle Miller]

Someone's proved induction principles for pnat, so you don't have cast tonat here. Check out docs#pnat.strong_induction_on and the next few lemmas.

[Eric Wieser]

Pnat is an inductive type, and if you do induction on it you'll get a nat you can then do normal nat induction on

[Eric Wieser]

But @Kyle Miller's suggestion does those messy bits for you

[Kyle Miller]

Inductive type definitions are a way to get a bunch of useful axioms and constructors automatically, but you can construct your own types out of other inductive types then define your own 'axioms' and constructors, where the 'axioms' are actually theorems you prove. For pnat, you can think of 1 : pnat and (+1) : pnat -> pnat as being the constructors, and docs#pnat.rec_on as being the recursion/induction principle. This lets you forget how exactly pnat is defined.

[Eric Rodriguez]

I'd personally just avoid pnat if possible and use either (n+1) everywhere, or a hypothesis that n > 0

[Eric Rodriguez]

It's usually not worth the hassle

[Kyle Miller]

As @Eric Wieser said, pnat is actually an inductive type (as docs#subtype), but I think you're meant to not take advantage of this fact -- it's an implementation detail. (But never taking advantage of it seems like a hassle...)

[Eric Rodriguez]

if you want the standard induction, there's also docs#pnat.rec_on

[Eric Rodriguez]

(deleted)