In coq, how to do "induction n eqn: Hn" in a way that doesn't mess up the inductive hypothesis?

Question

When using induction, I'd like to have hypotheses n = 0 and n = S n' to separate the cases.

Section x.
  Variable P : nat -> Prop.
  Axiom P0: P 0.
  Axiom PSn : forall n, P n -> P (S n).

  Theorem Pn: forall n:nat, P n.
  Proof. intros n. induction n.
   - (* = 0 *) 
     apply P0. 
   - (* = S n *)
     apply PSn. assumption.
  Qed.

In theory I could do this with induction n eqn: Hn, but that seems to mess up the inductive hypothesis:

  Theorem Pn2: forall n:nat, P n.
  Proof. intros n. induction n eqn: Hn.
   - (* Hn : n = 0 *) 
     apply P0. 
   - (* Hn : n = S n0 *)
     (*** 1 subgoals
      P : nat -> Prop
      n : nat
      n0 : nat
      Hn : n = S n0
      IHn0 : n = n0 -> P n0
      ______________________________________(1/1)
      P (S n0)
     ****)
  Abort.
End x.

Is there an easy way to get what I want here?

Answer 1

I'm not sure if this is any easier, than what you have done in your second attempt, but you can first "remember" n.

 Theorem Pn: forall n:nat, P n.
 Proof. intro n. remember n. induction n.
 - (*P : nat -> Prop
     n0 : nat
     Heqn0 : n0 = 0
     ============================
     P n0
    *)
    subst. apply P0.
 - (* P : nat -> Prop
      n : nat
      n0 : nat
      Heqn0 : n0 = S n
      IHn : n0 = n -> P n0
      ============================
      P n0
    *)

Answer 2

Ooo, I think I figured it out!

Applying the inductive hypothesis changes your goal from (P n) to (P (constructor n')), so I think in general you can just match against the goal to create the equation n = construct n'.

Here's a tactic that I think does this:

(* like set (a:=b) except introduces a name and hypothesis *)
Tactic Notation 
    "provide_name" ident(n) "=" constr(v)
       "as" simple_intropattern(H) :=
    assert (exists n, n = v) as [n H] by (exists v; reflexivity).

Tactic Notation
  "induction_eqn" ident(n) "as" simple_intropattern(HNS)
    "eqn:" ident(Hn) :=
  let PROP := fresh in (
    pattern n;
    match goal with [ |- ?FP _ ] => set ( PROP := FP ) end;
    induction n as HNS;
    match goal with [ |- PROP ?nnn ] => provide_name n = nnn as Hn end;
    unfold PROP in *; clear PROP
  ).

It works for my example:

Theorem Pn_3: forall n:nat, P n.
Proof.
  intros n.
  induction_eqn n as [|n'] eqn: Hn.
  - (* n: nat, Hn: n = 0; Goal: P 0 *)
    apply P0.
  - (* n': nat, IHn': P n';
       n: nat, Hn: n = S n'
       Goal: P (S n') *)
    apply PSn. exact IHn'.
Qed.

Answer 3

Matt was almost right, you just forgot to generalize a bit your goal by reverting the remembered n:

Theorem Pn2: forall n:nat, P n.
  Proof. intros n. remember n. revert n0 Heqn0.
  induction n as [ | p hi]; intros m heq.
  - (* heq : n = 0 *)  subst. apply P0. 
  - (* heq : n = S n0 *)
    (* 
  1 subgoal
  P : nat -> Prop
  p : nat
  hi : forall n0 : nat, n0 = p -> P n0
  m : nat
  heq : m = S p
  ______________________________________(1/1)
  P m
  *) subst; apply (PSn p). apply hi. reflexivity.