理解 nat_ind2 的逻辑基础

Question

作为 nat 的另一种归纳原理，

nat_ind2

定义如下：

Definition nat_ind2 :
  forall (P : nat -> Prop),
  P 0 ->
  P 1 ->
  (forall n : nat, P n -> P (S(S n))) ->
  forall n : nat , P n :=
    fun P => fun P0 => fun P1 => fun PSS =>
      fix f (n:nat) := match n with
                         0 => P0
                       | 1 => P1
                       | S (S n') => PSS n' (f n')
                       end.

如果我的 IDE 没有错误，函数

f

的类型为

nat -> nat

。但我认为

PSS

在其第二个参数中需要

P n

类型的内容，那么为什么

f

的类型如此呢？

另外，有没有办法将 nat_ind2 定义为

Fixpoint

？我试过这个：

Fixpoint nat_ind (P : nat -> Prop) (P0 : P 0) (P1 : P 1) 
  (PSS : forall n : nat, P n -> P (S (S n))) (n : nat) :=
  fix PK := 
  match n with
  | 0 => P0
  | 1 => P1
  | S (S k) => PSS k (PK k)
  end.

但这不起作用。我认为主要的困难是无法注释

PK

以采用正确的类型（

P k

）。我对 coq 还很陌生，所以可能缺少一些东西。

编辑：我对

f

的类型如何适应该命题感到困惑。

f

没有出现在任何地方吗？因为在 nat_ind2 的类型中，

PSS

和

(n:nat)

（对应于

forall n: nat,...

）之间没有任何内容。无论如何，总的来说，只是很困惑

Answer 1

使用最近的 Coq (8.18)，你可以写：

Fixpoint nat_ind2 (P : nat -> Prop) (P0 : P 0) (P1 : P 1) 
  (PSS : forall n : nat, P n -> P (S (S n))) (n : nat) :=
  match n with
  | 0 => P0
  | 1 => P1
  | S (S k) => PSS k (nat_ind2 P P0 P1 PSS k)
  end.

About nat_ind2.

这给出了

nat_ind2 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n

我认为这并不总是可能的——随着时间的推移，修复点的一致性检查器已经得到了改进。

但是使用上面更复杂的设计和局部固定点是有原因的：您可以只传递一个变化的参数，并让所有其他参数远离外部函数。如果函数用于计算，这确实会产生性能/堆栈空间差异，但对于通常仅在不透明证明中使用的归纳原理，这不会产生差异，恕我直言，没有本地固定点定义的更简单的变体是更好的。