Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Proof Irrelevance and injection

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof Irrelevance and injection


Chronological Thread 
  • From: Jonas Oberhauser <s9joober AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Proof Irrelevance and injection
  • Date: Wed, 14 Nov 2012 06:14:25 +0100

Hi everyone,

I got a little confused by an error message in Coq 8.3. This is a broken down example that reproduces the message:

Inductive P : Prop := p : nat -> P.

Goal forall x y, p x = p y -> x = y.
intros x y. intros e. injection e.

"Error: Nothing to do, it is an equality between convertible terms."

I assume this is because we don't want to scare proof irrelevance away. It seems a little bit harsh, though, since I'm unable to prove eg "p 4 = p 2" without assuming PI. So I don't think p 4 and p 2 are convertible. (nor do I think p x and p y are, in general).

Kind regards, jonas


  • [Coq-Club] Proof Irrelevance and injection, Jonas Oberhauser, 11/14/2012

Archive powered by MHonArc 2.6.18.

Top of Page