在coq中,如何以一种不会破坏归纳假设的方式进行“归纳法：Hn”？

2019年8月6日 182次阅读

当使用归纳时,我想假设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.

从理论上讲,我可以通过感应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.

有没有一种简单的方法来获得我想要的东西？

最佳答案 噢,我想我想通了！

应用归纳假设会将您的目标从(P n)改为(P(构造函数n’)),因此我认为通常您可以匹配目标来创建等式n =构造n’.

这是我认为这样做的策略：

(* 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
  ).

它适用于我的例子：

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.
点赞