The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Thx very much Adam, Vladimir and Chris for your quick answers,
With your pointers, the situation is much clearer for me now.

Indeed inj_pair2 in EqdepFacts corresponds to what I needed.
As I understand, inj_pair2 is a consequence of the axiom eq_rect_eq
in Eqdep which expresses the "invariance by substitution of
reflexive equality proofs."

Is eq_rect_eq the axiom that has been proved independent from CIC ?

Vladimir suggests that inj_pair2 itself is refuted in a
specific (univalent) model of CIC ?

Also, the axiom eq_rect_eq is provable when restricted on
types with decidable equality and thus, the injectivity
of projT2 is provable on decidable types. This is
inj_pairT2 in Eqdep_dec.

Anyway, thanks again,

Dominique

PS: may be the Coq FAQ could mention the problem of
    the injectivity of projT2 and/or why existT is a
    constructor on which the injectivity tactic fails.

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

On 01/25/2012 09:32 PM, Adam Chlipala wrote:
> On 01/25/2012 01:57 PM, 
> Dominique.Larchey-Wendling AT loria.fr
>  wrote:
> > 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.
>
> I wish I could reply with a pointer to a standard FAQ location, but I'm
> not sure such a place exists. Nonetheless, coq-club gets this question
> every few weeks. :)
>
> The theorem you suggest is not provable in Coq; it is formally
> independent from CIC. In the [Eqdep] module of the standard library, you
> can find a proof in terms of an axiom that has been proved on paper to
> be consistent with CIC. I think the theorem is [inj_pair2].