strengthen uPred_mono

See merge request iris/iris!513

More general instance for framing under `<affine>`

See merge request iris/iris!522

Make `iFrame` "less" smart w.r.t. clean up of modalities.

See merge request iris/iris!521

various algebra lemmas

See merge request iris/iris!523

Previously, if would "cleanup" `<affine>` and `□` if the result after framing
is affine and intuitionistic, respectively. This behavior was inconsistent,
since similar "cleanup" was not performed for `<absorbing>` and `<persistent>`.
This MR thus removes this "cleanup" of modalities. It now consistently removes
the modalities `<affine>`, `<absorbing>, `<persistent>` and `□` only if the
result after framing is `True` or `emp`.

Since `iFrame` is already very complicated, and since its performance is
sometimes suboptimal in bigger developments, @jung and I believed doing
fewer "smart" things is better than the alternative, namely performing doing
sophisticated "cleanup" for all modalities, which is presented in
iris/iris!450

document Iris side-effects

Closes #311

See merge request iris/iris!524

Strengthen auth_both_valid and auth_both_frac_valid

See merge request iris/iris!520

Improve docs for `iModIntro`.

See merge request iris/iris!519

Based om iris/iris!467 (comment 53064)
by @Blaisorblade.

Fix typos

See merge request iris/iris!518

Improve some iIntros error messages

See merge request iris/iris!517

A failing iIntros for implications should prettify the identifier before
printing, and iIntros on something that isn't a wand or implication
should say what couldn't be introduced (to clarify that `iIntros "HP
HQ"` failed because of the HQ in particular, for example).

ghost-var lib: more lemmas for when you own the two halves

See merge request iris/iris!511

Fix direction of `auth_auth_validN`

See merge request iris/iris!515

For example, `auth_auth_valid`.

Fix error when destructing as multiple pats

See merge request iris/iris!512

`iDestruct H as "H1 H2"` produces an error that says the pattern should
contain exactly one proper introduction pattern. When multiple patterns
are provided, due to Ltac variable shadowing iDestructHypFindPat was
instead reporting only the first pattern in the error message (and even
that was printed as the parsed AST rather than the original string).

Report an error when iIntro fails to find a forall

See merge request iris/iris!510

The error handling for `iIntro (?)` and similar tactics didn't correctly
report failures when the goal couldn't be turned into a universal
quantifier. This is something missing from !482 due to no test
triggering the error.

use sep. conjunction instead of conjunction for allocation lemmas

See merge request iris/iris!508