1

我正在阅读软件基础书，在 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 都不会发生？我不确定。

4

2 回答 2

3

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

sumbool A B符号的类型{A} + {B}表征了将证明要么 要么 的决策A过程B。

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

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

于 2015-05-03T04:57:38.177 回答
-1

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

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

于 2015-05-03T04:58:10.160 回答