The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 21 Nov 2011 23:39:10 -0800,
Michael Shulman 
<mshulman AT ucsd.edu>
 a écrit :

Note also "eapply lemma" which will introduce (if needed) ?xxx types to
be solved later; it can be very useful sometimes; see the documentation
for more information on it.

> Hi Arnaud,
> 
> Thanks for your reply.  The case I encountered involved no
> typeclasses, however, so that can't be the problem.  Unfortunately, it
> is in the middle of a lengthy development, and without any
> understanding of what the underlying issue might be, it is hard for me
> to come up with a simpler example.  I realize that's not very helpful;
> sorry.
> 
> Mike
> 
> On Mon, Nov 21, 2011 at 22:54, Arnaud Spiwack
> <aspiwack AT lix.polytechnique.fr>
>  wrote:
> > Hi Mike,
> >
> > Here is another working script that may illuminate what's happening:
> >
> > Definition idmap {A} : A -> A := fun x => x.
> >
> > Theorem thm A (x:A) : A.
> > Proof.
> >   apply (@idmap _).
> >   assumption.
> > Defined.
> >
> > Coq uses type information from the goal to try and solve the holes
> > properly. That said, last time I checked, it didn't interact well
> > with typeclasses, which are solved too eagerly (an improper
> > typeclass can then be inferred before the goal is inspected). I
> > suspect this is what's hitting you. Though this is pure guesswork.
> >
> >
> > Arnaud
> >
> >
> > On 21 November 2011 23:35, Michael Shulman 
> > <mshulman AT ucsd.edu>
> > wrote:
> >>
> >> 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
> >> >>
> >> >
> >> >
> >>
> >
> >
>