Stream: math-comp users

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


view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:30):

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:32):

You have in_cons and mem_cat

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:33):

So to prove that you use a bit different proof style

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:33):

by move=> x_in_s; rewrite mem_cat x_in_s.

view this post on Zulip Andrey Klaus (Nov 12 2021 at 16:41):

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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2021 at 16:42):

You are most welcome

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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