The Coq mailing list

[Paolo Herms <paolo.herms AT inria.fr>]

Actually I think this is a bug of the injection tactic, so you may want to 
file 
a bug report.
-- 
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France

On Thursday 03 February 2011 10:02:52 
ruy.leywild AT imdea.org
 wrote:
> Hi all, in the following example I want to prove injectivity of a
> dependent pair.  Below, inj has an explicit type parameter whereas inj'
> assumes the variables have type unit.  In v8.2pl1 both proofs work; but in
> higher versions (v8.2pl2, v8.3, and v8.3pl1) the first works but the
> latter fails(!).  My current workaround is to use inj to prove inj', but
> I'd rather prove it directly if possible.  Any suggestions?
> 
> Thanks, Ruy.
> 
> 
> Require Import Eqdep.
> Set Implicit Arguments.
> 
> Record dynamic : Type := dyn {typ : Type; val : typ}.
> 
> Lemma inj A (x y : A) : dyn x = dyn y -> x = y.
> Proof. intros A x y H; injection H; apply inj_pairT2. Qed.
> 
> Lemma inj' (x y : unit) : dyn x = dyn y -> x = y.
> Proof. intros x y H; injection H; apply inj_pairT2. Qed.
> 
> > intros x y H; injection H; apply inj_pairT2.
> > 
> >               ^^^^^^^^^^^
> 
> Error: Failed to decompose the equality.