coq - sumbool 和直觉析取之间的区别

Question

根据Coq的文档

sumbool is a boolean type equipped with the justification of their value

我认为在 Coq 实现的直觉(或构造性)逻辑中，这已经是析取的一个属性。

例如，要在 Coq 中证明排除的中间 p\/~p，你必须做实际工作，这不是一个逻辑公理。因此，p\/q 的证明必须是 p 的证明或 q 的证明。

那为什么我们需要sumbool p q？

编辑

通过用精确的证明替换策略，我得到了更具体的错误消息。这个很好:

Lemma sumbool_or : forall p q : Prop, sumbool p q -> p \/ q.
Proof.
  exact (fun (p q : Prop) (H : sumbool p  q) =>
           match H with
           | left p0 => or_introl p0
           | right q0 => or_intror q0
           end).
Qed.

但是这个

Lemma or_sumbool : forall p q : Prop, p \/ q -> sumbool p q.
Proof.
  exact (fun (p q : Prop) (H : p \/ q) =>
           match H with
           | or_introl p0 => left p0
           | or_intror q0 => right q0
           end).
Qed.

告诉我

Error:
Incorrect elimination of "H" 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.

我有点惊讶。那么像 match 这样的原语取决于我们想要证明的事情类型？不过，它看起来只是低级 lambda 演算。

Answer 1

sumbool类型存在于 Coq 的计算相关宇宙中 Type (或Set)。特别是，我们可以使用返回 {P} + {Q} 元素的函数编写程序。 (例如，标准库的 Nat.eq_dec : forall n m : nat, {n = m} + {n <> m} ，它测试两个数字是否相等)。

另一方面，逻辑析取属于与计算无关的宇宙 Prop 。我们无法对类型证明 P \/ Q 进行案例分析因为 Coq 的设计目的是在提取程序时删除证明，而这样的案例分析可能会改变计算的结果。例如，这使我们可以安全地添加排除的中间公理 forall P : Prop, P \/ ~ P不影响提取的程序的执行。

还可以添加位于Type中的排除中间的强形式。 :forall P : Prop, {P} + {~P} ;但是，如果我们用这个公理来编写程序，我们将无法执行它们。