coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: Ramon <i AT ramon.org.il>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Using sigT and existT
- Date: Thu, 29 Dec 2011 09:10:38 -0500
Ramon wrote:
I am playing around with Coq, and got stuck when trying to prove:
Lemma existT_equal
: forall T F (X : T) a b,
existT F X a = existT F X b ->
a = b.
This fact is independent of CIC. That is, it is neither provable nor disprovable. The standard library establishes [existsT_equal] under the name [EqDep.inj_pair2], appealing to an axiom. When [T] has decidable equality, you can give an axiom-free proof, for instance with [Eqdep_dec.inj_pair2_eq_dec].
- [Coq-Club] Using sigT and existT, Ramon
- Re: [Coq-Club] Using sigT and existT, Adam Chlipala
- Re: [Coq-Club] Using sigT and existT,
Chris Dams
- Re: [Coq-Club] Using sigT and existT, Ramon Snir
Archive powered by MhonArc 2.6.16.