COQ中枚举类型的相等性

Question

我有一个在COQ中的有限枚举类型（称为T），想要检查元素的相等性。这意味着我需要一个函数：

bool beq_T(x:T,y:T)  

我只能通过逐个分析的方式来定义这样一个函数，这会导致很多匹配语句，看起来非常繁琐。因此，我想知道是否有更简单的方法来实现这个功能。

- Cryptostasis

Answer 1

更简单的说，Scheme Equality for ... 生成两个函数，分别返回布尔值和 sumbool。

- eponier

Answer 2

坏消息是，实现beq_T的程序必须在两个参数上有一个大型匹配语句。好消息是，您可以使用Coq的tactic language自动生成/合成此程序。例如，给定以下类型：

Inductive T := t0 | t1 | t2 | t3.

你可以如下定义beq_T。前两个destruct策略会合成匹配x和y所需的代码。match策略检查它所在的分支，并根据x = y是否成立，合成返回true或false的程序。

Definition beq_T (x y:T) : bool.
  destruct x eqn:?;
  destruct y eqn:?;
  match goal with 
  | _:x = ?T, _:y = ?T |- _ => exact true
  | _ => exact false
  end.
Defined.

如果想查看合成的程序，请运行：

Print beq_T.

感谢Coq已经提供了一个几乎满足您需求的策略。它被称为decide equality。它自动合成一个程序，决定一个类型T的两个元素是否相等。但是，它不仅返回布尔值，还返回两个元素（不）相等的证明。

Definition eqDec_T (x y:T) : {x = y} + {x <> y}.
  decide equality.
Defined.

有了这个程序的综合，实现beq_T就变得很容易。

Definition beq_T' {x y:T} : bool := if eqDec_T x y then true else false.

- Konstantin Weitz