coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.