## Stream: math-comp users

### Topic: ✔ how to work with all (fun x => has (pred1 x) s1) s2

#### Andrey Klaus (Nov 13 2021 at 16:53):

Hello everybody.
I have next lemma

``````Goal forall (T : eqType) (s1 s2 s3: seq T), all (fun x => has (pred1 x) (s1++s2) s3.
``````

I would like to do something like this:

``````rewrite has_pred1 mem_cat.
``````

but I'm not able because of `fun x => ...`.
Could somebody give any hints how to work with this kind of things?

#### Andrey Klaus (Nov 13 2021 at 16:56):

Well, it may be I'm a bit wrong with my definitions..
I would like to prove next thing.

``````Definition incl (T : eqType) (vrs' vrs : seq T) := all (fun x => has (pred1 x) vrs) vrs'.

Lemma undup_cat_incl (T : eqType) :
forall (vrs vrs' : seq T),
incl vrs (undup (vrs ++ vrs')) && incl vrs' (undup (vrs ++ vrs')).
``````
1. Did I miss `incl` in mathcomp?/What people use usually for incl?
2. Any other hints are very welcome.

#### Paolo Giarrusso (Nov 13 2021 at 19:27):

For rewriting under binders (fun x => ...), plain Coq has setoid_rewrite, while ssreflect uses another tactic (`over`)

#### Paolo Giarrusso (Nov 13 2021 at 19:29):

But this is just about point 1; the Coq manual should have details and might be helpful. Else math-comp experts can probably be more specific.

#### Ana de Almeida Borges (Nov 13 2021 at 19:30):

Also helpful if you're going to use `all` and `has` are the `allP` and `hasP` lemmas. Transforming `all` with `allP` is almost always the first thing I do when I see an `all` cropping up in a proof. If you do `apply/allP => t` on your goal, it allows you to rewrite as you desire.

#### Ana de Almeida Borges (Nov 13 2021 at 19:33):

As for `incl`, perhaps you are looking for `subseq`? Look for it here.

#### Ana de Almeida Borges (Nov 13 2021 at 19:35):

Hmmm, I think `subseq` cares about ordering and `incl` doesn't, so it's not the same unless you chain it with `perm_eq` or something. Edit: Not even that, since `perm_eq` still cares about duplicates and `incl` doesn't.

#### Ana de Almeida Borges (Nov 13 2021 at 19:37):

Anyway, your use of `incl` and `undup` leads be to think you may be using `seq` to implement sets, and in that case I would recommend using a set library, not a list library.

#### Ana de Almeida Borges (Nov 13 2021 at 19:44):

As far as I know, there are two finite set libraries in mathcomp: finset for when the elements have a `finType` structure, and finmap for when you can only assume `choiceType`. Se also this thread.

#### Andrey Klaus (Nov 13 2021 at 23:14):

@Paolo Giarrusso , thank you, especially for mentioning setoid_rewrite and the over tactic, I didn't know what is it.

#### Andrey Klaus (Nov 13 2021 at 23:17):

@Ana de Almeida Borges , thank you for the pointing me to `allP => t`, it works just great. As for your notice that I may reinvent the set, you are most likely right and I thought about this too, but for now I still would like to try finish my proof as it is.

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

Andrey Klaus has marked this topic as resolved.

#### Christian Doczkal (Nov 14 2021 at 09:19):

Andrey Klaus said:

As for your notice that I may reinvent the set, you are most likely right and I thought about this too, but for now I still would like to try finish my proof as it is.

Depending on what you are doing exactly, this may actually be the right thing to do. Using the `{set T}` type requires that `T` is a finite type. Of course, there is also `finmap`, which provides finite sets over types with a choice operator.

For what it's worth, the boolean version of `incl s1 s2` is just `all (mem s2) s1` and the propositional version is written `{subset s1 <= s2}`. Note that while `seq T` is a `predType` whenever `T` is an eqType, using `_ \subset _` requires that `T` is a finite type.

#### Andrey Klaus (Nov 14 2021 at 17:15):

@Christian Doczkal, thank you for the comment especially for the `all (mem s2) s1`. It looks like `mem` is what I've missed. As for other parts of your comments, I have to say I was a bit confused with fintype and choice type so, I'm not sure I'm on the most optimal way. But I prefer finish it as is anyway. Thanks again for the notice.

Last updated: Jul 25 2024 at 15:02 UTC