The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

The original design choice of the injection tactic (and hence of
inversion which uses injection) was to skip injection of subterms of
type a proposition and obviously the related error message "Nothing to
do, it is an equality between convertible terms" is wrong.

I tried to activate injection of subterms of type a proposition, but
the resulting behavior is not really convincing because most of the
time these proofs depends on other subterms and injection produces
sigma-expressions difficult to deal with.

So, my current view would be to keep injection as it is, considering
that for proofs of the kind of the lemma L1 below, one has to give up
using injection.

An alternative could be to make available a flag controlling the
behavior of injection, or to provide a variant of injection that works
on subterms are proofs. But would there be a lot of lemmas that would
benefit of such a variant?

Hugo Herbelin

From Christian Doczkal:
> 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
>