I'm not able to find such lemma. So, the question, do I miss something or there is no such lemma yet?
So, I need to proof lemmas as next
Lemma mem_head' (T : eqType) (x a : T) s : x \in s -> x \in (a :: s). Admitted. Lemma mem_cat_fst (T : eqType) (x : T) s' : forall s, x \in s -> x \in (s ++ s'). Admitted. Lemma mem_cat_snd (T : eqType) (x : T) s : forall s', x \in s -> x \in (s ++ s'). Admitted.
Hi @Andrey Klaus , indeed there should be such a lemma, one sec
So to prove that you use a bit different proof style
by move=> x_in_s; rewrite mem_cat x_in_s.
Hello, Emilio! Thank you very much! Especially for the proof style hint.
The reason this style is preferred is that math-comp defaults to rewriting lemmas (as they tend to work a bit more generally) when an equational theory exists
Note how mem_cat goes in both directions, so it is a bit more "general"
Note also that
in_cons is usually a part of the
inE rewriting db
it is a good idea to extend inE (locally) for your own needs, but beware of performance
You are most welcome
One point of using equations is that they work the same, no matter whether you're rewriting in an assumption or in the conclusion. Also, they often allow proving additional equalities without making any case analysis, as seen by the following (contrived) example:
Goal forall (T: eqType) (s : seq T) x, (x \in s ++ s) = (x \in s). Proof. by move=> T s x; rewrite mem_cat orbb. Qed.
Note that there is no need to make this a lemma, because one can simulate rewriting with this lemmas by rewriting with
orbb. So another benefit is that one needs fewer lemmas.
@Christian Doczkal , thank you very much for the explanation. I can see now why there is no such lemmas.
Andrey Klaus has marked this topic as resolved.
Last updated: Jan 29 2023 at 19:02 UTC