# How to apply constructor injectivity in the goal

Suppose I have a goal

Goal forall m n, S m = S n -> m = n.
intros m n H.

1 goal

m, n : nat
H : S m = S n
============================
m = n


I know that I can use injection H as H to transform H to m = n. However, sometimes I would like to transform the goal instead. In the specific case of nat, there is the lemma eq_add_S:

Goal forall m n, S m = S n -> m = n.
intros m n H.

1 goal

m, n : nat
H : S m = S n
============================
S m = S n


However, is there a tactic like injection that will work for any constructor?

• But injection H (without as) just changes the goal, leaving the context unchanged. Then you can use intro, rewrite, subst, etc., to resume your proof. Jan 11 at 7:04
• It is a bit of a mouthful, but you can do enough (S m = S n) by congruence.. What should be the behaviour of the tactic you envision? In particular, what if the inductive type has two constructors (think nat with an extra S' : nat -> nat), what goal should the tactic generate in your setting? S m = S n? S' m = S' n? Something else? Jan 11 at 10:21

You can write an ad-hoc tactic


Ltac injection_goal v :=
match goal with
|- ?A = ?B =>
let H := fresh "H" in assert (H: v A = v B); try now injection H
end.

Goal forall m n,  S m = S n -> m = n.
intros m n H.
injection_goal S.