This is not a major optimization, but it seems to be an optimization nonetheless, so I thought I'd submit it to at least get some measurements from existing iris projects. From a quick benchmark, on our project we get a ~7-8% speedup (but I expect the speedup to be lower in most cases).
The idea is to avoid unnecessary calls to iRename. Currently, when doing
iDestruct "H" as "[H1 H2]", iDestruct will produce two hypotheses, generating a fresh name for the first one and reusing "H" for the second one, then will call itself recursively, renaming each hypothesis into "H1"/"H2".
These final calls to iRename are superfluous, because we could have chosen the right names directly, and those iRenames can add up to 25-30% of the time taken by iDestruct (it's the
eapply of the renaming lemma that takes time, I guess just because of unification).
The first commit of the PR optimizes the split case of iDestruct (
as "[H1 H2]"), as this is what I expect to be the most common use of
iDestruct. The second commit optimizes the IIntuitionistic/ISpatial/IModalElim cases; the change is slightly more intrusive, as it requires generalizing the corresponding lemmas to include a renaming step.
I ran a couple synthetic microbenchmarks to confirm that this is actually achieving something.
idestruct_bench.v: before: Benchmark #1: coqc idestruct_bench.v Time (mean ± σ): 6.105 s ± 0.092 s [User: 5.837 s, System: 0.238 s] Range (min … max): 5.920 s … 6.272 s 10 runs after: Benchmark #1: coqc idestruct_bench.v Time (mean ± σ): 4.370 s ± 0.071 s [User: 4.135 s, System: 0.216 s] Range (min … max): 4.271 s … 4.522 s 10 runs idestruct_bench_2.v: before: Benchmark #1: coqc idestruct_bench_2.v Time (mean ± σ): 6.228 s ± 0.240 s [User: 5.973 s, System: 0.235 s] Range (min … max): 5.638 s … 6.475 s 15 runs after: Benchmark #1: coqc idestruct_bench_2.v Time (mean ± σ): 4.644 s ± 0.442 s [User: 4.420 s, System: 0.208 s] Range (min … max): 4.057 s … 5.202 s 15 runs
The measurements are kind of noisy, I suspect because part of the time is spent just doing I/O to load the iris theories; but nevertheless demonstrate that there is indeed a speedup +/- corresponding to the 25% of the time spent in iRename that I could measure before.