The Coq mailing list

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

Hi Hugo,

> The "apply ... with (x:=...)" construction applies to terms. So, it is
> an "apply term with (x:=term')" construction and not an
> "apply reference with (x:=term)".

My bug is mostly about "foo (name:=bar)". So I take it this, too, takes
[foo] to be any term and not just a reference?
  Indeed I expected this to be directly referring to a "Definition" or
so, which I take it is what you call a reference.

[...]

> This being said, I'll now try to address your questions.

Thanks for these explanations! I think I understand slightly better now
how all this works.

>> There is no ambiguity here, I am writing an application
>> of [foo] which only has one parameter called [P].
> 
> So, to paraphrase the explanation above, there is no ambiguity either
> for Coq here. You are writing an application of "foo" which is
> interpreted as "@foo _" and which has (after application of "_"),
> parameters called "P0" and "Q0", as "Check foo" tells.

So, let me try to see if I understand. The problem here is that in [@foo
_], the "_" is an existential that *could* use the [P] from the outside.
And hence the [P] in the definition of [foo] has to be renamed, so that
the two can be told apart in the existential?

What I don't entirely understand here is that the existential is
actually quantified "outside" the [P] in [foo], i.e., the implicit [n]
is an argument occurring *before" [P]. It hence cannot refer to [P]. But
still, somehow, in this type

> forall P0 Q0 : Prop, ?n@{P:=P; Q:=Q; H:=H; H0:=H0} = 0 -> Q0 -> P0 -> Q0

the existential ends up below the [P] (now renamed to [P0]), because the
[n] is *used* there. And that's where the clash comes from? So,
essentially, the trouble is that Coq is unable to express that these two
variables called "P" are *different* variables, and hence the only way
to get the outside [P] to the inside is to rename the inner [P].

If we could write

> rename P into P0 in forall P Q0 : Prop, ?n@{P:=P0; Q:=Q; H:=H; H0:=H0} = 0 
> -> Q0 -> P -> Q0

then the inner [P] would not need renaming.

But, in any case -- I can see that getting this named-argument business
right when working with any term is near impossible. I expected it to be
for references only, and that's where the clash of intuitions occurs.

Kind regards,
Ralf