How can I rewrite selectively in Coq?

Question

Require Import Coq.Arith.Arith.

Section foo.

  Variable a : nat.
  Variable fvs : list nat.
  Variable maxNum : list nat -> nat.
  Hypothesis H : a = max (maxNum fvs) a + 1.
  Hypothesis H1 : max (maxNum fvs) a >= a.

  Goal False.
a: nat
fvs: list nat
maxNum: list nat -> nat
H: a = Init.Nat.max (maxNum fvs) a + 1
H1: Init.Nat.max (maxNum fvs) a >= a
False

Doing rewrite H in H1., replaces both the as whereas I only want to rewrite the a on the RHS. Can it be done? I want to prove false from the above two hypotheses.

Answer

One option is to use rewrite ... at <position>. like so:

    rewrite H in H1 at 2.
a: nat
fvs: list nat
maxNum: list nat -> nat
H: a = Init.Nat.max (maxNum fvs) a + 1
H1: Init.Nat.max (maxNum fvs) a >=
Init.Nat.max (maxNum fvs) a + 1
False

What you want can also be done in a slightly different way. Observe that max (maxNum fvs) a is irrelevant here -- you can use any natural number instead of that expression and your theorem would still hold. That means you can use the generalize tactic.

    Undo.
a: nat
fvs: list nat
maxNum: list nat -> nat
H: a = Init.Nat.max (maxNum fvs) a + 1
H1: Init.Nat.max (maxNum fvs) a >= a
False
    revert H H1.
a: nat
fvs: list nat
maxNum: list nat -> nat
a = Init.Nat.max (maxNum fvs) a + 1 ->
Init.Nat.max (maxNum fvs) a >= a -> False generalize (max (maxNum fvs) a) as n.
a: nat
fvs: list nat
maxNum: list nat -> nat
forall n : nat, a = n + 1 -> n >= a -> False
    intros n ->.
fvs: list nat
maxNum: list nat -> nat
n: nat
n >= n + 1 -> False rewrite Nat.add_1_r.
fvs: list nat
maxNum: list nat -> nat
n: nat
n >= S n -> False
    apply Nat.nle_succ_diag_l.
  Qed.

End foo.