Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proof irrelevance

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof irrelevance


Chronological Thread 
  • From: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
  • To: AUGER Cédric <sedrikov AT gmail.com>
  • Cc: Andreas Abel <andreas.abel AT ifi.lmu.de>, coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Proof irrelevance
  • Date: Fri, 23 Nov 2012 11:41:00 -0500

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


Archive powered by MHonArc 2.6.18.

Top of Page