The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

Hello Michael,

Thanks for your detailed response.

You write:

This is e.g done by working in the computational world with types without dependent restrictions and formulate the restrictions as separate lemmas and group the two together with modules or typeclasses.

Do you have an example which illustrates this way of working?

Regards,

Jeff.

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Soegtrop, Michael <michael.soegtrop AT intel.com>
Sent: 18 September 2017 10:06:16
To: coq-club AT inria.fr
Subject: RE: [Coq-Club] Problem with dependent match statement

 

Dear Jeff,

> Could you clarify what you mean by your last sentence.

I guess you mean

>> it is known that A is a set with n elements so that f can't be defined for a
>> different parameter type.

Well this was sloppy again (physicists ...). I meant to say that the tabulate function is likely intended to enumerate inductive sets with exactly n elements. In such a situation having an enumeration function f which takes (Fin n) as argument type is most natural und you simply might not have an enumeration function which takes a different argument type.

Obviously the argument type of f must have at least n distinct instances as well, otherwise (f x) could not possibly give all instances of A. And since f, as any Coq function, has to be total, its argument type has either to have exactly n instances, or f has to return the same instance of A for different instances of the parameter type. Since n is a parameter of the tabulate function, you need some way to express "an inductive type with exactly n instances", and this is (Fin n) or something equivalent. Of cause one could use e.g. nat as argument type for f, e.g. by returning Option A, but it always results in some special case handling. Imagine you have type combiners like tuples or arrays and functions which create from enumeration functions for elements enumeration functions for the combined type. In such a setup enumeration functions which take (Fin n) as argument make things easier.

On the other handling such dependent type constructs can (IMHO) be a bit more difficult in Coq than in AGDA. I heard people say "yes Coq is dependently typed - but don't use it". In AGDA you have an editor to help you find the terms which fulfill the type restrictions. In Coq you usually use tactics to find these terms, but keep them hidden in proof terms. In a way Coq is usually split in a not (so much) dependently typed computational term world and a hidden dependently typed proof term world. I would say quite a few people working with Coq keep these two worlds as separate as possible. This is e.g done by working in the computational world with types without dependent restrictions and formulate the restrictions as separate lemmas and group the two together with modules or typeclasses. There are also people advocating a more dependently typed programming style in Coq, see e.g. https://emea01.safelinks.protection.outlook.com/?url="http%3A%2F%2Fadam.chlipala.net%2Fcpdt%2F&data=01%7C01%7Cjeffrey.terrell%40kcl.ac.uk%7C52a8ab55ceb44ae89c8408d4fe748e31%7C8370cf1416f34c16b83c724071654356%7C0&sdata=SoxFEBBqo%2BC7ZAqXfqTHTlOf1rNSgySFR5lM7qtnH8k%3D&reserved=0. I am mostly interested in highly automated usages of Coq in industrial environments and didn't yet come to a final conclusion what level of dependent types in programs is easiest to handle in such a setup - I am still experimenting.

I don't know how to handle the tabulate function best. I think it depends on its usage. If it is used in the proof term world, I would stay with the (Fin n) argument type, but then I would use tactics to define it - something like instead of actually writing down the tabulate function you more make a proof that such a function exists and you don't care how it looks. If such a function is used in the computational world, I would probably define it in a different way - but not sure.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, https://emea01.safelinks.protection.outlook.com/?url="www.intel.de&data=01%7C01%7Cjeffrey.terrell%40kcl.ac.uk%7C52a8ab55ceb44ae89c8408d4fe748e31%7C8370cf1416f34c16b83c724071654356%7C0&sdata=P1zS5SoDW9EMKWt9UOmLR3oCeqPYq7kYRcL7PeX5B9w%3D&reserved=0
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928