The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 3 Feb 2011 10:02:34 +0100 (CET),
ruy.leywild AT imdea.org
 a écrit :

> 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.
> 
> 

That is not very satisfactory, but with "Print inj." you can
"reverse-enginer" the proof script to provide one,
such as:

Lemma inj' (x y : unit) : dyn x = dyn y -> x = y.
Proof.
 intro H.
 apply (inj_pairT2 Type (fun x => x)).
 apply (f_equal (fun e => match e with {|typ:=typ;val:=val|} =>
        existT (fun t => t) typ val end) H).
(* Here is a longer variation in lines of script of the previous tactic
   (but the proof term will be about the same size and probably
    slightly more readable):
 change (match {| typ := unit; val := y |} with
         {| typ := unit_; val := y_ |} =>
         existT (fun x0 : Type => x0) unit x = existT (fun x0 : Type =>
x0) unit_ y_ end).
 case H.
 split.*)
Qed.

And of course, there is the "cheat":

Lemma inj' (x y : unit) : dyn x = dyn y -> x = y.
Proof.
 case x; case y; split.
Qed.

which doesn't use H at all, but I think you're not interested in it!