The Coq mailing list

[Enrico Tassi <gareuselesinge AT virgilio.it>]

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

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


Thanks in advance
-- 
Enrico Tassi