The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hello.

Pierre-Marie beat me to it, but here is the proof how it implies proof 
irrelevance:

Axiom sig_map_eq : forall
  {A   : Type}
  (P   : A -> Prop)
  (x y : sig P),
  proj1_sig x = proj1_sig y -> x = y.

Lemma proof_irrelevance (P:Prop) (p q : P) : p = q.
Proof.
  set (A := exist (fun I => P) I p).
  set (B := exist (fun I => P) I q).
  change p with (proj2_sig A).
  change q with (proj2_sig B).
  cutrewrite (A = B). reflexivity.
  apply sig_map_eq. reflexivity.
Qed.

Proof irrelevance is stronger than K an thus not provable in CIC and 
neither is  sig_map_eq.

A useful special case where sig_map_eq is provable is for P of the form 
(fun X => b = true).
This is used heavily in Ssreflect.

Regards
Christian




Am 02.06.2013 23:45, schrieb Floyd Lee:
> Hello list.
>
> Is this deceptively simple theorem provable in Coq's logic?
>
> Lemma sig_map_eq : forall
>    {A   : Type}
>    (P   : A -> Prop)
>    (x y : sig P),
>    proj1_sig x = proj1_sig y -> x = y.
> Proof.
>    intros A P x y H_eq.
>    destruct x as [x Hx].
>    destruct y as [y Hy].
>    simpl in H_eq.
>    rewrite H_eq.
>
> Error: Abstracting over the term "x" leads to a term
> "fun x : A => exist P x Hx = exist P y Hy" which is ill-typed.
>
> It would seem to need both proof irrelevance and functional
> extensionality. Unfortunately, I can't seem to get to the point
> that I can actually apply either of them.
>
> _____________________________________________________________
> ---
> http://mail.secureroot.com/ - free mailbox for hackers and geeks