The Coq mailing list

[Dominique.Larchey-Wendling AT loria.fr]

Hi,

I am new to this list and perhaps my question is a bit naive but how can I 
prove
the following result ?

Section Test.
  
  Variable X : Type.
  Variable P : X -> Type.

  Proposition projT2_fun (x : X) (s1 s2 : P x) : existT _ x s1 = existT _ x s2
-> s1 = s2.


Indeed the 3 following proof attempts fail ...

  Proof.
    intros H. injection H.

===> does not fail but does not generate s1 = s2 as an hypothesis. Instead
     it generates "existT _ x s1 = existT _ x s2" which of course does not 
help.

then

  Proof.
    intros H. 
    assert (s1 = projT2 (existT P x s1)) as H12; auto.
    assert (s2 = projT2 (existT P x s2)) as H22; auto.
    rewrite H12, H22.
    rewrite H.

===> gives an error message like

Error: Abstracting over the term "existT P x s1" leads to a term
"fun s : sigT P => projT2 s = projT2 (existT P x s2)" which is ill-typed.

then

  Proof.
    intros H. 
    assert (s1 = projT2 (existT P x s1)) as H12; auto.
    assert (s2 = projT2 (existT P x s2)) as H22; auto.
    rewrite H12, H22.
    dependent rewrite -> H.

===> gives an error message like

Error: Cannot find a well-typed generalization of the goal that makes the
proof progress.

---------------------------

I might have missed some important point about dependent equalities/types ...

Any help will be much appreciated.