The Coq mailing list

[Jasper Hugunin <jasperh AT cs.washington.edu>]

Ah, except you are trying to go in the reverse direction as I initially read the question. Sorry for my misunderstanding.

As others have said, this works for any function, not just constructors.

- Jasper Hugunin

On Thu, Dec 13, 2018 at 7:55 PM Jasper Hugunin <jasperh AT cs.washington.edu> wrote:

To use injection in the way you want to, you need to specify a term. Please do check the docs. Here is a minimal working example:

```

Goal forall a b c d : nat, pair a b = pair c d -> (a = c) * (b = d).

intros a b c d H.

injection H.

intros e2 e1.

exact (pair e1 e2).

Qed.

```

- Jasper Hugunin

On Thu, Dec 13, 2018 at 7:15 PM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

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