The Coq mailing list

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

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

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). For subject reduction, I have heard that
not all Coq constructions respects it, so adding one wouldn't be that
much annoying, and last, if I well understood, adding 'eta' for
'unit_types' (eq, Acc, True, …) would repair this subject reduction.
You said that accessibility proofs certify termination, so having an
accessibility proof is enough, we do not really care which one it is.
Proof irrelevance does not provide you any one, just that two
accessibility proofs are equal. If you have none, proof-irrelevance
won't help you much to exploit anything. Then if you admit one (as you
did), then you just add some axiom, which is sound or not, but you
cannot tell much of it from my point of view.

I doubt you find it interesting, and it does not mean much, but I
instantiated pi_refl, to see what would be the outputs.

Definition pi_refl : h = h'.
  exact ((eq_refl h : (h:Acc R 1:Prop) = (h:Acc R 1:Prop))
        : (h:Acc R 1:Prop) = (h':Acc R 1:Prop)).
Defined.
Print pi_refl.
(*
pi_refl = 
(eq_refl
 :(h:Acc R 1:Prop) = (h:Acc R 1:Prop))
:(h:Acc R 1:Prop) = (h':Acc R 1:Prop)
     : h = h'
*)
Definition p : g h = false
   := resp h h' pi_refl.

Eval compute in p.
(*
     = eq_refl
     : g h = false
*)

> 
> 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.
> >
>