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