The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  You're right, that's a bit weird. We must have removed or are missing a warning telling you that Inductive should rather not be used for a non-recursive record definition and that Record is the preferred way to define them. As soon as you write Inductive, eta is disabled (eta on recursive types is a quite different beast, see N. Ghani's thesis for example for a short exposition). This finiteness information you give (Variant/Record(bifinite) or Inductive(finite) or CoInductive(cofinite)) is checked and used by the kernel now, in particular to decide if eta can be decided. All this information should be in the documentation indeed.

Best regards,

-- Matthieu

On Wed, Dec 7, 2016 at 9:06 AM Ralf Jung <jung AT mpi-sws.org> wrote:

Hi,

> Le 07/12/2016 à 08:32, Ralf Jung a écrit :
>> Hi,
>>
>>> As I understand it, any record declared with the [Record] vernacular
>>> whose projections can be defined, which has at least one projection,
>>> automatically gets eta.  That is, the following records do not enjoy eta:
>>>   Set Primitive Projections.
>>>   Record unit := tt {}.
>>>   Record inhabited (A : Type) : Prop := inhabits { inhabited_val : A }.
>>>   Record unnamed_inhabitant (A : Type) := { _ : A }.
>>>   Inductive prod A B := pair { fst : A ; snd : B }.
>>> and all records which do not suffer from any of these "problems" will
>>> automatically get eta conversion when primitive projections are turned
>>> on.   Someone else (Matthieu?) can correct me if I've missed anything.
>> I see; in our case, we used 'Inductive' instead of 'Record' so we did
>> not get eta.  Thanks!  That's kind of a surprising difference between
>> these vernaculars, at the very least, it should be documented.
>
> Well, I think it is:
>
> "The option Set Primitive Projections turns on the use of primitive
> projections when defining subsequent records."

The 'Inductive' *is* a record with primitive projections.  It just
doesn't get eta.  I do not see a way to interpret that into the
documentation.

Kind regards,
Ralf

>
>
>
>
>>
>> Kind regards,
>> Ralf
>>
>>> On Tue, Dec 6, 2016 at 3:57 PM Ralf Jung <jung AT mpi-sws.org
>>> <mailto:jung AT mpi-sws.org>> wrote:
>>>
>>>     Hi all,
>>>
>>>     We started to play around with primitive projections a little in our
>>>     development, and if they work (which unfortunately still is a rather big
>>>     if), we could achieve some fairly significant performance improvements:
>>>     Coq 8.6 got >7% faster (that's total compilation time!) by switching the
>>>     record we use for sealing some of our core definitions to primitive
>>>     projections. That's pretty impressive!
>>>
>>>     One thing we couldn't figure out though is when we get eta conversion
>>>     for primitive projections.  The aforementioned record used for sealing
>>>     does not have eta (according to About), while other records do.  Are the
>>>     rules for when a primitive record gets eta written down anywhere?  All I
>>>     could find in the documentation is the two paragraphs in
>>>     <https://coq.inria.fr/distrib/8.6beta1/refman/Reference-Manual004.html>,
>>>     which don't even mention that primitive projections have anything to do
>>>     with eta conversion.
>>>
>>>     Kind regards,
>>>     Ralf
>>>
>