The Coq mailing list

[Hugo Herbelin <hugo.herbelin AT inria.fr>]

Hi,

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

I agree (Guillaume Melquiond actually convinced me offline that the
halting problem was simulable in an inconsistent context). I know this
topic has been discussed in length already several years ago but it
happens I'm still confused about it.

So, would it make sense to have "limited" proof-irrelevance which
would only make equal proofs known to be inhabitable (for some
syntactic criterion of inhabitability, based on what the user already
proved to be inhabitable)? This would rule out the ability to unfold
fixpoints whose termination is not justified by a model of Coq. But
this would still allow to make definitionally equal most of the proofs
it is convenient to identify in practice (like two proofs of "x<y", or
two proofs of "Acc lt x").

Hugo

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