coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Proof irrelevance, AUGER Cédric, 11/21/2012
- Re: [Coq-Club] Proof irrelevance, Andreas Abel, 11/22/2012
- Re: [Coq-Club] Proof irrelevance, AUGER Cédric, 11/22/2012
- Re: [Coq-Club] Proof irrelevance, Matthieu Sozeau, 11/23/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/23/2012
- Re: [Coq-Club] Proof irrelevance, Matthieu Sozeau, 11/24/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/24/2012
- Re: [Coq-Club] Proof irrelevance, Andreas Abel, 11/25/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Guillaume Melquiond, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Guillaume Melquiond, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Arnaud Spiwack, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Guillaume Melquiond, 11/26/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/24/2012
- Re: [Coq-Club] Proof irrelevance, Matthieu Sozeau, 11/24/2012
- Re: [Coq-Club] Proof irrelevance, Hugo Herbelin, 11/23/2012
- Re: [Coq-Club] Proof irrelevance, Matthieu Sozeau, 11/23/2012
- Re: [Coq-Club] Proof irrelevance, AUGER Cédric, 11/22/2012
- Re: [Coq-Club] Proof irrelevance, Andreas Abel, 11/22/2012
Archive powered by MHonArc 2.6.18.