Stream: math-comp users

Topic: split on membership in list


view this post on Zulip Yves Bertot (Apr 01 2022 at 15:04):

When x is an element of sequence s, I sometimes need to split s along what case/splitPr does. But I find this idiom hard to use, because if does not have case_eq-like behavior that is easy to operate. I find it more convenient to have the following lemma, which I added to my own development.

Lemma mem_seq_split (T : eqType) (x : T) (s : seq T) :
  x \in s -> exists s1 s2, s = s1 ++ x :: s2.
Proof.
by move=> /splitPr [s1 s2]; exists s1, s2.
Qed.

Here are my question:


Last updated: Feb 08 2023 at 04:04 UTC