coq - 在 Coq : how many underscores are needed? 中声明隐式参数

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 的定义中与 < ，代码编译无误!

我有两个问题:

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).

不是被定义为

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

所以 exponent_valid 的类型可以转换为

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

这意味着该函数最多可以接受三个参数。

但是，我想 Arguments 命令是否应该考虑可转换性，或者是否需要向函数提供所有参数的信息，这是值得商榷的。也许应该只允许用户删除任何尾随下划线。