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

when using induction, i'd have hypotheses n = 0 , n = s n' separate 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 induction n eqn: hn, seems mess 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 easy way want here?

ooo, think figured out!

applying inductive hypothesis changes goal (p n) (p (constructor n')), think in general can match against goal create equation n = construct n'.

here's tactic think this:

(* set (a:=b) except introduces name , hypothesis *) tactic notation      "provide_name" ident(n) "=" constr(v)        "as" simple_intropattern(h) :=     assert (exists n, n = v) [n h] (exists v; reflexivity).  tactic notation   "induction_eqn" ident(n) "as" simple_intropattern(hns)     "eqn:" ident(hn) :=   let prop := fresh in (     pattern n;     match goal [ |- ?fp _ ] => set ( prop := fp ) end;     induction n hns;     match goal [ |- prop ?nnn ] => provide_name n = nnn hn end;     unfold prop in *; clear prop   ). 

it works example:

theorem pn_3: forall n:nat, p n. proof.   intros n.   induction_eqn n [|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.