The Coq mailing list

[Christine Paulin <paulin AT lri.fr>]

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

A few remarks :

no2 should not only be related to extraction, but also to the possibility 
to contradict proof irrelevance (if you define Bool in Prop, you will
be able to prove true<>false)

Prop small SetI should also be marked no2 

SetI small Type should be yes

Christine Paulin


 > 
 > 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
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86