coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y

From: "Floyd Lee" <undecidable AT secureroot.com>
To: "Christian Doczkal" <doczkal AT ps.uni-saarland.de>
Cc: <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y
Date: Mon, 3 Jun 2013 07:13:12 -0700

Thanks to all that replied.

I eventually stumbled upon:

Require Import Coq.Logic.ProofIrrelevance.

Lemma sig_map : forall
{A : Type}
(P : A -> Prop)
(x : sig P)
(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.
subst x.
rewrite (@proof_irrelevance (P y) Hy Hx).
reflexivity.
Qed.

Which would seem to be in line with the other solutions provided.

_____________________________________________________________
---
http://mail.secureroot.com/ - free mailbox for hackers and geeks

[Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Floyd Lee, 06/03/2013
- Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Adam Chlipala, 06/03/2013
- Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Pierre-Marie Pédrot, 06/03/2013
  - Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Pierre-Marie Pédrot, 06/03/2013
- Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Christian Doczkal, 06/03/2013
- <Possible follow-up(s)>
- Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Floyd Lee, 06/03/2013