coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christian Doczkal <doczkal AT ps.uni-saarland.de>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] odd behavior of inversion and injection
- Date: Wed, 16 Jun 2010 10:44:44 +0200
Dear Coq-Club
I noticed some very odd behavior of the inversion and injection tactic.
Consider the following proof script:
(** ======================= BEGIN COQ ============================= **)
Definition eq_sig := forall A a (P : A -> Prop) p q , exist P a p = exist P a
q.
Definition proof_irrelevance := forall (P : Prop) (p q : P) , p = q.
Lemma L1 : eq_sig -> proof_irrelevance.
intros eqsig P p q.
assert (H := eqsig True I (fun _ => P) p q).
inversion H. (* does nothing *)
(* injection H. *)
(* fails with: Error: Nothing to do, it is an equality between convertible
terms. *)
(* change (exist (fun _ : True => P) I q = exist (fun _ : True => P) I q) in
H. *)
(* this (fortunately) fails with: Error: Not convertible. *)
Abort.
(* Doing the same proof with sigT and booleans (a convoluted way of proving
False -> False)
works as expected *)
Definition eq_sigT := forall A a (P : A -> Type) p q , existT P a p = existT
P a q.
Definition bool_irrelevance := forall (p q : bool) , p = q.
Lemma L2 : eq_sigT -> bool_irrelevance.
intros eq p q. assert (H := eq True I (fun _ => bool) p q).
injection H. apply id.
Qed.
(* Furthermore, changing "sigT => sig" and "bool => Prop" in L2
also makes the first lemma go through *)
Lemma L1 : eq_sig -> proof_irrelevance.
Proof (
fun (eq0 : eq_sig) (P : Prop) (p q : P) =>
let H := eq0 True I (fun _ : True => P) p q in
let H0 :=
f_equal (fun e : sig (fun _ : True => P) => let (_, b) := e in b) H in
let H1 := id (A:=p = q) in H1 H0
).
(** ======================= END COQ ============================= **)
So at the very least, the error message injection provides is wrong. But
moreover I find the error somewhat puzzling since the proof term that
should be constructed (right?) does indeed check. Does someone know what
is going wrong there?
--
Regards
Christian
- [Coq-Club] odd behavior of inversion and injection, Christian Doczkal
- Re: [Coq-Club] odd behavior of inversion and injection, Hugo Herbelin
Archive powered by MhonArc 2.6.16.