在 Set 类型的事物的居民上定义可判定的相等性

Question

我正在尝试在 BES 中定义变量的等级。 BES被定义为方程列表，变量是命题变量集合的居民，不是归纳类型：

Variable propVar : Set.

Definition rank (E:BES)(x:propVar) : nat :=
let fix block(E':BES)(curMu:bool) : nat := 
match E' with
| nil => fail
| cons (mu xc _) E2 => 
  if xc=x then (if curMu then O else S(O))
    else (if curMu then block E2 true else S(block E2 false))
| cons (nu xc _) E2 => 
  if eqb xc x then (if curMu then S(O) else O)
    else (if curMu then S(block E2 false) else block E2 true)
end
in
block E false.

但是，Coq 不接受这个定义，因为 xc=x 是 Prop 类型，而 Coq 需要 Bool 类型的东西。

是否可以在propVar 上定义类似于bool_dec 的可判定相等性，以便我可以使用它来代替xc=x？

Answer 1

你应该添加

Parameter propVardec : forall x y: propVar, {x = y}+{x <> y}.

此语句添加了propVar 的每个元素都相等或不同的假设，从而使您的类型可确定。

你也可以定义

Parameter propVarbeq : propVar -> propVar -> bool.

这或多或少是一样的。主要区别在于第一个为您提供相等（或差异）的证明，而第二个仅告诉您它们是否相等。

如果您曾经实例化您的 propVar 类型，您还应该证明/实例化这两个函数。