如何比較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是做實際工作。