En el siguiente fragmento de código Coq (cortado de un ejemplo real), intento declarar el primer argumento de exponent_valid como implícito:

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

Según tengo entendido, la función exponent_valid toma dos argumentos: uno de tipo float_format y otro de tipo float, y el primero se puede inferir. Sin embargo, la compilación del fragmento anterior falla con el siguiente mensaje de error:

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

Y de hecho, cambiando la declaración Arguments a:

Arguments exponent_valid {fmt} _ _.

Hace que el mensaje de error desaparezca.

Esta bien; Soy relativamente nuevo en Coq y puedo creer que me he olvidado de algo. Pero ahora, el bit que realmente me confunde: si reemplazo el <= en la definición de exponent_valid con un <, ¡el código se compila sin errores!

Tengo dos preguntas:

  1. ¿Por qué necesito un _ adicional en el primer caso?
  2. ¿Por qué reemplazar <= por < hace una diferencia en la cantidad de parámetros esperados por exponent_valid?

En caso de que sea relevante, estoy trabajando con Coq 8.4pl5.

coq
3
Mark Dickinson 22 ene. 2015 a las 23:38

2 respuestas

La mejor respuesta

exponent_valid tiene tipo

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

Sin notaciones es

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

Z.le se define como

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

not se define como

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

Entonces, el tipo de exponent_valid es convertible a

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

Lo que significa que la función puede tomar hasta tres argumentos.

Pero, supongo que es discutible si el comando Arguments debería tener en cuenta la convertibilidad o incluso si necesita que se le proporcione información sobre todos los argumentos de una función. Tal vez a los usuarios se les debería permitir quitar los guiones bajos al final.

6
perror 22 ago. 2015 a las 08:00

Su comprensión es correcta, y esto me parece un error (bastante extraño). Acabo de presentar un informe sobre el rastreador de errores.

Editar : Ah, la observación de flockshade a continuación pasó completamente desapercibida mientras miraba estas cosas. ¡Tiene sentido que tenga tres argumentos después de todo!

2
Arthur Azevedo De Amorim 23 ene. 2015 a las 19:50