我正在尝试确保将Coq提取到Haskell时会丢弃无用的东西Prop
。但是,当我使用以下示例时,我看到两者divides
和prime
都被提取为Haskell空类型。这是为什么?
(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
match p with
| 0 => false
| 1 => false
| S p' => (negb (helper p p'))
end.
(***********)
(* divides *)
(***********)
Definition divides (n p : nat) : Prop :=
exists (m : nat), ((mult m n) = p).
(*********)
(* prime *)
(*********)
Definition prime (p : nat) : Prop :=
(p > 1) /\ (forall (n : nat), ((divides n p) -> ((n = 1) \/ (n = p)))).
(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/some_file.hs" isPrime divides prime.
Run Code Online (Sandbox Code Playgroud)
这是divides
和发生的事情prime
:
type Divides = ()
type Prime = ()
Run Code Online (Sandbox Code Playgroud)
提取它们有什么用?
这是预期的行为。Prop
命题来自的命题意味着这些命题在计算上是不相关的,因为那里的命题是为了确保正确性,例如表示算法的前后条件,而不参与计算。
这种情况类似于静态类型语言的类型-人们通常希望从运行时中删除类型。在这里,我们也希望删除证明的术语。
Coq的类型系统对此提供了支持,该系统禁止将逻辑信息从类型输入Prop
到Type
,例如
Definition foo : True \/ True -> nat :=
fun t => match t with
| or_introl _ => 0
| or_intror _ => 42
end.
Run Code Online (Sandbox Code Playgroud)
结果是
Run Code Online (Sandbox Code Playgroud)Error: Incorrect elimination of "t" in the inductive type "or": the return type has sort "Set" while it should be "Prop". Elimination of an inductive object of sort Prop is not allowed on a predicate in sort Set because proofs can be eliminated only to build proofs.
一个自然的问题出现了:
因此,理想情况下
divides
,prime
应该从提取的文件中将其完全删除,对吗?它们为什么在那里存在?
正如Pierre Letouzey 在Coq提取概述中所解释的:
现在让我们总结一下Coq提取的当前状态。在[7]中描述的理论提取函数仍然有用,并且被用作提取系统的核心。此函数折叠(但不能完全删除)逻辑部分(以sort形式存在
Prop
)和类型。完全删除会在条款评估中引起危险的更改,甚至在某些情况下甚至可能导致错误或不终止。