The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 24/06/2020 12:58, Thorsten Altenkirch wrote:
> If you have functions you need funext, the function type is a basic
> coinductive type and this is its coinduction principle. Otherwise you
> could also argue that you don’t need induction for natural numbers and
> each time when you say something about natural numbers you relativize
> this to the inductive ones. Actually we were doing these sort of things
> when working in the pure calculus of constructions in the 1980ies.

Well, I'd be personally happy to have a variant of CIC with a restricted
form of dependent elimination compatible with effects. The weaker the
theory your proof depends on, the more "portable" it is to stronger
theories, which are potentially inconsistent between one another.

I usually liken this the case of languages with hard-wired concurrency
features: there are people who only ever write sequential programs and
that would be happy not to have to put locks everywhere for many of
their imperative structures to keep working, not even talking about the
runtime cost of the latter.

Accepting funext unconditionally breaks most of the models I design for
a living. A lot of people have been working in a theory without funext
without fuss, it would be sad to prevent them from using whatever
logical principles these models implement.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature