refactor: Hyps optimisations (experiment)

[alvinylt]

Description

There are many ways to potentially optimise the Iris Proof Mode, especially regarding how the spatial and intuitionistic contexts are organised using Hyps in ProofMode/Expr.lean. To name a few:

• The functions Hyps.spatialIVarIds and Hyps.intuitionisticIVarIds use list concatenation (++): quadratic complexity due to repeated copying of lists. This can easily be optimised using an accumulator (commit 24db6ec).
• The function Hyps.add does not perform balancing. It will be interesting to see whether having a balanced tree enables notable optimisations. Otherwise, we might instead simply have two separate lists (as in Rocq), one for spatial hypotheses and another for intuitionistic hypotheses. This would avoid complications (e.g. in Hyps.buildAccuProof) such as having multiple trees representing the same context (with the same order of hypotheses).
• Possibly some data structures for more efficient lookup of hypotheses (e.g. using Hyps.select) instead of repeated isDefEq.
• Prevent hypotheses from shuffling around when IPM tactics are used.

It will also be helpful to think through how the optimisations can be evaluated.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[alvinylt]

!bench

[leanprover-radar]

Benchmark results for 790a068 against 4d8eee8 are in. No significant results found. @alvinylt

• 🟥 build//instructions: +3.7G (+0.22%)

Small changes (1🟥)

• 🟥 build/module/Iris.ProofMode.Expr//instructions: +1.7G (+12.24%)