The Coq mailing list

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

Dear Andreas,

I like your synthesis of the situation.

If we restrict proof-irrelevance to non-recursive-singleton (Acc) and
no-with-indices-singleton (eq) propositions (*), then we have to
forbid also propositional variables, since they may get eventually
substituted by one of these propositions we want to exclude. But that
might still be interesting in practice compared to ruling out Acc
from the class of singleton propositions [ruling out Prop subset of
Type(1) is a priori an orthogonal issue] as in Matthieu's patch.

My "proposal" is currently nothing more than an informal idea. It is
not about having a "closed proof" but about having a proof whose free
variables live in inhabitable types (for some computer-checkable
criterion of inhabitability, like nat or bool are trivially checkable
inhabited) so that there is an interpretation of it in the underlying
model. If the idea can be made into a concrete proposal, this would
also give more than no proof-irrelevance at all while still not
restricting the current uses of Acc. By not having (definitional)
proof-irrelevance in non-provably inhabited types, we would loose
statements generic over propositions such as forall X:Prop,
forall p q:X, p=q but I don't know how much this would be a problem
in practical life (which I believe is mostly about getting rid of the
propositional part in subtypes made out of a concrete predicate).

Hugo

(*) In the case of eq, as was shown by Christine Paulin, the lost of a
witness of convertibility induced by proof-irrelevance (eq_refl) can
actually be recovered by effectively re-checking dynamically whether
the arguments of the equality are convertible.

On Sun, Nov 25, 2012 at 07:57:43AM +0100, Andreas Abel wrote:
> 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/