Coq:我如何从可判定的支持中创建一个bool？

Question

我希望将我的程序构造成抽象模块，并编写使用抽象类型的函数。但是我不能用match来破坏抽象类型，所以我必须创建一个类似的逆引理，但是我也不能在它上match。我试着把我的问题归结为：

首先，创建一个可以由Module Type类型使用的decidable。

Require Import Decidable.

Module Type decType.
  Parameter T : Type.
  Axiom decT : forall (a b:T), decidable (a=b).
End decType.

下面是一个例子：nat是可判定的。但其目的是编写plus等只针对抽象类型。(我删除了参数zero、Succ以及它们的要求，以使这里的示例最小化)。

Require Peano_dec.

Module nat_dec <: decType.
  Definition T := nat.
  Definition decT := Peano_dec.dec_eq_nat.
End nat_dec.

现在，关于我的问题:我想在decType模块上编写一个参数化的模块，如果a=b和false不是这样的话，它的函数返回true。由于a和b是decType的，这应该是可判定的(因此是可计算的，或者？)，但是如何编写beq呢？

Module decBool (M: decType).
  Import M.
  Definition beq (a b:T) : bool :=
    ???
  .

End decBool.

到目前为止，我的想法是必须向decType模块类型中添加一个布尔函数，如下所示：

Module Type decType.
  Parameter T : Type.
  Axiom decT : forall (a b:T), decidable (a=b).
  Parameter decB : forall (a b:T), {a=b}+{a<>b}.
End decType.

然后在上面的decB模块中定义nat_dec。

这就是我们必须做的(即定义函数decB)吗？难道根本不可能使用抽象的事实，即类型是可判定的，而不经过返回bool的函数吗？

Answer 1

您不能编写此函数，因为Coq (cf )中的命题和计算对象分离。例如这个答案 )。

注意，向模块中添加decB参数使decidable公理变得不必要，因为您可以使用{P} + {Q}派生P \/ Q。

我想再加几个相关的笔记。首先，我将避免使用Coq模块系统来执行名称空间和编写不透明定义以外的任何事情。如果您想要编写参数定义，您可能会更好地使用相关记录。

Record eqType := {
  sort :> Type; 
  eqb : sort -> sort -> bool;
  eqbP : forall x y, eqb x y = true <-> x = y
}.

这本质上是斯皮尔采取的方法。您可以使用规范结构(如Ssreflect )或类型类来简化这些依赖记录的使用。

其次，您可以编写显式消除器函数，以避免诉诸match。例如，nat_rect函数允许您使用高阶参数在nat上编写递归函数：

nat_rect : forall (T : nat -> Type),
             (* value for 0 *)
             T 0 ->
             (* body for recursive call *)
             (forall n, T n -> T (S n)) ->
             forall n, T n.

这些函数为每种归纳数据类型自动定义。它们涉及依赖类型，但您也可以使用它们进行非依赖类型的递归。虽然这样做有点效率低下，但您也可以通过传递忽略递归调用值的函数(在上面的示例中，第二个函数参数的T n参数)，将它们用于模式匹配。