1

私はSoftware Foundationsの本を読んでいます.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}を証明する決定手順を特徴付けます。AB

したがって、これeq_id_decは入力として 2 つidの を受け取り、それらが等しいという証明、またはそれらが異なるという証明のいずれかを返す項です。

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に等しいか、等しくないかのどちらかであり、定義により常にtrueになります-したがって、すべてのid1 / id2に対してtrueです。

于 2015-05-03T04:58:10.160 に答える