The Coq mailing list

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

Hi,

I'm sorry, I'm a bit lost in this discussion.

Andreas said:
> Variable pi_refl : h = h'.
> Definition p : g h = false
>   := resp h h' pi_refl.
> 
> (* If we have proof irrelevance, then pi_refl can be replaced by eq_refl.
>    But then p reduces to eq_refl, but eq_refl does not have type g h = 
> false,
> 
>    because g h does not reduce.

I don't follow. If we have proof irrelevance, then h == h' since h and
h' are in Acc R 1 with Acc R 1 : Prop (I write == for definitional
equality, aka conversion). Hence eq_refl is typable of type g h = g h',
which itself is convertible to g h = false. No?

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?

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.

No?

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