In coq, how to make the "induction n eqn: Hn" in such a way as not to spoil the inductive hypothesis?
When using induction, I would like to be able to hypothesize n = 0
and 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, I could do this with a help induction n eqn: Hn
, but this seems to screw 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?
source to share
Ooh, I think I got it!
Applying the inductive guess changes your goal from (P n) to (P (constructor n ')), so I think in general you can just match with the goal of making the equation n = construct n'.
Here's a tactic that I think does it:
(* 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
).
This 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.
source to share
Matt was almost right, you just forgot to generalize your purpose a little by remembering 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.
source to share
I'm not sure if this is any easier than what you did in the second try, but you can "remember" first 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
*)
source to share