The Coq mailing list

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

Hi,

Let me first describe how Coq works as it is before addressing your
questions.

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)".

Being an "apply term with (x:=term')" construction, when you write
"apply foo with (P:=P)", "foo" has to be interpreted as a term. Here
"foo" is declared with an implicit _maximal_ argument, hence the
notation "foo" denotes the term "@foo _".

As soon as "with" applies to a term and not a reference, the only way
I see to give meaning to the (P:=P) is to look for the type of the
term and see its binders. Calling "Check foo" in the context of the
proof of lemma bar to look at the type of foo gives (in 8.5):

foo
      : forall P0 Q0 : Prop, ?n = 0 -> Q0 -> P0 -> Q0
where
?n : [P : Prop  Q : Prop  H : Q  H0 : P |- nat] 

where ?n is the name chosen for the existential variable corresponding
to "_" in "@foo _".

Each existential variable is defined in a context shown after the
"where" clause (in 8.5). Here ?n is defined in context
"P : Prop  Q : Prop  H : Q  H0 : P".

Each use of an existential variable comes with an instance of the
defining context of the existential variable. This can be made fully
explicit by using the command "Set Printing Existential Instances".
After issuing this command, "Check foo" gives:

foo
     : forall P0 Q0 : Prop, ?n@{P:=P; Q:=Q; H:=H; H0:=H0} = 0 -> Q0 -> P0 -> 
Q0
where
?n : [P : Prop  Q : Prop  H : Q  H0 : P |- nat] 

where "@{P:=P; Q:=Q; H:=H; H0:=H0}" denotes the instance (here a
canonical instance which instantiates the P of the declaration of ?n
with the P in the context of the proof of bar, etc.)

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

> > 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.
> 
> I do not understand this syntax. What is the "?n@{...}"?


> Also, what you say does not seem to explain why this only happens when
> [foo] was declared in a Section.

This is not related per so to the Section. It is related to 
- the interpretation of foo as a term and not as a reference in "foo with 
(P:=P)"
- the existence of a maximal implicit argument to foo which makes that
  interpreting foo as a term means actually considering "@foo _"

Would you have e.g. defined foo without a section by

Lemma foo {n:nat} (P Q : Prop) : n = O -> Q -> P -> Q.

the situation would have been similar.

> However, disregarding the details of the implementation, don't you agree
> that having to write
> 
>   foo (P0:=P)
> 
> when foo was actually declared as having type "forall P:Prop, ..." is
> very confusing?

I agree that this is confusing. This is a consequence of interpreting
foo as a term, rather than as a reference and maybe this was not a
good design choice, as, indeed, most usages correspond to a situation
where foo is a reference (and thought as such). For instance in the
standard library, I found only 18 occurrences of "apply term with"
where term is not a reference, while there are several hundreds of
cases where it is just a reference.

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

>   From a user perspective, Coq is essentially making up a new name here
> for something that I already named differently.

As soon as the rule is to interpret "foo" as a term, it is not anymore
possible to keep the names P and Q because the result of "Check foo",
which is the same as the result of "Check (@foo _)" would capture the
P and Q which occur in the instance of ?n and which are the P and Q of
the context of the proof of bar, and not the P and Q of the statement
of foo. Alpha-conversion is mandatory.

> > So, probably, you intended to do
> > 
> >   apply @foo with (P:=P).
> > 
> > Hope it helps,
> 
> Being able to work around this with the @ is certainly useful. However,
> since only *implicit* arguments can be named, this trick becomes
> impractical once any non-implicit argument has to be specified -- it
> cannot be named, so one has to resort to underscores again.

I understand that your request is to have the ability to write 
"foo (P:=P)" the same way as the notation "foo (n:=0)" is available
for implicit arguments such as "n" here. I guess you would also like
to have this in any context, and not only as part of the "with" clause
of a tactic.

In any case it happens that this is not exactly the design choice
adopted for the "with" construction of tactics because of the term vs
reference issue described above.

So, could I rephrase your point as the following:
1. why not to provide the (P:=P) notation also for non-implicit arguments?
2. why to interpret "foo" as a term and not as a reference in the 
   "foo with (P:=P)" construction of tactics?
3. assuming 1. and 2., can "apply foo with (P:=P)" be a form of
   short-hand for "apply (foo (P:=P))" (with extra conditions on the
   number of arguments instantiated)?

Then, this looks to me as interesting directions to investigate and
worth discussions among users, developers and other contributors,
evaluating in particular the price to pay in term of compatibility.

Best regards,

Hugo

Technical PS: For 1., the relevant file in the archive is
interp/constrintern.ml, function extract_explicit_arg. For 2., it
should be enough to make a change in entry constr_with_bindings of
parsing/g_tactic.ml4 to test the syntactic restriction, then to change
intern_constr_with_binding in tacintern.ml.