Make iSplit work below existentials?
I have a goal of the form
∃ x : vec val m, ⌜#l = #l⌝ ∗ ▷ l ↦∗ x
and all my assumptions are only available later. I cannot do iNext
because not everything is below a later, but I can do rewrite -uPred.sep_exist_l. iSplit; first done.
. This works because some part of what is below the existential does not depend on the witness.
Now I wonder, would it make sense for iSplit
to work in this case (giving me ⌜#l = #l⌝
and ∃ x : vec val m, ▷ l ↦∗ x
as goals)? The rewrite I did above is not very discoverable, but neither is the iSplit
. What do you think? @jjourdan @robbertkrebbers
(You may wonder why I have things under the existential that do not depend on the witness. The reason is that lemmas of the form ∃ x y z, P
work much better with the proofmode, because I an do a single iDestruct ... as (x y z) ...
. If I pushed the existential down, destructing things would become much more annoying.)