The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 23 Oct 2012 12:19:57 +0200,
Pierre-Marie Pédrot 
<pierre-marie.pedrot AT inria.fr>
 a écrit :

> I'm almost sure this has already been discussed here, but I can't find
> it anymore, so I'm asking before doing anything wrong.
> 
> Here is my problem: is there something subtle I'm missing between the
> two following (co)inductive definitions, or is this, as I think I read
> somewhere, a unimplemented feature?
> 
> This works:
> 
> Inductive toto :=
> | Toto : (unit -> toto) -> toto.
> 
> This does not, because Coq asserts it would break the positivity
> condition:
> 
> Inductive titi :=
> | Titi : (forall p, match p with tt => titi end) -> titi.
> 
> This seems really odd to me. Is there any metatheoretical result
> forbidding this or may I already write the patch fixing this (which I
> badly need and did not manage to somehow bypass when working with
> coinductives)?

I do not know what kind of patch you intend to do.

Recently, people have spoken of généralization of eta-expansion to
other structures than functions. I guess it is one of these cases here:

match p with
| tt => titi
end

is clearly equivalent to "titi".

But I bet you want something different than your dummy example.

Some restriction of the positivity condition is required to ensure
soundness. But Coq positivity restriction is too strong and should
allow more terms. Unfortunately as far as I guess, the strict
requirements are not well known, so many good type definitions are
refused by the typechecker, whereas they could be allowed.

What exactly would your patch do?