The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Hi Alexandre,

Thanks for your reply!  Something like that was my first guess as to
what was going on.  But it seems to me that there must be something
more than that (or else I am just not understanding), because "apply
lemma" sometimes (indeed, usually) does work, even when 'lemma' has
maximally inserted implicit arguments.  For instance:

  Definition idmap {A} : A -> A := fun x => x.

  Theorem thm A (x:A) : A.
  Proof.
    apply idmap.
    assumption.
  Defined.

Here the argument A is maximally inserted to idmap.  So if "apply
idmap" is immediately converted to "apply (@idmap _)", then how can
Coq determine that the _ there should be A before it passes the term
off to 'apply'?

Mike

On Mon, Nov 21, 2011 at 13:29, Alexandre Pilkiewicz
<alexandre.pilkiewicz AT polytechnique.org>
 wrote:
> Hi Micheal:
>
> There are two types of implicit arguments: the "normal" ones, and the
> "maximally inserted". The intuition is this: the normal ones are
> automatically added (say, replace by _) by the system when an argument
> after them is provided. The maximally inserted ones are added as soon
> as all the arguments before are given. Let us see an example :)
>
> Definition fst A B (ab:A * B) := let (a, _) := ab in a.
>
> fst is of type forall A B : Type, A * B -> A
>
> Say A and B are implicit:
>
> Implicit Arguments fst [A B].
>
> Then this works:
> Eval compute in (fst (true, 5)).
> and computes true: because the argument ab (here (true, 5)) is given,
> A and B are "inserted" (it's equivalent to @fst _ _ (true, 5))
>
> Now what about
> Require Import List.
> Notation "[ ]" := nil.
> Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
> Eval compute in (map fst [(true, 5); (false, 6)]).
>
> It fails, saying:
> Error: The term "fst" has type "forall A B : Type, A * B -> A"
>  while it is expected to have type "?21 -> ?22".
>
> Here fst is by itself, without arguments: so A and B are *not*
> inserted (remember that Implicit Arguments are inserted when an
> argument following them is provided). So it has the "nude" type of
> fst, which is not of the form _ -> _, and therefore cannot be an
> argument of map.
>
> Solution? The first is to go for
> Eval compute in (map (@fst _ _) [(true, 5); (false, 6)]).
>
> The second is to use maximally inserted arguments:
> Implicit Arguments fst [[A] [B]].
> Eval compute in (map fst [(true, 5); (false, 6)]).
>
> Here it works, because A and B are immediately added.
>
> So now what is the problem with apply? Basically, when you have
> maximally inserted arguments
> apply foo
> is like
> apply (@foo _ _).
> But the systems tries to type (@foo _ _) *before* giving to apply
> (which is good if you type something like "apply (5 false)", you
> directly have a type error on the application of a nat to a bool). But
> there, there is no context to type the _. Hence the type error.
> If the arguments are only implicit, it's like typing "apply @foo",
> which is typable.
>
> Hopes this helps
>
> Cheers, Alexandre
>
>
>
> On Mon, Nov 21, 2011 at 7:08 PM, Michael Shulman 
> <mshulman AT ucsd.edu>
>  wrote:
>> Hi,
>>
>> What is the difference between
>>
>> apply lemma.
>>
>> and
>>
>> apply @lemma.
>>
>> ?  I have encountered a few situations where the former fails but the
>> latter succeeds.  This confuses me, because in both cases all the
>> arguments of lemma (implicit or non-implicit) have to be deduced from
>> context.  Is the first one somehow trying to guess the implicit
>> arguments too soon or without enough information?
>>
>> Thanks!
>> Mike
>>
>
>