The Coq mailing list

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

On 23 nov. 2012, at 14:54, Hugo Herbelin 
<hugo.herbelin AT inria.fr>
 wrote:

> Hi,

<snip/>

> Matthieu said:
>> 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.
> 
> Indeed, proof-irrelevance would imply that any "fix" is definitionally
> equal to any arbitrary deep unfolding of it. How much this would
> damage the decidability of the type-checking, it is unclear to me.
> For type-checking, don't we just need an algorithm that, for any two
> expressions a and b involving fixpoints over Acc proofs, is able to
> decide the up-to-proof-irrelevance convertibility of a and b by
> needing only a finite number of unfoldings of these fixpoints in a and b.
> Is it really clear that such an algorithm does not exist?

The problem is that this "finite" number of unfoldings is unknown and
in an incoherent context you could certainly craft a conversion problem 
that would lead the algorithm to infinitely unfold the fix. 
Let's try:

Fix_F full_rel (fun F a -> if F a = 0 then 0 else 0) acc a \conv 0 <->
(if Fix_F full_rel (fun F a -> if F a...) acc a = 0 then 0 else 0) a acc 
\conv 0 <->
(if (if Fix_F full_rel (fun F a -> if F a...) acc a = 0 then 0 else 0) = 0 
then 0 else 0) \conv 0 …

Basically this reduces to the halting problem, no?

> Note that these issues are not specifically related to proof-
> irrelevance. The same would happen if one would like to have the eta
> rule for Acc, i.e. "a == Acc_intro x (Acc_inv a)" for "a:Acc R x", as
> a definitional rule.

Indeed, recursive eta rules seem just as hard to handle.
-- Matthieu

> On Fri, Nov 23, 2012 at 11:41:00AM -0500, Matthieu Sozeau wrote:
>> 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