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).