The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Le 08/01/2014 18:49, Jean Goubault-Larrecq a écrit :

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Le 08/01/2014 18:40, Cody Roux a écrit :

On 01/07/2014 04:19 AM, Altenkirch Thorsten wrote:

A convincing way to justify those systems would be to provide a 
translation into eliminators. I suggested this to Andreas a while
ago.

That sounds fair. A couple years ago, I tried seeing if there was
a straightforward way to perform this translation (with Jorge
Sacchini). It's not trivial, and in particular I found that I would
probably need some form of proof-irrelevance, even for
"first-order" datatypes, which seems ironic. However in this case
we would only need it on "h-level 0" so it doesn't seem hopeless.

Higher-order datatypes are a bit more difficult, and I admit I
never worked it out. I believe it's possible though.

The fact that the implementation is behind the theoretical
capabilities is just that, an implementation problem.

The eliminators are like axioms in set theory and it is
worthwhile to translate any extension by reducing them to the
axiom instead of adding new ones even though they may be
semantically justified.

That's fair, but I don't see why eliminators have a more powerful 
ontological status than sized-types. They require work to be
derived as well, and the correctness proofs for them are quite
similar to that for sized types. This seems like a matter of
preference. Obviously I'm not neutral in this matter though.

I'm no Coq expert, but wasn't this idea of translating
pattern-matching to eliminators (recursors) already
the core of Cristina Cornes' PhD thesis, back in the
time where Coq only had recursors and no pattern-matching?
  I seem to recall she had already realized the difficulty
of the task, and the importance of axiom K, at least.

All the best,

- -- Jean.


-----BEGIN PGP SIGNATURE-----
Version: GnuPG/MacGPG2 v2.0.18 (Darwin)
Comment: GPGTools - http://gpgtools.org
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iQEcBAEBAgAGBQJSzY/DAAoJEBO3J6HB7Rh1WyUH/3uim2ZTsfzddH0gbCngNeFu
vqnvXmd8VPKNoH4LE9Ydhi2J4ibCmnyPH2sFi1ee6t5Kt9Oz8GhOc7HzRdlB2qsq
GpD+lxDE8I9HdokfDyYnP2RP2ZiUs2/2m1bcAJkWVZLwlcKyKiwr/yzY/lNdSIRS
J/YYIXMI/wCw1b38ZoFXvaa0okOS8IDDde2W1lybvRSO0F1ZO6qMzWwas5hD78mC
FU8MeU7xYvWOv30GRyYEl0PaUswCmmGhvVqZDH0Ttum2ONnQpQ9JhMKB6AaVZQu/
hB7/PE8vOXCFLBUMkBTfn/R655VHbs87tytgMLKE5Q+eMs5hA7u3lfEMIzzP+io=
=JLKR
-----END PGP SIGNATURE-----

Hello Jean.

You are right. Unfortunately, her PhD is in French and I know no electronic copy of it. In the credits for Coq 6.1, http://coq.inria.fr/distrib/current/refman/Reference-Manual002.html#sec5 , it is written: "Cristina Cornes designed an extension of the Coq syntax to allow definition of terms using a powerful pattern-matching analysis in the style of ML programs." You can find the table of contents of her PhD on https://who.rocq.inria.fr/Frederic.Blanqui/divers/cornes97phd-toc.pdf (messages on coq-club are limited to 39 Ko...).

Best regards,

Frédéric.


-------- Message original -------- Sujet: Diffusion des messages : erreur utilisateur Date : Thu, 09 Jan 2014 10:09:43 +0100 De : SYMPA <sympa_inria AT inria.fr> Pour : frederic.blanqui AT inria.fr

Problème de diffusion de votre message pour la liste 'coq-club' :


Votre message n'a pas pu être envoyé parce que sa taille (403 ko) était
supérieure à la taille maximum de message autorisée pour cette liste (39 ko).

Note : Comme les fichiers binaires doivent être encodés dans le format ASCII,
moins efficace, la taille finale d'une pièce jointe est souvent nettement
supérieure à celle du fichier original.

Pour plus de détails, contactez coq-club-request AT inria.fr