haskell - 证明在 Coq 提取中的作用

Question

我试图了解证明在 Coq 提取中的作用。我有以下取自 here 的整数除以二的示例。在我的第一次尝试中，我使用了 Adished 关键字:

(*********************)
(* div_2_even_number *)
(*********************)
Definition div_2_even_number: forall n,
  (Nat.Even n) -> {p:nat | n=p+p}.
Proof.
Admitted.

(*************)
(* test_even *)
(*************)
Definition test_even: forall n,
  {Nat.Even n}+{Nat.Even (pred n)}.
Proof.
Admitted.

(********************)
(* div_2_any_number *)
(********************)
Definition div_2_any_number (n:nat):
  {p:nat | n = p+p}+{p:nat | (pred n) = p+p} :=
  match (test_even n) with
  | left h => inl _ (div_2_even_number n h)
  | right h' => inr _ (div_2_even_number (pred n) h')
  end.

(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/some_file.hs" div_2_any_number.

当我检查生成的 Haskell 文件时，我发现它确实丢失了:

div_2_even_number :: Prelude.Integer -> Prelude.Integer
div_2_even_number =
  Prelude.error "AXIOM TO BE REALIZED"

test_even :: Prelude.Integer -> Prelude.Bool
test_even =
  Prelude.error "AXIOM TO BE REALIZED"

div_2_any_number :: Prelude.Integer -> Prelude.Either Prelude.Integer
                    Prelude.Integer
div_2_any_number n =
  case test_even n of {
   Prelude.True -> Prelude.Left (div_2_even_number n);
   Prelude.False -> Prelude.Right (div_2_even_number (pred n))}

所以我想好吧，让我们证明div_2_even_number:

(*********************)
(* div_2_even_number *)
(*********************)
Definition div_2_even_number: forall n,
  (Nat.Even n) -> {p:nat | n=p+p}.
Proof.
  intros n0 H.
  unfold Nat.Even in H.
  destruct H as [m0].
  exists m0.
Qed.

但我收到以下错误:

Error: Case analysis on sort Set is not allowed for inductive definition ex.

这是怎么回事？我显然在这里遗漏了一些东西。

Answer 1

虽然chi说的是正确的，但在这种情况下，你实际上可以从存在证明中提取见证人p。当你有一个 bool 谓词 P : nat -> bool 时，如果 exists p, P p = true，你可以计算一些满足以下条件的 p谓词通过从 0 开始运行以下函数来实现:

find p := if P p then p else find (S p)

您无法直接在 Coq 中编写此函数，但可以通过设计一个特殊的归纳命题来实现。此模式在 choice module 中实现数学元件库:

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.

(* == is the boolean equality test *)
Definition even n := exists p, (n == 2 * p) = true.

Definition div_2_even_number n (nP : even n) : {p | (n == 2 * p) = true} :=
  Sub (xchoose nP) (xchooseP nP).

xchoose : (exists n, P n = true) -> nat 函数执行上述搜索，xchooseP 显示其结果满足 bool 谓词。 (实际类型比这更通用，但是当实例化为 nat 时，它们会产生此签名。)我使用了 bool 相等运算符来简化代码，但也可以使用 = 相反。

话虽这么说，如果您关心运行代码，那么以这种方式编程效率非常低:您需要执行 n/2 nat 比较来测试除法n。最好编写一个除法函数的简单类型版本:

Fixpoint div2 n :=
  match n with
  | 0 | 1 => 0
  | S (S n) => S (div2 n)
  end.