Inductive ty: Set :=
| I
| O.
Definition f (x: ty) (y: ty): nat :=
if x = y then 0 else 1.
私はタイプtyの二つの用語を比較する機能fをしたいが、それはコンパイルできないと、私はこのエラーを参照してください。Coqで同じSetの2つの要素を比較するにはどうすればよいですか？
The term
x = yhas typePropwhich is not a (co-)inductive type.
あなたが行うことができた（平等がtyのために決定可能であることを証明する必要があります自動的にdecide equalityを使用して）、その定義をif ... then ... else ...ステートメントで使用します。具体的には：
Inductive ty: Set :=
| I
| O.
Definition ty_eq_dec : forall (x y : ty), { x = y } + { x <> y }.
Proof.
decide equality.
Defined.
Definition f (x: ty) (y: ty): nat :=
if ty_eq_dec x y then 0 else 1.
あなたは、誘導データ型の要素を比較するためにmatchを使用することができます。
Definition f x y := match x,y with I, I | O, O => 0 | _,_ => 1 end.
decide equalityは、より一般的な戦術で、無限のセットのために動作しますが、本当の仕事をしているmatchであることを知って良いです。
あなたはこの関数がforall xy、fxy = 0を満たすことによってこの答えを改善することができます<-> x = yこのことは非常に簡単に証明できます。 – Yves
{} + {}についてもう少し分かりますか？ Proposition1やProp2のように思った。しかし、それはそのようには機能しません。彼らのために「分割」のようなものがありますか？ – abhishek
@abhishek [sumbool]（https://coq.inria.fr/library/Coq.Bool.Sumbool.html）を参照してください。例： [このブログの投稿]（http://seb.mondet.org/blog/post/coqtests-02-sumbools.html） – gallais