我正在通过阅读"使用依赖类型的认证编程"一书来学习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仅出现在计算中.