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?

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')).
```

- Did I miss
`incl`

in mathcomp?/What people use usually for incl? - Any other hints are very welcome.

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

)

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.

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.

As for `incl`

, perhaps you are looking for `subseq`

? Look for it here.

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.

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.

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.

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

@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.

Andrey Klaus has marked this topic as resolved.

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.

@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