在 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 的新手，我相信我忽略了一些东西。但是现在确实让我感到困惑的一点是：如果我将 exponent_valid 定义中的 <= 替换为 <，代码编译时没有错误！

我有两个问题：

为什么在第一种情况下我需要一个额外的 _？
为什么用 < 替换 <= 会对 exponent_valid 预期的参数数量产生影响？

如果相关，我正在使用 Coq 8.4pl5。

Answer 1

您的理解是正确的，这对我来说看起来像是一个（非常奇怪的）错误。我刚刚在错误跟踪器上提交了 report。

编辑：啊，我在看这个东西的时候完全没有注意到 flockshade 在下面的观察。毕竟它有三个参数是有意义的！

Answer 2

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 命令是否应该考虑可转换性，或者是否需要为函数的所有参数提供信息，这是值得商榷的。也许应该允许用户删除任何尾随下划线。

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

Declaring implicit arguments in Coq: how many underscores are needed?

coq