eq_refl的奇怪隐式类型

Question

在Coq中,命题是类型,证明是值.例如,我们可以写一个像这样的简单证明,证明了这一点0=0.

Definition test : (eq 0 0) := eq_refl 0.

有趣的是,当检查其类型时eq_refl,它会显示出来

eq_refl
     : ?x = ?x
where
?A : [ |- Type] 
?x : [ |- ?A]

这意味着所有的论据eq_refl都是隐含的.在Coq中,除非使用隐式参数,否则通常不允许显式确定隐式参数@.为了证明0=0,我们可以明确地@eq_refl nat 0或只是eq_refl作为nat并且0可以推导出来.但在开始的例子中,eq_refl 0也有效.为什么？

这件事一般不起作用,例如

Definition foobar {A : Type -> Type} {T : Type} :  list (A T) := [].
Definition test : list (list nat) := foobar.
Fail Definition test' : list (list nat) := foobar nat.

Answer 1

常量的隐式参数结构有时可能依赖于几个 Arguments指令,如文件$COQLIB/theories/Init/Logic.v309和310中所示,这里再现:

Arguments eq {A} x _.
Arguments eq_refl {A x} , [A] x.

这里Arguments记录了命令的使用,但我没有看到它提到了几个隐式参数配置被接受.

另一方面,该命令Print Implicit eq_refl.返回有关以下事实的准确信息:可以使用两种理解隐式参数的方法,一种是函数接收1参数,另一种是函数接收0参数.