The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Dear Ralf,

I just replied to your bug report. I'm afraid the misunderstanding
comes from the maximal implicit argument of foo.

Indeed, if you type

  Set Printing Existential Instances.

and do

  Check foo.
  (*
  foo
       : forall P0 Q0 : Prop, ?n@{P:=P; Q:=Q; H:=H; H0:=H0} = 0 -> Q0 -> P0 
-> Q0
  *)

You'll see that the type of foo depends on the "P" of the goal and
that there is no other choice than renaming the "P" of foo into
another name.

So, probably, you intended to do

  apply @foo with (P:=P).

Hope it helps,

Hugo

On Wed, May 04, 2016 at 02:45:24PM +0200, Ralf Jung wrote:
> 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