The Coq mailing list

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

Hi Jeremy,

You can try (apply f_equal with ...), injectivity or inversion

Best,

D.

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

Section eq.

  Variable (X : Type) (a b c d : X).

  Fact eq1 : (a,b) = (c,d) -> a=c.
  Proof.
    intros H.
    apply f_equal with (f := fst) in H.
    simpl in H.
    trivial.
  Qed.

  Fact eq2 : (a,b) = (c,d) -> a=c.
  Proof.
    injection 1.
    trivial.
  Qed.

  Fact eq3 : (a,b) = (c,d) -> a=c.
  Proof.
    inversion 1.
    trivial.
  Qed.

End eq.

----- Mail original -----
> De: "Jeremy Dawson" 
> <Jeremy.Dawson AT anu.edu.au>
> À: "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Vendredi 14 Décembre 2018 04:14:13
> Objet: Re: [Coq-Club] injectivity of constructors

> Thanks all for the various replies, but injection doesn't work,
> giving error
> Ltac call to "injection" failed.
> Error: Not a negated primitive equality.
> 
> Jeremy
> 
> On 12/14/2018 02:07 PM, Jasper Hugunin wrote:
>> `injection` seems to fit your description, see
>> https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.injection.
>> 
>> - Jasper Hugunin
>> 
>> On Thu, Dec 13, 2018 at 4:54 PM Lily Chung 
>> <ikdc AT mit.edu
>> <mailto:ikdc AT mit.edu>>
>>  wrote:
>> 
>>     That follows from general properties of equality, and has nothing to
>>     do with constructors.  Try f_equal.