Coq -- 理解 `forall` 语法

Question

我正在通过阅读“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 个前提替换目标(对于 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) 情况)。

所以它就像它实际上获得了 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语法工作？

谢谢，

Answer 1

事实上，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 能够计算出 a应该是 42和 b应该是 23 .剩下的唯一目标就是证明 42 <> 0 .但确实，Coq 隐式传递了 42和 23作为 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 .非正式地，给出一个列表 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 .

注意两点:
- 首先我说“构造陈述”，这与“构造陈述的证明”非常不同。这两个函数只返回类型/命题/陈述，可能是真或假，可能是可证明的或不可证明的。
- 第一个，曾经喂过一些列表 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只出现在计算中。