How to add Coq automation hints that can't be applied twice (for e.g. transitivity)

try_once.v

(** Support writing external hints for lemmas that must not be applied twice for a goal. *)
(* The usedLemma and un_usedLemma marker is taken from Crush.v (where they were called done and un_done). *)

(** Devious marker predicate to use for encoding state within proof goals *)
Definition usedLemma {T : Type} (x : T) := True.

(** After a round of application with the above, we will have a lot of junk [usedLemma] markers to clean up; hence this tactic. *)
Ltac un_usedLemma :=
  repeat match goal with
           | [ H : usedLemma _ |- _ ] => clear H
         end.
Ltac markUsed H := assert (usedLemma H) by constructor.

Ltac try_once lm :=
    match goal with
    | H : usedLemma lm |- _ => fail 1
    | _ => markUsed lm; eapply lm
    end.

(** Example. *)
(* Hint Extern 10 => try_once Trans_stp : core. *)


Tactic Notation "try_once_tac" constr(T) tactic(tac) :=
  match goal with
  | H : usedLemma T |- _ => fail 1
  | _ => markUsed T; tac
  end.

(** Example. *)
(* Definition injectHyps_marker := 0. *)
(* Hint Extern 5 => try_once_tac injectHyps_marker injectHyps : core. *)