{id1 = id2} + {id1 id1 id2}∀id1 id2 : id是什么意思？

Question

我正在阅读软件基础一书，在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都不能发生？我没有把握。

Answer 1

不，这并不排除平等和不平等同时为真的情况(尽管在实践中这里就是这样)。

符号{A} + {B}的类型sumbool A B描述了一个将证明A或B的决策过程。

所以这个eq_id_dec是一个以两个ids作为输入的项，返回它们相等的证明，或者它们是不同的证明。

有关sumbool的更多信息，请访问：https://coq.inria.fr/distrib/current/stdlib/Coq.Bool.Sumbool.html

Answer 2

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

非常简单-它要么等于id2，要么不等于，根据定义总是正确的-所以它对所有id1/id2都是正确的。