The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Here is an attempt at a systematic explanation:

A term of a (possibly recursive) singleton type does not have any 
run-time content and can be safely erased during extraction, because at 
run-time all terms are closed, thus a singleton type does really have at 
most one canonical inhabitant.

At type-checking type, the situation is different.  There are infinitely 
many open terms that inhabit a singleton type.  The question is whether 
they bear different information.  This is indeed the case at least for 
recursive singleton types and for non-linear dependent families such as 
the identity type.

The information contained in h : Acc R e, for instance, is how often you 
may unfold a function defined by well-founded recursion on relation R 
called at term e with accessibility proof h.

As discussed by you below, if you have eta-expansion for recursive 
singleton types, then you destroy this information, justifying proof 
irrelevance, but you also destroy strong normalization.  If you do not 
have eta-expansion, you destroy subject reduction if you accept proof 
irrelevance (as I demonstrated).

Things which do contain (computational) information cannot be made 
irrelevant (unless you take away means to eliminate them, but then, in 
my opinion, you also remove the information).

So, we cannot have proof irrelevant for all of Prop unless we restrict 
singleton elimination to propositions whose proofs have really no 
content.  This excludes singleton elimination for some recursive 
propositions like Acc and for non-linear families such as the identity type.

A systematic solution is to have a sub-universe of Prop that contains 
only propositions whose proofs you are either not allowed to eliminate 
(they are not singleton propositions) or which do not have any content 
at type-checking time.

Effectively, there is already a sub-universe of Prop: singleton props. 
One could treat the sub-universe of proof-irrelevant props similar: 
whenever the type checker compares two proofs for definitional equality, 
it can immediately succeed if the proposition belongs to this 
sub-universe.  (Internally one could try to be smarter and keep track of 
the sub-universes.)

@Hugo, do I understand your proposal correctly, that you want proof 
irrelevance for those propositions P that have a closed proof?

I guess or would also want proof irrelevance for non-recursive empty 
propositions, or?

Cheers,
Andreas

On 24.11.12 6:58 PM, Hugo Herbelin wrote:
> 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

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/