The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

See the thread "CiC without elim restriction" from last week.  Thanks to Dan 
and Bruno for their explanations.  Gert


Am 04.12.2011 um 20:47 schrieb Adam Chlipala:

> Jelle wrote:
>> Hello,
>> 
>> When running Coq with "-impredicative-set" I would have expected the
>> following to work:
>> 
>>  Record foo : Set := mkFoo { bar : Set }.
>>  foo is defined
>>  foo_ind is defined
>>  foo_rec is defined
>> 
>> But the projection is not defined:
>> 
>>  Warning: bar cannot be defined because it is large and foo is not.
>> 
>> Trying this manually gives:
>> 
>>  Definition bar (x : foo) := match x with mkFoo b =>  b end.
>> 
>>  Error: Incorrect elimination of "x" in the inductive type "foo":
>>  the return type has sort "Type" while it should be "Prop" or "Set".
>> 
>>  Elimination of an inductive object of sort Set is not allowed on a
>>  predicate in sort Type because strong elimination on non-small
>>  inductive types leads to paradoxes.
>> 
>> What is going on here? -impredicative-set doesn't work with records?
>> And what exactly is strong elimination?
>>   
> 
> Strong elimination (usually called large elimination, actually) is a 
> [match] whose result type doesn't have type [Set] or [Prop].  Less 
> formally, it's a [match] returning a type.  A large inductive type 
> definition has at least one constructor whose type contains a "polymorphic" 
> [forall], quantifying over types.  Your [foo] is certainly one such type, 
> since the type of [mkFoo] includes quantification over [Set].
> 
> To preserve consistency, large elimination on large inductive definitions 
> in impredicative [Set] must be disallowed.  The details of this I am not 
> familiar with.