General Invariant Tactic

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".

@robbertkrebbers

changed title from WIP Joe/inv tac to WIP General Invariant Tactic

changed the description

#94 (closed) is related, but the goals here are less ambitious, since the tactic still produces a "Hclose".

I think this is actually entirely orthogonal -- generalizing the tactic to "anything that satisfies the accessor", and changing its UI to no longer produce "Hclose". This MR does the former only, which seems desirable on its own. So, I agree we can ignore #94 (closed) for this discussion.

added 1 commit

• cd1bc1a7 - Simplify iInv tactic; start to extend for support for cinv and na_inv.

Compare with previous version

added 1 commit

• f65b6336 - More robust hypothesis selection in iInv; Handles cinv usage in spanning tree example.

Compare with previous version

added 1 commit

• b8f25cc0 - iInv: support for selection which auxiliary hypotheses to use (e.g. for na_own); more tests.

Compare with previous version

added 1 commit

• 61ea67f9 - Move iInv into generic proofmode directory; documentation. Move namespaces to bi/lib/

Compare with previous version

added 11 commits

• 61ea67f9...ddd48268 - 7 commits from branch gen_proofmode
• d9042f31 - WIP general invariant tactic.
• fd0ded6f - More robust hypothesis selection in iInv; Handles cinv usage in spanning tree example.
• 6ccd0a13 - iInv: support for selection which auxiliary hypotheses to use (e.g. for na_own); more tests.
• be6a0f28 - Move iInv into generic proofmode directory; documentation. Move namespaces to bi/lib/

Compare with previous version

unmarked as a Work In Progress

changed the description

resolved all discussions

I removed the "WIP" because as far as I'm concerned it seems to work and covers the intended use cases. However, I'm sure there are still things that are unclear and there may be ways to make the Ltac more robust, so let me know what you think, particularly @robbertkrebbers.

It handles the usage of "cinv_open" in the spanning tree from iris-examples. I'm not sure what else is up to date enough with gen_proofmode to test against.