The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

In Matita they claim to have made a step towards such a unification of
techniques:
Hints in unification
http://www.cs.unibo.it/~asperti/PAPERS/tphol09.pdf

Bas

On Mon, Jan 18, 2010 at 1:38 PM, AUGER 
<Cedric.Auger AT lri.fr>
 wrote:
> Le Sat, 16 Jan 2010 13:36:47 +0100, Stéphane Lescuyer
>Â <stephane.lescuyer AT inria.fr>
>  a écrit:
>
>> On Sat, Jan 16, 2010 at 1:23 PM, Adam Chlipala 
>>Â <adamc AT hcoop.net>
>>  wrote:
>>>
>>> Chris Dams wrote:
>>>>
>>>> It seems writing records like list_type is about the same as writing
>>>> Modules. Moreover, they are first class citizens in the Coq language,
>>>> being Inductives with some extra destructor names for convenience. So,
>>>> why was the basic Coq language polluted with the seemingly useless
>>>> concept of modules?
>>>>
>>>
>>> There are certainly ways to make Coq's module system more useful, but I
>>> wouldn't call it useless.  You get the automatic support for "subtyping"
>>> that comes from module signature ascription.  It's also useful to work
>>> with
>>> second-class constructs in many cases; they are intrinsically easier to
>>> understand, because the reader knows you can do fewer things with them.
>>>  Finally, there are commands like [Import] that only work on modules,
>>> though
>>> a similar command could certainly be implemented for records.
>>
>> And it should also be mentioned that each module has its own
>> namespace, while records don't. And modules (and interfaces) can
>> contain notations, hints, etc.
>
> I also discussed of it with some people, and modules should be more
> efficient
> as they define top-level objects.
>
> Furthermore files are seen as modules and not records and as Stephane said,
> we can define tactics in module types and call them with dot notation.
>
> For example, if you want to extract some code, it is rather wise to use
> modules instead
> of records, for performances; for proofs, it is less important.
>
> But other things in Coq seem not very useful (and in fact they can be):
> Classes (as they just are Records, but have automation for certain things)
> Records (as they just are Inductives, and cannot be used inside mutual
> inductives for stupid reasons)
> a lot of tactics are redundant,
> use of Lemmas, Theorem, Corollary in one hand and Variable, Hypothesis,
> Parameter in the other hand.
>
> I agree that these features lack some kind of unification.
>
> --
> Cédric AUGER
>
> Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
>
>