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?
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:
It works for my example: