The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

On 22 nov. 2012, at 03:51, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:

> Le Thu, 22 Nov 2012 01:42:48 +0100,
> Andreas Abel 
> <andreas.abel AT ifi.lmu.de>
>  a écrit :
> 
>> Adding proof irrelevance to breaks Coq breaks subject reduction,
>> because of singleton elimination.  Proof irrelevance equates all
>> accessibility proofs, but accessibility proofs are used to certify
>> termination.  Here is an exploit:
> 
> I do not really see your point with an example which is absurd (I mean
> that with your 'Variable h', you can prove False, so that I could
> prove 'g h = true' as well).

Indeed Variable h : Acc R 1. is equivalent to False already,
but subject reduction should hold in any context as we do
reduction under arbitrary contexts.

Look at it this way: definitional proof irrelevance for Acc in Prop can 
hold only if singleton elimination is forbidden for it still.
Otherwise, the definitional equational theory should validate
[forall a : Acc, Fix F a = Fix F (Acc_intro a) = F [Fix F a]]. Clearly
[Fix F a = F [Fix F a]] will be hard to handle as a terminating rewrite
system, it leads to infinite reductions.

> For subject reduction, I have heard that
> not all Coq constructions respects it, so adding one wouldn't be that
> much annoying.

Really? I would be less annoyed if everything did respect SR. 

> and last, if I well understood, adding 'eta' for
> 'unit_types' (eq, Acc, True, …) would repair this subject reduction.

The only way to fix the non-termination would be to say that singleton 
elimination should be allowed for computationally-irrelevant types only,
which removes Acc's elimination into Set/Type. Then the issue that Andreas
mentioned goes away as well.

I have a patch that adds proof-irrelevance with the additional restriction
that Prop </= Type (but Prop : Type(1) still). It's not up to date with
the trunk though, but I can send it to you if you want to try it.

-- Matthieu