Zulip Chat Archive

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

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

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):

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):

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

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.

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):