The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

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/