Better handling of persistent results in `iDestruct`, `iPoseProof`, `iAssert` and friends

This MR improves the behavior of iSpecialize, iDestruct .. as #.., iPoseProof .. as #.., and iAssert .. as #.. on hypotheses whose conclusion is persistent. The most notable end-user improvements to tactics are as follows:

1. When using iSpecialize (H with "[pat]"), the hypothesis H will remain in the intuitionistic context if the pattern pat does not consume any spatial hypotheses. For example, before this MR, iSpecialize (H with "[]") used to move H to the spatial context.
2. When using iDestruct (H with "pats") as #pat, the tactic will succeed even if the conclusion of R is not persistent, but as long as H is in the intuitionistic context and pats does not consume any spatial hypotheses. For example, when having H : P -∗ Q in the intuitionistic context, before this MR, iDestruct (H with "[]") as #H used to fail; now it succeeds.
3. When using iAssert P with "[pat]" as #pat, the tactic will succeed even if P is not persistent, but as long as pat does not consume any spatial hypotheses. See below for an example.

Improvement (1) is a consequence of a stronger implementation of tac_specialize_assert. Improvements (2) and (3) are a consequence of a better procedure to decide when to use tac_specialize_intuitionistic_helper or not. I have implemented the core part of this procedure in Gallina instead of through Ltac hackery, and tried to document the way it works in the code.

Documentation

As shown in the documentation of the code, the exact way when iSpecialize .. as # fails or falls back on the behavior of not copying the context is rather intricate. We could document this in docs/proof_mode.md, but I'm not sure I want to do that. The tactic iSpecialize .. as # is used mostly as a helper to implement iDestruct .. as #.., iPoseProof .. as #.., and iAssert .. as #... As such, I would like to keep the freedom of modifying iSpecialize .. as # to improve the tactics we actually care about.

Maybe it's better to make clear in the documentation that the exact behavior of iSpecialize .. as # is thus underspecified?

Relation to issue #186

This MR makes the following version of the example in #186 work:

Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
  □ P -∗ □ |==> P.
Proof.
  iIntros "#HP".
  (* Test that [HPupd1] ends up in the intuitionistic context *)
  iAssert (|==> P)%I with "[]" as "#HPupd1"; first done.
  (* This should not work, [|==> P] is not persistent. *)
  Fail iAssert (|==> P)%I with "[#]" as "#HPupd2"; first done.
  done.
Qed.

Relation to MR !216 (closed)

MR !216 (closed) changes the behavior of [#] to produce a goal with a persistence modality in case the premise is not persistent. On its own, MR !216 (closed) does not fix either of the iAssert examples above, but in combination with this MR, I think we can also make the following to work:

Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
  □ P -∗ □ |==> P.
Proof.
  iIntros "#HP".
  iAssert (|==> P)%I with "[#]" as "#HPupd2".
  { (* Gives the goal `<pers> |==> P` *) done. }
  done.
Qed.

CC @dfrumin