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

Question

In the following snippet of Coq code (cut down from a real example), I'm trying to declare the first argument to exponent_valid as implicit:

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} _.

As I understand it, the exponent_valid function takes two arguments: one of type float_format and one of type float, and the first can be inferred. However, compiling the above snippet fails with the following error message:

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

And indeed, changing the Arguments declaration to:

Arguments exponent_valid {fmt} _ _.

makes the error message go away.

That's okay; I'm a relative newcomer to Coq and I can well believe that I've overlooked something. But now for the bit that's really confusing me: if I replace the <= in the definition of exponent_valid with a <, the code compiles without error!

I have two questions:

Why do I need an extra _ in the first case ?
Why does replacing <= with < make a difference to the number of parameters expected by exponent_valid ?

In case it's relevant, I'm working with Coq 8.4pl5.

flockshade flockshade · Accepted Answer · 2015-01-23T15:21:32

exponent_valid has type

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

Without notations it's

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

Z.le is defined as

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

not is defined as

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

And so exponent_valid's type is convertible to

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

which means the function can take upto three arguments.

But, I guess it's debatable whether the Arguments command should take convertibility into account or even if it needs to be supplied information on all arguments to a function. Maybe users should just be allowed to drop any trailing underscores.

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

2 Answers