∀id1 id2 : id, {id1 = id2} + {id1 ≠ id2} 是什么意思？答案

【问题标题】：What does ∀id1 id2 : id, {id1 = id2} + {id1 ≠ id2} mean?∀id1 id2 : id, {id1 = id2} + {id1 ≠ id2} 是什么意思？
【发布时间】：2015-07-12 16:05:52
【问题描述】：

我正在阅读《软件基础》一书，在 Imp.v 文件中，定理 eq_id_dec 的定义如下：

Theorem eq_id_dec : forall id1 id2 : id, {id1 = id2} + {id1 <> id2}.
Proof.
   intros id1 id2.
   destruct id1 as [n1]. destruct id2 as [n2].
   destruct (eq_nat_dec n1 n2) as [Heq | Hneq].
   Case "n1 = n2".
     left. rewrite Heq. reflexivity.
   Case "n1 <> n2".
     right. intros contra. inversion contra. apply Hneq. apply H0.
Defined.

这个定理是否意味着对于任何 id 类型的 id1 和 id2，id1=id2 和 id1!=id2 都不会发生？我不确定。

【问题讨论】：

标签： coq imperative-languages

【解决方案1】：

不，它不排除等式和不等式同时为真的情况（尽管在实践中是这样）。

符号{A} + {B} 的类型sumbool A B 表示将证明A 或B 的决策过程。

所以这个eq_id_dec 是一个将两个ids 作为输入的术语，要么返回它们相等的证明，要么返回它们不同的证明。

更多关于 sumbool 的信息在这里：https://coq.inria.fr/distrib/current/stdlib/Coq.Bool.Sumbool.html

【讨论】：

所以，如果我必须调用这个函数，我必须传入一个 id 类型的值。 Id 是 Id：nat -> id。我该怎么做。我在 (eq_id_dec (id 4) (id 5)) 中进行 Eval Compute。它失败了
评估计算在 (eq_id_dec (Id 4) (Id 5))。

【解决方案2】：

对于所有 id1 和 id2，id1 = id2 或 id1 不等于 id2。

非常简单 - 要么等于 id2 要么不等于，根据定义，这将始终为真 - 所以对所有 id1/id2 都是如此。

【讨论】：

除了在像 Coq 这样的直觉框架中，P \/ ~P 不一定是真的（你可以添加排中作为公理）。您必须证明id1 和id2 类型的相等性是可判定的（因此定理名称中的dec）。