Search code examples
coqcoq-tactic

Coq inversion tactic that works on the goal?

I was wondering if there is an inversion-like tactic in Coq that works on the goal instead of on one of the hypotheses? That is, if there is some tactic that can invert identical constructors in equalities on the goal.

For a silly example, 

Goal forall x :nat, 2 + x + 3 = x + 5.
 intros. simpl.

, which gives

S ( S (x + 3) ) = S ( S ( S ( ... x)...)

I wanted to invert the first two S, so that what remains to prove is 

  x + 3 = 3 + x

My questions are

  1. Is this "inversion" of constructors sound?

  2. If the logic is sound, is there a tactic in Coq to do it?

Solution

  • The same question was answered a couple of days ago. There is no "inversion" involved in what you want to do, simple equality will do:

    Goal forall x :nat, 2 + x + 3 = 5 + x.
Proof.
intros; simpl.
assert (x + 3 = 3 + x). admit.
now rewrite H.

    To simplify this pattern, Coq provides a simple goal congruence tactic, try:

    intros; simpl; repeat f_equal.