The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 01/24/2012 09:41 PM, Hugo Herbelin wrote:
> Hi,
>
> You basically exhausted the elementary bricks of types for which
> singleton elimination is allowed:
>
> recursivity: Acc
> tuples: True, and
> indices: eq
> emptyness: False
>
> Indeed, indices is where finer discriminating criteria can be thought of.
>
>    
I don't have much to add to what Hugo said. Just a couple of remarks:

- False_rect transports inconsistencies from Prop to Type: any 
proposition is inhabited implies any type is inhabited.
- singleton elimination for Acc can be viewed as the composition of the 
singleton elimination on tuples (Acc is a 1-tuple), with the possibility 
to write fixpoints with co-domain in Type, and recursive argument in 
Prop. The first part is harmless, but the second one implies False_rect: 
if we assume False, eq is a well-founded order, and we can inhabit any 
type with a well-founded recursion:
Check (fun (abs:False) (X:Type) =>
  (fix F (h:Acc eq 0) :X := F (Acc_inv h (eq_refl 0)))
    (False_ind _ abs)).
: False -> forall X : Type, X

Probably no reason to be worried in a homotopical world, though...

Bruno.

--

Bruno Barras                    Typical team - INRIA Saclay
LIX - Ecole Polytechnique       91128 Palaiseau Cedex - France
Tel: +33 1 69 33 40 57          Fax: +33 1 69 33 30 14