The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

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.