如何比较Coq中相同Set的两个元素（相等）？

Question

Inductive ty: Set := 
| I 
| O. 

Definition f (x: ty) (y: ty): nat := 
    if x = y then 0 else 1. 

我想要的功能f比较ty类型的两个方面，但它并不能编译，我看到这个错误：

The term x = y has type Prop which is not a (co-)inductive type.

Answer 1

你需要证明平等是可判定为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. 

Answer 2

您可以使用match来感应数据类型的元素进行比较。

Definition f x y := match x,y with I, I | O, O => 0 | _,_ => 1 end. 

decide equality是一个更普遍的策略，并适用于无限集，但它是很好的知道，这是match是做实际工作。