在 coq 中，如何以不搞乱归纳假设的方式进行“归纳 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 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
    *)