在coq中定义一个多态类型

Question

所以我正在做一个学习 coq 的练习。我试图根据这种编码定义一个类型： forall X.(X -> X) -> X -> X;`这是来自 Alonzo Church（他提出了自然数的编码）如下：

0 , f:x:x

1 , f:x:fx

2 , f:x:f(fx)

3 , f:x:f(f(fx))

.....

n , f:x:fnx:

我的代码如下：

Definition nat := forall X : Type, (X -> X) -> X -> X.

这个练习要求我定义表达式 0、1、2 和 3，它们将对应的数字编码为 nat 的元素： 以下是我认为的结果

Definition zero : nat :=
  fun (X : Type) (f : X -> X) (x : X) => x.
Definition one : nat := 
  fun (X : Type) (f : X -> X) (x : X) => f x.
Definition two : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f (f x).
Definition three : nat :=
  fun (X:Type)(f: X -> X)(x: X) => f ( f ( f x )).

我的问题是我需要证明 plus n one = succ n。 n 是我定义的类型 Nat

我有一个如下定义的 succ 函数：

Definition succ (n : nat) : nat :=
fun (X : Type) (f : X -> X) (x : X) => f (n X f x).

my plus 函数定义如下：

Definition plus (n m : nat) : nat :=
fun (X : Type) (f : X -> X) (x : X) => (n X f (m X f x)).

问题是当我试图证明 plus n one = succ n 时，我卡在了中间，不知道如何证明。 代码如下：

Theorem plus_succ: forall (n : nat),
  plus n one = succ n.
Proof.
  intros.

1 个子目标 ñ：自然 ______________________________________(1/1) 加n一=成功n

而且我无法进行反转或任何其他策略......（我是 Coq 新手，到目前为止我已经学习了列表、多边形、归纳和策略）

这让我想到，我上面定义的一个、两个或所有定义可能都不准确。 如果有人可以帮助我或给我一些提示，将不胜感激！谢谢！

Answer 1

在 Coq 中使用 Church 编码本身并不是一个坏主意，但你不能对这种类型的居民说太多（除了像你一样构建其中的一些）。

第一个问题是这种 Church 编码的居民是函数，并且您将能够证明两个函数在纯 Coq 中是相等的，前提是它们计算为相同的值（直到展开、beta 缩减、缩减匹配和修复）。 plus n one 和 succ n 不是这种情况：您在左轴 fun X f x => f (n X f x) 和右轴 fun X f x => n X f (f x) 上。您可能希望证明的是forall (X : type) (f : X -> X) (x : X), f (n X f x) = n X f (f x)，然后您需要使用functional extensionality，这是一个公理，指出函数之间的相等性由函数在其域的每个点的值决定（参见Coq.Logic.FunctionalExtensionality in有关该点的更多详细信息，请参阅标准库）。这个公理经常被假设，但它也不是无辜的（例如，它确实阻止了计算）。

您将遇到的第二个问题是您希望 nat = forall X, (X -> X) -> X -> X 的居民在他们的第一个参数 X : Type 中成为参数函数，但实际上并没有强制执行此操作。实际上，如果您假设其他公理，例如排除-中间，您可以构建非参数居民。在纯 Coq（没有任何公理）中，Bernardy 和 Lasson 的结果表明，确实所有 nat 类型的居民 都是参数化的，但是您不能内化这个结果。如果没有参数，你就没有子弹来证明诸如f (n X f x) = n X f (f x) 之类的方程。

所以你的烦恼来自这两个问题：

1. 在没有函数可扩展性的情况下，您可以证明的函数之间的等式非常有限，并且
2. 您无法在纯 Coq 中内部表达对类型的量化是参数化的。

如果您想详细了解这些参数化问题以及使用 Church 编码（或这些编码的变体）仍然可以实现什么，我建议您查看 Chlipala 的 Parametric Higher-Order Abstract Syntax。