Remove `CopyDestruct` heuristic

The CI showed that !591 (merged) caused a lot of breakage in the reverse dependencies.

While debugging this breakage, I noticed that the heuristic in iDestruct (H ...) as .. which decides when to remove/keep the original hypothesis H was broken. I implemented this heuristic several years ago, but as !591 (merged) showed, the implementation was buggy and hence it was never actually triggered.

The problem

Similar to Coq's destruct, the tactic iDestruct (H ...) as .. removes the original hypothesis H if there is no information loss caused by the destruct. For example:

• If H : P ∨ Q, then H can be removed without information loss after eliminating the disjunction. The results P and Q are strictly stronger than P ∨ Q.
• If H : ∀ x, P x, then H cannot be removed without information loss after eliminating the universal quantifier. After all, we might want to use H with a different value for x.

Note that in separation logic these considerations only apply if H is in the intuitionistic context, if H is in the spatial context, we cannot keep H either way.

The old heuristic

The old heuristic, which was wrongly implemented and thus never triggered, looked at the type of H in iDestruct (H ...) as ... If the type contains a universal quantifier, it would keep H, otherwise it would remove H. As the breakage of !591 (merged) showed, this heuristic had several problems:

• The hypothesis H might have type P -∗ Q and we might instantiate H with HP : P from the spatial context, i.e., iDestruct ("H" with "HP") as "HQ". The old heuristic would remove H, which would lead to information loss because HQ ends up in the spatial context, while we might want to use H another time.
• The hypothesis H might have type P ↔ Q and we might instantiate H with HP : P, i.e., iDestruct ("H" with "HP") as "HQ". The old heuristic would remove H, which would lead to information loss, because we might also want to use the other direction of the bi-implication.

The new heuristic

The new heuristic is much simpler, it will only remove H when iDestruct "H" as .. does not eliminate any universal quantifiers or wands/implications. This is simply detected by checking whether H is an identifier or a proof mode term (i.e., if it contains $! or with).

Backwards compatibility

The new heuristic is backwards compatible. It has the same behavior as we had prior to !589 (merged), but it removes a bunch of dead code, restructures some control flow, documents the current behavior, and adds some tests.

Todo

We should update the proof mode documentation. I have not done that yet to avoid conflicts with !589 (merged).

Credit

The tests are adapted from @tchajed's !591 (merged).