GitLab

Together with @jung and @jjourdan we discussed that it would be useful if iDestruct (and tactics like iSplit and iFrame) would have better support for big ops, in particular, that when having:

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