Although the notion of "invariant" is not completely generic, all of the "Iris derivative" logics (Iron, Fair refinements) have such a construct. At present each of these logics needs to redefine its own iInv tactic which is undesirable. Moreover, there are at least a few invariant-like things within Iris itself, including non-atomic and cancelable invariants which do not work with "iInv" -- instead one has to manually use iMod with the appropriate accessors.
This MR tries develops such a general tactic.
#94 (closed) is related, but the goals here are less ambitious, since the tactic still produces a "Hclose".