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:
do you feel that this lemma is worth adding to math-comp?
Users only need to know the "behavior" of existential and equality statements to make progress with this.
is the naming right?
many lemmas about membership in lists already have the mem
radical, but mem
is not restricted to sequences, this is why I added the seq
radical, but I am really unsure. I hope the split
part is really meaningful but I am open to suggestions.
where should this lemma be stored?
I think I would add it in seq.v, next to mem_cat and the like.
Last updated: Feb 08 2023 at 04:04 UTC