In-place simplification for Coq

Question

I want this goal:

Goal forall (A : Type) (j' : nat) (f : nat -> A), f (S j') = f (j' + 1).
forall (A : Type) (j' : nat) (f : nat -> A),
f (S j') = f (j' + 1)

to be proven automatically by Coq. Currently I have to write:

  intros.
A: Type
j': nat
f: nat -> A
f (S j') = f (j' + 1) apply f_equal.
A: Type
j': nat
f: nat -> A
S j' = j' + 1 lia.

But in general it can be more difficult and I might need to assert for instance that m - 0 = m and then rewrite. Is there a way to rewrite a term in-place, as Isabelle has?

Answer

I'm not sure exactly what you want. Perhaps the replace tactic can be of help to you.

Basically you would write

  intros.
A: Type
j': nat
f: nat -> A
f (S j') = f (j' + 1) replace (S j') with (j' + 1).
A: Type
j': nat
f: nat -> A
f (j' + 1) = f (j' + 1)
A: Type
j': nat
f: nat -> A
j' + 1 = S j'
  - (* f (j' + 1) = f (j' + 1) *)
A: Type
j': nat
f: nat -> A
f (j' + 1) = f (j' + 1)
    reflexivity.
  - (* j' + 1 = S j' *)
A: Type
j': nat
f: nat -> A
j' + 1 = S j'
    lia.

(Note that I'm using lia and not omega as omega is deprecated in favour of lia.)

You can even discharge the replacement directly by lia:

  intros.
A: Type
j': nat
f: nat -> A
f (S j') = f (j' + 1) replace (S j') with (j' + 1) by lia.
A: Type
j': nat
f: nat -> A
f (j' + 1) = f (j' + 1)
  reflexivity.

This way the replacement only succeeds if lia is able to solve the needed equality.