The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

-----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-----