coq - 在 coq 中，如何以不破坏归纳假设的方式执行 "induction n eqn: Hn"？

Question

使用归纳法时，我想有假设n = 0和 n = S n'分开案件。

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.

理论上我可以用 induction n eqn: Hn 做到这一点，但这似乎扰乱了归纳假设:

  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.

有没有一种简单的方法可以在这里得到我想要的东西？

Answer 1

马特几乎是对的，你只是忘记通过恢复内存来概括你的目标 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.