The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

Coq has an interesting feature to simplify applying functions and lemmas
with implicit arguments: The arguments can have names, and then they can
be passed based on their name in any expression, in any order. For example:

  Definition foo {a b : nat} := a + b + b.
  Eval compute in (foo (b:=5) (a:=2)).
  (* Prints 12 *)

This is great, because it means if I need to specify *some* implicit
argument, I don't need to specify *all* of them. Even better, applying
the function is stable under small changes to the function signature,
and I can specify argument that are taken "later" without specifying
those given "earlier".

However, there is a very weird bug in this mechanism, which I reported a
while ago as <https://coq.inria.fr/bugs/show_bug.cgi?id=4536>. Namely,
under some circumstances, the name which is used to refer to the
argument of [foo] can change:

  Section S.
    Context {n: nat}.
    Lemma foo (P Q : Prop) : n = O -> Q -> P -> Q.
    Proof. tauto. Qed.
  End S.

  Lemma bar (P Q: Prop) : Q -> P -> Q.
  Proof.
    intros ? ?. Fail eapply foo with (P := P).
    (* [P] above now turned into [P0] ?!? *)
    eapply foo with (P0 := P).

  (* Either getting rid of the [n = 0 -> ] in [foo], or renaming
     the [P] argument of [bar] to something else, will result in the
     script above to fail because now [foo]'s argument has to be called
     [P] again. What?!? *)

These circumstances depend on whether [foo] was using variables of an
enclosing section (the [n] above), and on the current context at the
time of *applying* [foo] (the first argument of [bar] is also called
[P]). To me this was obviously a bug; I cannot imagine any situation in
which you'd *want* this behavior. Guillaume however noticed that there's
actually code in Coq doing this "on purpose".

What is the justification for this behavior of Coq? I have to say that I
am rather shocked by this being "by design". This behavior breaks, for
example, tactics that want to apply lemmas using the named-argument
syntax -- those lemmas suddenly stop working depending on the context
the tactics are applied in. But even when using this syntax directly,
one does not expect the name used to refer to something to be suddenly
and silently changed by Coq. And finally, the fact that this depends on
whether a section variable has been captured by the lemma sure makes
this look like a bug.
  So, if this is "on purpose", I urge you to reconsider this decision.
Even if backwards compatibility prevents you from just changing the
behavior, having a flag to configure this would be nice. I suggest "Set
NoInsaneBoundArguments" or similar. ;-)  But I would also be really
curios to learn what is the reasoning behind this. I cannot come up with
a good justification of the behavior described above.

And while I am on it -- what is the reason that this syntax can be used
only for implicit arguments? I think it would be just as useful for
explicit arguments; for example to give arguments in a different order,
or when applying a lemma, as in [apply (lemma (arg:=foo))], without
having to specify [arg] as implicit.

Kind regards,
Ralf