The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

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