7

我通过阅读“Certified Programming with Dependent Types”一书来学习 Coq，但我在理解forall语法时遇到了麻烦。

作为一个例子，让我们考虑一下这种相互归纳的数据类型：（代码来自书中）

Inductive even_list : Set :=
| ENil : even_list
| ECons : nat -> odd_list -> even_list

with odd_list : Set :=
| OCons : nat -> even_list -> odd_list.

和这个相互递归的函数定义：

Fixpoint elength (el : even_list) : nat :=
  match el with
  | ENil => O
  | ECons _ ol => S (olength ol)
  end

with olength (ol : odd_list) : nat :=
  match ol with
  | OCons _ el => S (elength el)
  end.

Fixpoint eapp (el1 el2 : even_list) : even_list :=
  match el1 with
  | ENil => el2
  | ECons n ol => ECons n (oapp ol el2)
  end

with oapp (ol : odd_list) (el : even_list) : odd_list :=
  match ol with
  | OCons n el' => OCons n (eapp el' el)
  end.

我们生成了归纳方案：

Scheme even_list_mut := Induction for even_list Sort Prop
with odd_list_mut    := Induction for odd_list Sort Prop.

现在我不明白的是，从even_list_mut我可以看到它需要 3 个参数的类型：

even_list_mut
     : forall (P : even_list -> Prop) (P0 : odd_list -> Prop),
       P ENil ->
       (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) ->
       (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) ->
       forall e : even_list, P e

但为了应用它，我们需要为其提供两个参数，并将目标替换为 3 个前提（for和P ENilcase ）。forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)forall (n : nat) (e : even_list), P e -> P0 (OCons n e)

所以它实际上得到了 5 个参数，而不是 3 个。

但是当我们想到这种类型时，这个想法就失败了：

fun el1 : even_list =>
  forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2
       : even_list -> Prop

和

fun el1 el2 : even_list => elength (eapp el1 el2) = elength el1 + elength el2
     : even_list -> even_list -> Prop

谁能解释forall语法是如何工作的？

谢谢，

4

1 回答 1

7

实际上，even_list_mut需要 6 个参数：

even_list_mut
 : forall
     (P : even_list -> Prop)                                      (* 1 *)
     (P0 : odd_list -> Prop),                                     (* 2 *)
     P ENil ->                                                    (* 3 *)
     (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) ->  (* 4 *)
     (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> (* 5 *)
     forall e : even_list,                                        (* 6 *)
     P e

您可以将箭头视为语法糖：

A -> B
===
forall _ : A, B

所以你可以这样重写even_list_mut：

even_list_mut
 : forall
     (P  : even_list -> Prop)
     (P0 : odd_list -> Prop)
     (_  : P ENil)
     (_  : forall (n : nat) (o : odd_list), P0 o -> P (ECons n o))
     (_  : forall (n : nat) (e : even_list), P e -> P0 (OCons n e))
     (e : even_list),
     P e

有时当你应用这样一个术语时，一些参数可以通过统一推断出来（将术语的返回类型与你的目标进行比较），所以这些参数不会成为目标，因为 Coq 已经弄清楚了。例如，假设我有：

div_not_zero :
  forall (a b : Z) (Anot0 : a <> 0), a / b <> 0

我把它应用到目标42 / 23 <> 0上。Coq 能够弄清楚aought to be42和bought to be 23。剩下的唯一目标就是证明42 <> 0。但实际上，Coq 隐含地将42and23作为参数传递给div_not_zero.

我希望这有帮助。

编辑1：

回答您的附加问题：

fun (el1 : even_list) =>
  forall (el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2
: even_list -> Prop

是一个参数的函数，el1 : even_list，它返回类型forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2。非正式地，给定一个 list el1，它构造语句for every list el2, the length of appending it to el1 is the sum of its length and el1's length。

fun (el1 el2 : even_list) =>
  elength (eapp el1 el2) = elength el1 + elength el2
: even_list -> even_list -> Prop

是一个有两个参数el1 : even_list和的函数el2 : even_list，它返回类型elength (eapp el1 el2) = elength el1 + elength el2。非正式地，给定两个列表，它构造语句for these particular two lists, the length of appending them is the sum of their length。

注意两件事： - 首先我说的是“构造语句”，这与“构造语句的证明”非常不同。这两个函数只返回类型/命题/陈述，可能是真或假，可能是可证明的或不可证明的。- 第一个，一旦输入一些 list el1，返回一个非常有趣的类型。如果您有该陈述的证明，您就会知道对于 的任何选择el2，附加它el1的长度是长度的总和。

实际上，这是要考虑的另一种类型/语句：

forall (el1 el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2
: Prop

该语句表示对于任何两个列表，附加的长度是长度的总和。

可能让您感到困惑的一件事是，这正在发生：

fun (el1 el2 : even_list) =>
  (* some proof of elength (eapp el1 el2) = elength el1 + elength el2 *)

是一个术语，其类型为

forall (el1 el2 : even_list),
  elength (eapp el1 el2) = elength el1 + elength el2

这是一个类型为的语句

Prop

所以你看到了，这fun是forall两件相关但非常不同的事情。事实上，形式的一切fun (t : T) => p t都是一个术语，其类型是forall (t : T), P t，假设p t有 类型P t。

因此，当您编写以下内容时会出现混淆：

fun (t : T) => forall (q : Q), foo
               ^^^^^^^^^^^^^^^^^^^
               this has type  Prop

因为这有类型：

forall (t : T), Prop (* just apply the rule *)

所以forall确实可以出现在两种情况下，因为这种微积分能够计算类型。因此，您可能会forall在计算中看到（这暗示了这是一个类型构建计算的事实），或者您可能会在类型中看到它（这是您通常看到的地方）。但forall对于所有意图和目的来说都是一样的。另一方面，fun仅出现在计算中。

于 2013-07-04T09:57:31.463 回答