1
$\begingroup$

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

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?

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Jan 11 at 7:04
  • $\begingroup$ 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? $\endgroup$ Jan 11 at 10:21

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.