Coq: automate repeated rewriting

Example test: forall f (n: nat), f n = n -> f (f n) = n.
Proof.
  intros f n H. repeat rewrite H. reflexivity.
Qed.

What would be a good way to further automate this? In particular, I would like to not have to mention the name of the hypothesis anywhere.

Solution

If the goal can be solved with some sequence of rewrites, then the congruence tactic can handle it.

The tactic congruence, by Pierre Corbineau, implements the standard Nelson and Oppen congruence closure algorithm, which is a decision procedure for ground equalities with uninterpreted symbols. It also include the constructor theory (see 8.5.7 and 8.5.6). If the goal is a non-quantified equality, congruence tries to prove it with non-quantified equalities in the context. Otherwise it tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis.

congruence is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the members of the equality must contain all the quantified variables in order for congruence to match against it.

The above basically means that congruence can solve your goal if it can be solved using rewrite and discriminate tactics. But sometimes congruence can't help you because it does not unfold definitions for you -- in that case you'll have to help it.

Example test: forall f (n: nat), f n = n -> f (f n) = n.
Proof. congruence. Qed.