从Coq向Haskell提取Prop会导致空类型

Question

我正在努力确保在将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.

以下是divides和prime的情况：

type Divides = ()

type Prime = ()

提取它们有什么用？

Answer 1

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

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

这由Coq的类型系统支持，该系统禁止从Prop到Type中的类型泄漏逻辑信息，例如，

Definition foo : True \/ True -> nat :=
  fun t => match t with
        | or_introl _ => 0
        | or_intror _ => 42
        end.

结果是

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在他的overview of extraction in Coq中解释的那样：

现在让我们总结一下Coq提取的当前状态。 [7]中描述的理论提取功能仍然相关，并用作提取系统的核心。此函数折叠（但不能完全删除）逻辑部分（生活在排序Prop中）和类型。完全删除会导致术语评估中的危险变化，甚至可能导致某些情况下的错误或不终止。