Coq:我如何从一个可判定的 Prop 中创建一个 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 上参数化的模块具有返回 true 的函数的模块如果 a=b和 false除此以外。由于 a和 b属于 decType这应该是可确定的(因此是可计算的，或者？)，但是我该如何写 beq ?

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

End decBool.

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

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 中的命题和计算对象是分开的(例如，参见 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 参数)。