sumbool和直觉析取之间的区别

Question

根据Coq的文档

sumbool是一种布尔类型，具有其值的合理性

我认为这已经是Coq实现的直觉（或建设性）逻辑的析取性质。

例如，要证明p \/ ~pCoq中排除的中间点，您必须进行实际工作，这不是逻辑公理。因此，的证明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的计算相关的Universe中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}; 但是，如果使用此公理来编写程序，则将无法执行它们。