从Coq提取道具到Haskell导致空类型

Ore*_*lom 1 haskell coq

我正在尝试确保将Coq提取到Haskell时会丢弃无用的东西Prop。但是,当我使用以下示例时,我看到两者dividesprime都被提取为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)

提取它们有什么用?

Ant*_*nov 5

这是预期的行为。Prop命题来自的命题意味着这些命题在计算上是不相关的,因为那里的命题是为了确保正确性,例如表示算法的前后条件,而不参与计算。

这种情况类似于静态类型语言的类型-人们通常希望从运行时中删除类型。在这里,我们也希望删除证明的术语。

Coq的类型系统对此提供了支持,该系统禁止将逻辑信息从类型输入PropType,例如

Definition foo : True \/ True -> nat :=
  fun t => match t with
        | or_introl _ => 0
        | or_intror _ => 42
        end.
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.
Run Code Online (Sandbox Code Playgroud)

一个自然的问题出现了:

因此,理想情况下dividesprime应该从提取的文件中将其完全删除,对吗?它们为什么在那里存在?

正如Pierre Letouzey 在Coq提取概述中所解释的:

现在让我们总结一下Coq提取的当前状态。在[7]中描述的理论提取函数仍然有用,并且被用作提取系统的核心。此函数折叠(但不能完全删除)逻辑部分(以sort形式存在Prop)和类型。完全删除会在条款评估中引起危险的更改,甚至在某些情况下甚至可能导致错误或不终止。