Stream: math-comp users

Topic: ✔ how to prove x \in s -> x \in s++s' ?

Andrey Klaus (Nov 12 2021 at 16:29):

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.

Emilio Jesús Gallego Arias (Nov 12 2021 at 16:30):

Hi @Andrey Klaus , indeed there should be such a lemma, one sec

Emilio Jesús Gallego Arias (Nov 12 2021 at 16:32):

You have in_cons and mem_cat

Emilio Jesús Gallego Arias (Nov 12 2021 at 16:33):

So to prove that you use a bit different proof style

Emilio Jesús Gallego Arias (Nov 12 2021 at 16:33):

by move=> x_in_s; rewrite mem_cat x_in_s.

Andrey Klaus (Nov 12 2021 at 16:41):

Hello, Emilio! Thank you very much! Especially for the proof style hint.

Emilio Jesús Gallego Arias (Nov 12 2021 at 16:41):

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

Emilio Jesús Gallego Arias (Nov 12 2021 at 16:41):

Note how mem_cat goes in both directions, so it is a bit more "general"

Emilio Jesús Gallego Arias (Nov 12 2021 at 16:41):

Note also that in_cons is usually a part of the inE rewriting db

Emilio Jesús Gallego Arias (Nov 12 2021 at 16:42):

it is a good idea to extend inE (locally) for your own needs, but beware of performance

Emilio Jesús Gallego Arias (Nov 12 2021 at 16:42):

You are most welcome

Christian Doczkal (Nov 12 2021 at 18:04):

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 mem_cat and orbb. So another benefit is that one needs fewer lemmas.

Andrey Klaus (Nov 13 2021 at 07:38):

@Christian Doczkal , thank you very much for the explanation. I can see now why there is no such lemmas.

Notification Bot (Nov 13 2021 at 23:18):

Andrey Klaus has marked this topic as resolved.

Last updated: Jan 29 2023 at 19:02 UTC