coq - (value) 构造函数中的全量化类型变量不能按需要显式键入

Question

我有以下 GADT。

Inductive GADT : Type -> Type :=
| A : forall A, GADT A
| B : GADT bool.

以下数据类型具有一个带有全限定类型变量的构造函数。

Inductive Wrap A :=
| wrap : GADT A -> Wrap A
| unwrap : forall X, GADT X -> (X -> Wrap A) -> Wrap A.

然后我想定义一个递归函数，它使用 unwrap 中的函数。

Fail Fixpoint wrappedGADT {A} (xs: Wrap A) : option (GADT A) :=
  match xs with
  | wrap _ x => Some x
  | unwrap _ _ fx k => match fx with
                       | A _ => None
                       | B => wrappedGADT (k true)
                       end
end.

根据此定义，我收到以下错误消息。

The term "true" has type "bool" while it is expected to have type "T".

我假设当我检查 fx 并获取案例 B 时，参数 fx 的类型为 GADT bool，因此，全量化类型变量 X 也是 bool。这个假设是错误的吗？

接下来，我尝试显式键入 unwrap，如下所示。

Fail Fixpoint wrappedGADT {A} (xs: Wrap A) : option (GADT A) :=
  match xs with
  | wrap _ x => Some x
  | @nwrap _ bool fx k => match fx with
                           | A _ => None
                           | B => wrappedGADT (k true)
                           end
  end.

根据这个定义，我得到了一个非常奇怪的错误消息。

术语“true”的类型为“Datatypes.bool”，而预期的类型为“bool”。

任何人都可以指出这个问题的根源吗？

Answer 1

不幸的是，Coq 中的原始匹配语句对于您在此处应用的推理类型并不总是很聪明。 “车队模式”(有关更多信息，请参阅 CPDT)通常是解决此类问题的答案。此处的直接应用程序如下所示:

Fail Fixpoint wrappedGADT {A} (xs: Wrap A) {struct xs} : option (GADT A) :=
  match xs with
  | wrap _ x => Some x
  | unwrap _ _ fx k => match fx in (GADT T)
                       return ((T -> Wrap A) -> option (GADT A)) with
                       | A _ => fun k0 => None
                       | B => fun k0 => wrappedGADT (k0 true)
                       end k
end.

然而，这会遇到另一个问题，即 Coq 无法在通过“convoy”传递函数后验证终止条件。似乎要解决这个问题，首先定义对 k 的值进行递归调用的函数就足够了，然后改为护送它:

Fixpoint wrappedGADT {A} (xs: Wrap A) {struct xs} : option (GADT A) :=
  match xs with
  | wrap _ x => Some x
  | unwrap _ _ fx k => let r := fun x => wrappedGADT (k x) in
                       match fx in (GADT T)
                       return ((T -> option (GADT A)) -> option (GADT A)) with
                       | A _ => fun _ => None
                       | B => fun r' => r' true
                       end r
end.

对于您的第二次代码尝试，您正在创建一个局部变量 bool 以在 unwrap 构造函数中保存名为 X 的类型，它然后隐藏 Datatypes.bool 定义。通常，在 Coq 内核语言中没有办法只匹配一个特定类型(尽管类型类提供了一种在某种程度上模拟它的方法)。