coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andreas Abel <andreas.abel AT ifi.lmu.de>
- To: AUGER Cédric <sedrikov AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Proof irrelevance
- Date: Thu, 22 Nov 2012 01:42:48 +0100
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:
Section PI.
Definition isZero (n : nat) : bool
:= match n with
| O => true
| S _ => false
end.
Variable R : nat -> nat -> Prop.
Variable full : forall (x y : nat), R x y.
Definition
f : forall (x : nat), Acc R x -> nat
:= Fix_F (fun A => nat) (fun x f => S (f x (full x x))).
Variable h : Acc R 1.
Definition h' : Acc R 1 := @Acc_intro nat R 1 (Acc_inv h).
Definition g h := isZero (f 1 h).
Definition resp (h h' : Acc R 1) (p : h = h') : g h = g h'
:= match p with
| eq_refl => eq_refl
end.
Variable pi_refl : h = h'.
Definition p : g h = false
:= resp h h' pi_refl.
(* If we have proof irrelevance, then pi_refl can be replaced by eq_refl.
But then p reduces to eq_refl, but eq_refl does not have type g h = false,
because g h does not reduce.
Subject reduction is lost (once more).
*)
End PI.
Cheers,
Andreas
On 21.11.12 7:33 PM, AUGER Cédric wrote:
Hi all,
on a local copy of trunk I patched my term.ml as this to try to have
natively proof irrelevance.
cedric@Dakkon ~/c/trunk @> svn diff
kernel/term.ml Index: kernel/term.ml
===================================================================
--- kernel/term.ml (révision 15989)
+++ kernel/term.ml (copie de travail)
@@ -567,6 +567,8 @@
| Meta m1, Meta m2 -> Int.equal m1 m2
| Var id1, Var id2 -> Int.equal (id_ord id1 id2) 0
| Sort s1, Sort s2 -> Int.equal (Pervasives.compare s1 s2) 0 (**
FIXME **)
+ | Cast (_, _, Cast (t1, _, Sort(Prop Null))),
+ Cast (_, _, Cast (t2, _, Sort(Prop Null))) -> f t1 t2
| Cast (c1,_,_), _ -> f c1 t2
| _, Cast (c2,_,_) -> f t1 c2
| Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
With it, it appears I can prove proof-irrelevance axiom-free (although
it is not convenient at all…)
Lemma Proof_irrelevance:
forall (P : Prop) (a b : P), a = b.
intros.
exact (((eq_refl a) : (a:(P:Prop)) = (a:(P:Prop))) :
(a:(P:Prop)) = (b:(P:Prop))).
Qed.
I guess someone already tried this kind of stuff, so I was wondering
what are the badpoints in doing so.
* having a bad support of proof-irrelevance stuff[1]
* inconsistency with some axioms
* looks too much like a hack (and in fact it is one…), so it is not
elegant and may be fragile
* having to cast types is not really better than using some external
axiom
Maybe other points…
Some other question, what is the "(** FIXME **)" in the line just above
my patch?
[1] For example, this does not work, you need to be a little more
clever (I did not really tried to do it, but I know how to do it):
Goal forall (T : Type) (P : T -> Prop) (x y : sig P),
let (a, _) := x in let (b, _) := y in a = b ->
x = y.
Proof.
intros.
destruct x; destruct y.
intros; subst.
change (exist P x0 (p:P x0:Prop) =
exist P x0 (p0:P x0:Prop)).
change (exist P x0 (p:P x0:Prop) =
exist P x0 (p:P x0:Prop)).
clear p0.
split.
Qed.
--
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/
- [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, 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.