The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Actually, after more testing of this command, I don't think it has the
intended behaviour (at least in current v8.2 svn) : I would expect the
arguments defined in the Context command to be added with maximal
implicit status, just as they would be if the exact same
quantification was manually copy pasted in front of each definition in
the section.
More precisely, if I write :

Section EquivalenceProps.
  Context `{Setoid A}.
  Lemma l1 : forall x, ....
  ...
End EquivalenceProps.

this seems to be currently equivalent to writing :

Section EquivalenceProps.
  Variable A : Type.
  Variable H : Setoid A.
  Lemma l1 : forall x, ...
  ...
End EquivalenceProps.

So what I get by using Context `{ ... } instead of Variable/Hypothesis
is the automatic generalization of the parameter A ; this is nice, but
I would like the first definition to be equivalent to what happens if
I manually "unfold" the section :

Lemma l1 `{Setoid A} : forall x, ...
...

In that case, A and H are defined as maximal implicit in l1, and I
dont know how to get that with the current section mechanism, other
than manually setting implicit arguments afterwards :

Section EquivalenceProps.
  Context `{Setoid A}.
  Lemma l1 : forall x, ....
  ...
End EquivalenceProps.
Implicit Arguments l1 [[A] [H]].

If I have many lemmas (and I have 100s of them), this is not
satsifactory ; plus, I cant rely on the automatic implicit arguments
detection mechanism for the other arguments of l1 and the other
lemmas, since they are 'erased' by the Implicit Arguments command, so
I need to manually set the implicit status of every argument of every
definition, which is very cumbersome.

Does anyone have a solution with coq's current capabilities ? For now,
I resorted to the second definition (ie. not using sections at all)
but Im not happy with that obviously. Could the behavior of Context be
corrected in the v8.2 ?

Thank you in advance,

Stéphane L.

2009/5/11 Stéphane Lescuyer 
<stephane.lescuyer AT inria.fr>:
> I was just about to send an email to Matthieu to ask for such a
> command (I was very annoyed recently with the apparent impossibility
> to define instance variables in sections), now it turns out that it is
> already implemented but just lacks documentation :-) Thank you very
> much Arthur for spotting that, I read that paper months ago and I had
> forgotten about that.
>
> Stéphane L.
>
> On Mon, May 11, 2009 at 5:57 PM, Arthur Azevedo de Amorim
>Â <arthur.aa AT gmail.com>
>  wrote:
>> At a first glance, it seemed to me that the "Context" command that appears
>> on the paper on type classes is not documented. It would be nice to have it
>> on the Coq manual!
>>
>> --
>> Arthur Azevedo de Amorim
>>
>
>
>
> --
> I'm the kind of guy that until it happens, I won't worry about it. -
> R.H. RoY05, MVP06
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06