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

【问题标题】：Coq: How do I create a bool from a decidable Prop?Coq：我如何从一个可判定的 Prop 中创建一个布尔值？
【发布时间】：2015-10-02 14:25:13
【问题描述】：

我想将我的程序构建为抽象模块，并编写使用抽象类型的函数。但是我不能使用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 模块上参数化的模块，其函数返回 true 如果 a=b 和 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）？不通过返回 bool 的函数，就根本不可能使用类型是可确定的抽象事实吗？

【问题讨论】：

标签： coq

【解决方案1】：

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

请注意，将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 参数）。

【讨论】：