induction

Stream: lean4

[Chenyi Li]

I wonder how to what is the code to do induction on k of the type $k : \mathbb{N}+$. In mathematics, we prove for $k=1$, and assume the result holds for $k = j$ and prove $k=j+1$. Thank you very much!

[Scott Morrison]

There is src#PNat.recOn.

[Chenyi Li]

Thank you very much! I would try this!

[Scott Morrison]

It is marked as @[elab_as_elim], so I think you can just write induction k in tactic mode.

[Alex J. Best]

It needs to be tagged as @[eliminator] for that to work, elab as elim just changes the elaboration order.
Fortunately you can just add attribute [eliminator] PNat.recOn in your own file and it works fine.
Last I checked mathlib didn't have too many theorems (defs) tagged as eliminator. I'd be happy to see some more!