Use Ltac2 to avoid unrolling tactic notations with lists.

As requested yesterday (during an Ltac2 breakout session at the 3rd iris workshop) I removed all unrolled tactic notations in ltac_tactics.v by using Ltac2/Ltac1 FFI which allows us to iterate over Ltac1 lists.

I had to introduce some auxiliary tactics in places where notation was re-used previously. This no longer works because iIntros (xs) is not expanded to iIntros (x1 .. xN). So every tactic notation that gets re-used in notation further down in the file needs to have an equivalent Ltac tactic that can be called explicitly with all the arguments, especially lists such as xs.

I have no interest in bikeshedding the exact names, locations, indentations, the code factoring, or anything like that. I would very much appreciate somebody taking over these parts. I will gladly answer questions about and help with anything Ltac2-related, of course.

Apart from bikeshedding issues there is really just one question remaining: which lists should be marked non-empty. I saw that iClear for example does not demand an item in the list of coq idents so I wasn't sure if I should follow that example or not. For now I only marked the iExists argument with the ne_ prefix because that tactic definitely didn't accept an empty list before.

/cc @robbertkrebbers

This is amazing @janno! I did a quick pass and the changes look reasonable to me.

This looks great indeed! Some comments:

• Regarding iDestructHyp_intros_hd_, the old iInv code has been written by @jung as part of !143 (merged) I hope he can explain what comment to add.
• Regarding thunking in iRevertIntros. It's a bit weird that we have idtac; in some cases now, and in others not. I would be more in favor of making the argument of iRevertIntros an actual function, so that it is always thunked.
• What would be a suitable place to put utilities such as with_ltac1_list?

mentioned in merge request !935 (merged)

Apart from bikeshedding issues there is really just one question remaining: which lists should be marked non-empty. I saw that iClear for example does not demand an item in the list of coq idents so I wasn't sure if I should follow that example or not. For now I only marked the iExists argument with the ne_ prefix because that tactic definitely didn't accept an empty list before.

I think for all cases where we have a list of intro patterns in parentheses, we do not want to accept the empty list. If we accepted the empty list there would be 2 different ways of writing the same thing (iDestruct "H" as () "pat" and iDestruct "H" as "pat") and I can't see an upside to that.

mentioned in merge request !937 (merged)

mentioned in issue #523