证明在Coq提取中的作用

Question

我试图了解证明在Coq提取中的作用。我被两个取自有地板整数除法下面的例子在这里。我第一次尝试使用Admitted关键字：

(*********************)
(* 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从存在证据中提取证人。如果具有布尔谓词P : nat -> bool（if）exists p, P p = true，则可以p通过从0运行以下函数来计算一些满足该谓词的条件：

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

您不能直接在Coq中编写此函数，但是可以通过编写特殊的归纳命题来实现。此模式在数学组件库的选择模块中实现：

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显示其结果满足布尔谓词。（实际类型比这更通用，但是实例化时nat会产生此签名。）我使用布尔等式运算符简化了代码，但可以使用它来=代替。

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

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

Answer 2

您正在使用不同种类的类型。

> Check (Nat.Even 8).
Nat.Even 8
     : Prop

> Check {p:nat | 8=p+p}.
{p : nat | 8 = p + p}
     : Set

Coq类型系统的一个特点是您不能消除其类型为in的值Prop来获取其类型不在in的值Prop（大致而言-Coq对Prop不包含任何信息的类型（例如True和）做了一些例外False，但我们并非如此）。粗略地说，除了证明另一个命题之外，您不能对任何命题使用证明。

不幸的是，此限制要求Prop是强制性的（我们希望forall P: Prop, P->P成为某种类型Prop），并且要与被排除的中间律保持一致。我们不能拥有一切，否则我们会遇到Berardi的悖论。