The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Ok.  I see a note now about "Generalizable Variables" as a new feature
in the CHANGES file.  I also found the new use of "Generalizable
Variables" in the SetoidDec.v file for Coq 8.3.  But it seems like a
bad idea for coqdoc to strip out that command if it is actually
relevant to interpreting the subsequent Coq definitions.

But all of this business about generalizable variables verges on a
little too much voodoo for my taste...I am personally happier to read
and write this definition --

Definition my_equiv_decb {A} {S: Setoid A} {_: EqDec S} (x y: A): bool :=
 if x == y then true else false.

-- which I understand to be precisely identical to the one I gave below.

Speaking of which...if anybody is willing to elaborate on when to use
"Superclasses" (ch. 18.4.1) as opposed to "Substructures" (ch.
18.4.2), I would be very interested to hear about that.  I could be
terribly mistaken, but they seem to accomplish pretty much the same
thing.

 - Aaron

2010/10/12 Stéphane Lescuyer 
<stephane.lescuyer AT inria.fr>:
> Hi Aaron,
>
> This is the normal behaviour, and a difference between 8.2 and 8.3. In
> the special binder `{...}, it is convenient to have unbound variables
> be automatically generalized, this lets you write, say, "forall
> `{Bijection A B}" if you have the defined the class of bijections
> between two types, instead of having to explicitely write "forall {A
> B} `{Bijection A B}".
> In 8.2, such variables were automatically generalized (and marked as
> maximally implicit), but the issue is that if you wanted to use an
> existing object and you make a typo, Coq will proceed fine and
> generalize it. Therefore, starting with version 8.3, variables which
> can be generalized must be define with the command Generalizable
> Variables (see doc in 8.3 for exact syntax).
>
> Hope this helps,
> Stéphane
>
> On Tue, Oct 12, 2010 at 6:09 PM, Aaron Bohannon 
>Â <bohannon AT cis.upenn.edu>
>  wrote:
>> Hi, I'm afraid I may have sent this to an out-dated Coq Club address.
>> Here it is again, just in case...
>>
>> ---------- Forwarded message ----------
>> From: Aaron Bohannon 
>>Â <bohannon AT cis.upenn.edu>
>> Date: Mon, Oct 11, 2010 at 2:40 PM
>> Subject: type class issue in Coq 8.3
>> To: Coq List 
>>Â <coq-club AT pauillac.inria.fr>
>>
>>
>> Hi, consider the following situation.  We import SetoidDec; we check
>> that "equiv_decb" was defined in the file; and then we duplicate the
>> definition used in the SetoidDec file:
>>
>> Require Import SetoidDec.
>> Print Implicit equiv_decb.
>> Definition my_equiv_decb `{EqDec A} (x y: A): bool :=
>>  if x == y then true else false.
>>
>> In Coq 8.2, this works fine.  In Coq 8.3rc1, I get an error when
>> executing the Definition:
>>
>> Error: Unbound and ungeneralizable variable A
>>
>> I only barely understand Coq's type classes as it is, so I am quite
>> confused and really have no idea whether it is a bug or a feature.
>> However, I could not find any account of this difference in the
>> COMPATIBILITY file, the CHANGES file, or the 8.3 manual.
>>
>>  - Aaron
>>
>>
>
>
>
> --
> I'm the kind of guy that until it happens, I won't worry about it. -
> R.H. RoY05, MVP06
>