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.

`imset`

?

I guess it's `imset2`

that I can use?

How can one use it?

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)
*)
```

Or is it `imset`

itself that's useful here?

With `imset`

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

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]`

.

Oh.. Thanks!

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`

.

Julin Shaji has marked this topic as resolved.

Another doubt:

Given a value of type `{set {set A*B}}`

, how can one get a value of type `{set {set A}}`

?

Julin Shaji has marked this topic as unresolved.

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

?

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`

.

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])
```

Only now do I realize why Quentin mentioned the `[set E | x in A]`

notation earlier.. :sweat_smile:

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?

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

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.

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

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

bad?

`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