时间戳

首页 > 解决方案 > 从 Coq 提取 Prop 到 Haskell 会导致空类型

haskell - 从 Coq 提取 Prop 到 Haskell 会导致空类型

问题描述

我试图确保在将 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 = ()

提取它们有什么用？

标签： haskellcoq

解决方案

这是预期的行为。来自的事物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 在他的 Coq 提取概述中解释的那样：

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

推荐阅读