Skip to Content.
Sympa Menu

coq-club - [Coq-Club] is this lemma provable?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] is this lemma provable?


Chronological Thread 
  • 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.



Archive powered by MHonArc 2.6.18.

Top of Page