`iDestruct` for big ops
H : [∗ list] k ↦ x ∈ y :: l, Φ k x
we could use
iDestruct "H" as "[H1 H2]" to turn it into:
H1 : Φ 0 y H2 : [∗ list] k ↦ x ∈ l, Φ (S k) x
Although this is not particularly difficult to implement (it just requires one to declare suitable
IntoAnd instances), it gives rise to some potential ambiguity, namely, what is going to happen when having:
H : [∗ list] k ↦ x ∈ y :: l, Φ k x ∗ Ψ k x
Will it split through the cons, or through the star inside of the predicate in the big op?
Currently, it will split through the ∗ due to the instance
into_and_big_sepL. Declaring yet another
IntoAnd instance for the
cons case is a bad idea, as it will give rise to the ambiguity above, and we end up with tactics that will behave unpredictably.
However, I think that the
cons instance would be much more useful than the
∗ instance, hence I propose to drop the current
∗ instance, and instead declare instances for
cons (and possibly
app, which does not lead to ambiguity).