Stream: math-comp users

Topic: Map a set


view this post on Zulip Julin Shaji (Mar 19 2024 at 14:15):

I have a value of type {set A*B}. How can I convert it to a value of type {set A}?

Is there a map function?

I tried Search (set_of _ -> set_of _).
Found setX which can be used to go the other way, but not for what I needed.

view this post on Zulip Kazuhiko Sakaguchi (Mar 19 2024 at 14:59):

imset ?

view this post on Zulip Julin Shaji (Mar 19 2024 at 15:56):

I guess it's imset2 that I can use?

view this post on Zulip Julin Shaji (Mar 19 2024 at 15:57):

How can one use it?

view this post on Zulip Julin Shaji (Mar 19 2024 at 15:57):

I tried:

From mathcomp Require Import all_ssreflect.

Example eg1 := [set true; false].
Example eg2 := [set tt; tt].
Check imset2 (fun x y => (x,y)) (mem eg1).
(*
imset2 (aT1:=Datatypes_bool__canonical__fintype_Finite)
  (rT:=Datatypes_prod__canonical__fintype_Finite
         Datatypes_bool__canonical__fintype_Finite
         ?t)
  (fun x : Datatypes_bool__canonical__fintype_Finite => [eta pair x])
  (mem eg1)
     : (Datatypes_bool__canonical__fintype_Finite -> mem_pred ?t) ->
       {set Datatypes_prod__canonical__fintype_Finite
              Datatypes_bool__canonical__fintype_Finite
              ?t}
where
?t : [x : Datatypes_bool__canonical__fintype_Finite  y : ?t |- finType] (x,
     y cannot be used)
*)

view this post on Zulip Julin Shaji (Mar 19 2024 at 15:59):

Or is it imset itself that's useful here?

view this post on Zulip Julin Shaji (Mar 19 2024 at 16:32):

With imset, I coudln't figure out how to accept two sets.

view this post on Zulip Quentin VERMANDE (Mar 19 2024 at 19:56):

You only have one set, so you really need imset, to which you will give your set as the argument of type mem_pred aT. It is very hard to find with Search, unless you know what to look for. You can find it in the documentation header of finset.v (https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/finset.v). Note also that there are notations for this, namely f @: A and [set E | x in A].

view this post on Zulip Julin Shaji (Mar 20 2024 at 04:34):

Oh.. Thanks!

view this post on Zulip Julin Shaji (Mar 20 2024 at 04:35):

Sorry, just realized I had given the example wrong..

It should've been like:

Example eg3 := [set (true,tt); (false, tt)].

Got it with snd @: eg3.

view this post on Zulip Notification Bot (Mar 20 2024 at 04:53):

Julin Shaji has marked this topic as resolved.

view this post on Zulip Julin Shaji (Mar 20 2024 at 05:57):

Another doubt:

Given a value of type {set {set A*B}}, how can one get a value of type {set {set A}}?

view this post on Zulip Notification Bot (Mar 20 2024 at 05:57):

Julin Shaji has marked this topic as unresolved.

view this post on Zulip Julin Shaji (Mar 20 2024 at 05:57):

Could it be something like: (fun x => fst @: x) @: s ?

view this post on Zulip Julin Shaji (Mar 20 2024 at 05:59):

As in, we take elements of s: {set {set A*B}, each of which is a value of type {set A*B} and then apply fst via imset.

view this post on Zulip Julin Shaji (Mar 20 2024 at 07:36):

Okay, I think I got it. Went into proof mode to get this:

(fun (T1 T2 : finType) (H : {set {set T1 * T2}}) =>
 [set [set x.1 | x in t1t2] | t1t2 in H])

view this post on Zulip Julin Shaji (Mar 20 2024 at 07:37):

Only now do I realize why Quentin mentioned the [set E | x in A] notation earlier.. :sweat_smile:

view this post on Zulip Julin Shaji (Mar 21 2024 at 04:54):

Goals involving sets are showing up like finset_set_of__canonical__fintype_Finite T) instead of just {set T}.

Is there a way to change to show as {set T} itself?

view this post on Zulip Quentin VERMANDE (Mar 21 2024 at 08:04):

Not that I know of (unless you brutally assert the equality). Still, this is not normal, can you give an example?

view this post on Zulip Julin Shaji (Mar 27 2024 at 06:50):

Quentin VERMANDE said:

Not that I know of (unless you brutally assert the equality). Still, this is not normal, can you give an example?

Like this:

From mathcomp Require Import all_ssreflect.

Check [set: bool].
(* [set: bool] : {set Datatypes_bool__canonical__fintype_Finite} *)

Check [set true; false].
(* [set true; false] : {set Datatypes_bool__canonical__fintype_Finite} *)

Sorry for the late reply. I hadn't gone to find a small enough example earlier.

view this post on Zulip Julin Shaji (Mar 27 2024 at 06:57):


Speaking of equality, what could be a good way to see if two sets are equivalent?

view this post on Zulip Julin Shaji (Mar 27 2024 at 08:07):

Or a way to see if a set is empty? Is doing s == set0 bad?

view this post on Zulip Quentin VERMANDE (Mar 27 2024 at 09:17):

A == B and A = B are both correct ways to assert that two sets A and B are equal (in particular with B = set0 to assert that A is empty). The right one depends on the context (i.e. whether you want a boolean or a proposition).


Last updated: Jul 25 2024 at 15:02 UTC