coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] is this lemma provable?
- Date: Sat, 16 Mar 2013 21:31:34 -0300
Hello,
Consider the following types:
Inductive T : Type :=
a : T.
Inductive H : T -> Type :=
b : H a.
I have proved this trivial lemma:
Lemma provable :
forall x : T, x = a.
Proof.
intro x.
destruct x.
auto.
Qed.
But I couldn't prove this one:
Lemma unprovable :
forall q : H a, q = b.
Proof.
intro q.
Abort.
Could anyone explain me why? Has to do with proof irrelevance?
Thank you in advance.
- [Coq-Club] is this lemma provable?, Leonardo Rodriguez, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Adam Chlipala, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Thierry Martinez, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Adam Chlipala, 03/18/2013
- [Coq-Club] Second Call for Papers, PxTP 2013, Laurent Théry, 03/18/2013
- Re: [Coq-Club] is this lemma provable?, Adam Chlipala, 03/18/2013
- Re: [Coq-Club] is this lemma provable?, Thierry Martinez, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Daniel Schepler, 03/17/2013
- Re: [Coq-Club] is this lemma provable?, Adam Chlipala, 03/17/2013
Archive powered by MHonArc 2.6.18.