coq - 为什么我在这个例子中定义 Coercion 的方式是错误的，正确的方式是什么？

Question

我的 Coq 代码如下:

    Inductive A (X: Type) :=
      n1 : nat -> X -> (A X)
    .

    Arguments n1 {X} _ _. 

    Inductive B :=
      m1 : (A nat) -> B |
      m2 : B -> B -> B
    .

    Coercion m1 : A >-> B.

    Check m2 (m1 (n1 1 2)) (m1 (n1 2 2)). (* 1st Check *)
    Check m2 (n1 1 2) (n1 2 2). (* 2nd Check *)

我定义了类型 A 和 B(A 是多态类型)。在写下由运算符 'm2' 连接的 B 的表达式(如 '1st Check')时，我希望省略构造函数 'm1'(如 '2nd Check')，所以我定义了一个强制转换。然而，只有“第一次检查”有效，“第二次检查”不起作用。

在这里使用强制的正确方法是什么？为什么我的定义是错误的？

Answer 1

我不认为有任何方便的方法可以使用当前的强制引擎获得您想要的东西。当您输入 m1作为强制，Coq 表示它不尊重统一继承条件。当您在类型系列之间声明强制转换以修复某些参数时会发生这种情况；在这里，您修复了 X成为 nat .当这个条件被打破时，Coq 的类型检查器拒绝应用强制转换。

一个部分解决方案是引入一个中间类型:

Inductive A (X: Type) :=
      n1 : nat -> X -> (A X)
    .

    Arguments n1 {X} _ _.

Definition Anat := A nat.
Identity Coercion Anat_of_A : Anat >-> A.

Inductive B :=
  m1 : Anat -> B |
  m2 : B -> B -> B
.

Coercion m1 : Anat >-> B.

Check m2 (m1 (n1 1 2)) (m1 (n1 2 2)). (* 1st Check *)
Check m2 (n1 1 2 : Anat) (n1 2 2 : Anat). (* 2nd Check *)

问题在于 n1仍然产生 A 类型的东西最后，而不是 Anat .因此，您需要显式转换来说服 Coq 触发强制转换。当然，你也可以定义一个版本 n1专用于 X ，但这会违背制作 A 的目的多态的。