The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> Me and Claudio Sacerdoti Coen were investigating some bugs concerning
> the generation of elimination principles in a proof assistant we are
> developing at the university of Bologna (based on CiC).

> Since we found no clear explanations in the literature, we made some
> tests with coq-8 (with and without the -impredicative-set flag).
> Our result follow. We would be really happy to know if we are right or
> not (and if we decorated the "no" answers with the right cause).
> 
> Table of allowed eliminations:
> 
>             +--------------------+---------------------------+  
>             |   Inductive Type   |    Elimination to         |
>             +--------------------+---------------------------+
>             | Sort | "Smallness" | Prop | SetI | SetP | Type |
>             +--------------------+---------------------------+
>             | Prop     unit      | yes    yes    yes    yes  |
>             | Prop     small     | yes    [yes]  no2    no12 |
>             | Prop               | yes    no2    no2    no12 |
>             | SetI     small     | yes    yes    --     no1  |
>             | SetI               | yes    yes    --     no1  |
>             | SetP     small     | yes    --     yes    yes  |
>             | SetP     (* inductive type is rejected *)      |
>             | Type               | yes    yes    yes    yes  |
>             +--------------------+---------------------------+

  The [yes] should be a no2, as implemented in Coq. Actually, since
non-unit Prop behaves the same, the second and third line can be
merged (the only difference is that the no12 is simply a no2 in the
small Prop case).

  The no1 from small SetI to Type is probably a typo, it should be a yes.

> Legenda:
> 
>   1 : due to paradoxes a la Hurkens 
>   2 : due to code extraction
>   
>   [yes] : Current version of Coq rejects this, but a comment in the source 
>           code seems to allow this elimination. (See indtypes.ml line 479)
> 
>   SetP : Predicative Set
>   SetI : Impredicative Set
> 
>   very-small : Constructor arguments are in Prop only
>   small : Constructor arguments are not in Type
>   unit : Non (mutually) recursive /\ only one constructor /\ very-small

  Hugo Herbelin