Coq：如何从一个可判定的 Prop 中创建一个布尔值？

Question

我想将我的程序构建为抽象模块，并编写使用抽象类型的函数。但是我不能使用 match 来破坏抽象类型，所以我将不得不创建某种逆向引理，但我也不能 match 。我试图将我的问题归结为：

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

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 模块上参数化的模块，其函数 returns true if a=b and false 除此以外。由于 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.

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

这是必须要做的（即定义函数 decB）吗？如果不通过 returns bool?

的函数，是否根本不可能使用类型可确定的抽象事实

Answer 1

你不能写这个函数，因为 Coq 中的命题和计算对象是分离的（例如，参见）。

请注意，将您的 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 所采用的方法。您可以使用规范结构（如 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 参数）。

Coq：如何从一个可判定的 Prop 中创建一个布尔值？

Coq: How do I create a bool from a decidable Prop?

coq