How to automatically leverage hypotheses of the form x <> y?

Goal forall (w x y z: string), w <> x -> (if (eqb_string w x) then y else z) = z.
Proof.
  intros.
  rewrite false_eqb_string by trivial.
  reflexivity.
Qed.

false_eqb_string is a rather trivial proof principle. I'd like to use it implicitly, via autorewrite or similar. Unfortunately, if I add Hint Rewrite false_eqb_string, then any subterm of the form eqb_string _ _ gets rewritten, and the assumption _ <> _ added to goals, even when that's not a sensible thing to do.

How can I make rewrite false_eqb_string by trivial happen automatically, without mentioning it by name?

Solution

I believe the construction you are looking for is

Hint Rewrite false_eqb_string using solve [ trivial ].

This is documented in the reference manual. Unlike rewrite ... by ..., Hint Rewrite ... using ... will not undo the rewrite if the tactic does not fully solve the side conditions, so you must wrap it in solve [ ... ] to get that effect.