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: 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/



Archive powered by MHonArc 2.6.18.

Top of Page