coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof irrelevance

From: Frederic Blanqui <frederic.blanqui AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof irrelevance
Date: Tue, 27 Nov 2012 10:07:45 +0800

Hello.

I did not follow all this complex but interesting discussion but the last mail of Andreas makes me strongly think of Pierre-Yves Strub's PhD work (and its later improvements, see http://pierre-yves.strub.nu/) where the conversion is enriched by considering equivalent two terms that are so in some first-order equational theory extended with assumptions extracted from the context, that can be seen as a form of proof irrelevance. In order to ensure subject reduction, termination and decidability, some conditions are added on quantifications, etc. This can perhaps be helpful to the problems that you are discussing. Note also that Pierre-Yves implemented this system above Coq 8.3pl3 (see http://pierre-yves.strub.nu/coqmt/) and formalized it in Coq.

Regards,

Frederic.

Le 26/11/2012 23:40, Andreas Abel a écrit :

Dear Hugo,

On 26.11.2012 06:10, Hugo Herbelin wrote:

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.

I agree. In the case of singleton elimination one never gets into the situation of a propositional variable, so the situation is a bit different. If one wants to have proof irrelevance for some subset of Prop that includes propositional variables, I am afraid that one needs a new explicit universe like Prop-irr such that one can restrict quantification to

forall (X : Prop-irr), ...

accordingly. That this is not too nice for the users who must make a choice between Prop and Prop-irr is the dilemma. [I have been questioned quite a bit why Agda's irrelevance is not completely transparent (automatic irrelevance inference), and this is for a similar reason...]

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

Aha, I misunderstood you before. So you say that a proof does not have to live in the empty context, but a consistent (=satisfiable) context. If I understand you correctly this time, you want proof irrelevance for propositions of positive logic, those proven without ex-falsum-quodlibet. This is, of course, excluding postulated lies that cause all the trouble. Let me try a rule:

Gamma |- p, q : P : Prop |- sigma : Gamma
-------------------------------------------
Gamma |- p = q : P

Immediately justified is |- p[sigma] = q[sigma] : P[sigma], since proof irrelevance is safe for closed terms. However, the rule says (in terms of a Kripke model)

forall Delta |- rho : Gamma,
Delta |- p[rho] = q[rho] : P[rho]

and I cannot see how this is supposed to follow. It might be correct nevertheless, with a non-trivial proof.

Also, I do not see how this fixes the subject reduction problem with use of Acc. My counterexample can be adapted such that it does not use lies, just a postulated proof h of accessibility. Still, the recursive function would not reduce if applied to h, but it would reduce if applied to the eta-expansion of h. If you equate these, just because there are no lies flying around, you lose subject reduction.

To avoid subject reduction, you need at least also eta-expansion for singleton types. But eta-expansion might not terminate for recursive singletons, e.g.

Inductive Empty : Prop := | empty : (fromEmpty : Empty) -> Empty

h : Empty -->eta empty (fromEmpty h) -->eta ... diverges

Seems all very tricky. A clear but inconvenient solution is the extra Prop-irr universe...

(*) 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.

Yes, I have seen this. I guess this can be generalized to other non-linear families of propositions, but the changes to the reduction machinery and matching construct would be quite invasive. I tried to solve this problem by eta-expansion

p : t = u --> refl : t = u if t and u are convertible

however, I did not get very far. See

@STRING{nbe09 = "Workshop on Normalization by Evaluation, affiliated to
LiCS 2009, Los Angeles, 15 August 2009" }

@InProceedings{ abel:nbe09,
author = {Andreas Abel},
title = {Extensional Normalization in the Logical Framework with
Proof Irrelevant Equality},
booktitle = nbe09,
year = 2009,
editor = {Olivier Danvy}
}

Cheers,
Andreas

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/

Re: [Coq-Club] Proof irrelevance, (continued)