归纳定义中Coq隐式类型推导的规则是什么？

如何解决归纳定义中Coq隐式类型推导的规则是什么？

请考虑将X作为隐式类型的这种类型。

Inductive list' {X:Type} : Type :=
  | nil'
  | cons' (x : X) (l : list').

Coq推断cons'的第二个参数的类型为@list' A：

Fail Check cons' a (cons' b nil'). (* "cons' b nil'" expected to have type "@list' A"*)

但是如何明确推断出这种类型？ 我们可以创建另一种类型：

Inductive list'' {X:Type} : Type :=
  | nil''
  | cons'' (x : X) (l : @list'' B).

Check cons'' a (cons'' b nil'').

它表明l也可以是@list' B。

解决方法

准确地说，Coq推断cons'的类型为forall {X},X -> @list' X -> @list' X。然后，当您编写cons a时，Coq得出您必须建立一个@list' A，并用X填充A的情况，因此将第二个参数限制为类型@list' A。

但是，正如您所注意到的，选择X而不是其他某种类型并不是唯一的选择。在第二个示例中，cons''的类型为forall {X},X -> @list'' B -> @list'' X。但是，如果未指定该参数，大多数人大多数时候会希望其参数（冒号左侧的内容）是一致的，也就是说，参数中的结论与结论相同，通过启发式可以在此处选择X。总的来说，Coq不会太担心确保解决方案对于用户未指定的事情是唯一的。

在最新的Coq版本中，您可以使用选项Uniform Inductive Parameters指定所有参数都是统一的，或者使用|将统一参数与非统一参数分开。对于列表，看起来像

Inductive list' (X:Type) | : Type :=
  | nil'
  | cons' (x : X) (l : list').

请注意，对于|，在构造函数的声明中，list'的类型为Type，而对于没有|的类型，list'的类型为{{1 }}，并且存在一个约束，即构造函数的结论必须为Type -> Type（而参数可以自由使用list X）。