Add [iSelect], and various tactics based on it

This MR adds the following tactics:

• iSelect (pat)%I tac calls the tactic tac with the name of the last hypothesis of the Iris context matching pat,
• iRename select (pat)%I into name renames the last hypothesis of the Iris context matching pat into name,
• iDestruct select (pat)%I as ... is similar to iDestruct but it acts on the last hypothesis of the Iris context matching pat,
• iClear select (pat)%I clears the last hypothesis of the Iris context matching pat,
• iRevert select (pat)%I reverts the last hypothesis of the Iris context matching pat,
• iFrame select (pat)%I cancels the last hypothesis of the Iris context matching pat.

changed the description

added 1 commit

• 866559f4 - Add doc for [iRename select] and [iDestruct select].

Compare with previous version

This MR looks very useful!

In the future, we might want to have more select tactics. For which other tactics would this be useful?

added 1 commit

• 5a498150 - Simplification of [iSelect] + extra tests.

Compare with previous version

added 1 commit

• f8732094 - Tweak docs of [iRename select] and [iDestruct select].

Compare with previous version

added 1 commit

• 36aedc11 - Add [(...)%I] around the first argument of [iAssert] in doc.

Compare with previous version

resolved all threads

added 1 commit

• 9208c0ac - Fix typo in doc.

Compare with previous version

resolved all threads

What's the intended backtracking behavior for iSelect?

@lepigre could you add a test for iSelect where the pattern matches multiple hypotheses and one where it fails? If you do want to exploit backtracking something like iDestruct select _ as "#H" which will only work on the last persistent hypothesis would be a cool test.

added 1 commit

• 54eb2d1c - Tweak the backtracking behaviour to match stdpp.

Compare with previous version

resolved all threads

added 1 commit

• 3bdf8aac - Add [iClear select], [iRevert select] and [iFrame select].

Compare with previous version

resolved all threads