在Coq中声明隐式参数:需要多少个下划线？

Question

在下面的Coq代码片段中(从一个真实的例子中删除),我试图将第一个参数声明exponent_valid为隐式:

Require Import ZArith.
Open Scope Z.

Record float_format : Set := mk_float_format {
  minimum_exponent : Z
}.

Record float (fmt : float_format) : Set := mk_float {
  exponent : Z;
  exponent_valid : minimum_exponent fmt <= exponent
}.

Arguments exponent_valid {fmt} _.

据我所知,该exponent_valid函数有两个参数:一个是类型float_format,一个是类型float,第一个可以推断出来.但是,编译上面的代码段失败,并显示以下错误消息:

File "/Users/mdickinson/Desktop/Coq/floats/bug.v", line 13, characters 0-33:
Error: The following arguments are not declared: _.

事实上,将Arguments声明更改为:

Arguments exponent_valid {fmt} _ _.

使错误消息消失.

没关系; 我是Coq的新手,我完全相信我忽略了一些东西.但是现在我真的很困惑我:如果我用a 替换<=定义,代码编译没有错误!exponent_valid<

我有两个问题:

1. 为什么我_在第一种情况下需要额外的？
2. 为什么更换<=与<有所作为的由预期的参数个数exponent_valid？

如果它是相关的,我正在使用Coq 8.4pl5.

Answer 1

exponent_valid 有类型

forall (fmt : float_format) (f : float fmt), minimum_exponent fmt <= exponent fmt f.

没有符号就是这样

forall (fmt : float_format) (f : float fmt), Z.le (minimum_exponent fmt) (exponent fmt f).

Z.le 被定义为

= fun x y : Z => not (@eq comparison (Z.compare x y) Gt).

not 被定义为

= fun A : Prop => A -> False.

所以exponent_valid类型可以转换为

forall (fmt : float_format) (f : float fmt), 
   (minimum_exponent fmt ?= exponent fmt f) = Gt -> False,

这意味着该函数最多可以占用三个参数.

但是,我猜这个Arguments命令是否应该考虑到可转换性,或者即使它需要提供有关函数的所有参数的信息也是有争议的.也许应该允许用户删除任何尾随下划线.