coq - Coq —了解 `forall`语法

我正在通过阅读《依赖类型的认证编程》一书来学习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语法如何工作？

谢谢，

最佳答案

实际上，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。另一方面，ojit_code仅出现在计算中。

关于coq - Coq —了解 `forall`语法，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/17466817/