Coq -理解“`forall`”语法

Question

我正在通过阅读“带有依赖类型的认证编程”一书来学习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只出现在计算中。