## Stream: math-comp users

### Topic: Set to list conversion

#### Julin Shaji (Apr 02 2024 at 04:53):

Is it possible to refine a set to a plain list without all the
mathcomp stuff showing up in the list definition?

Like a way have the following conversions:

• `{set true; false; true}: {set bool}` to `[:: true; false]: seq bool`.
• `{set false}` to `[:: false]`
• `set0: {set bool}` to `[::]`

#### Cyril Cohen (Apr 03 2024 at 15:14):

I'm not sure what do you mean by refine..
Do you want automated proofs that `S = [set x | x in s]` for concrete `S` and `s`?

#### Cyril Cohen (Apr 03 2024 at 15:19):

My intuition is that the feature you are looking for is probably adequate as a feature request for CoqEAL/refinements or Trocq

#### Emilio Jesús Gallego Arias (Apr 03 2024 at 19:03):

@Julin Shaji typical proof would go like this:

``````From mathcomp Require Import all_ssreflect.

Definition a : {set bool} := [set true; false].

Lemma enum_setU (T: finType) (A B : {set T}) x :
x \in enum (A :|: B) = (x \in enum A) || (x \in enum B).
Proof. (* todo *) Qed.

Lemma foo : perm_eq (enum a) [:: true; false].
Proof.
by rewrite /a uniq_perm ?enum_uniq // => x; rewrite enum_setU !enum_set1 !inE.
Qed.
``````

so indeed you may need some lemmas on the internals of set, like the one above. Cyril's suggestion to use a refinement infra makes sense too (but I guess you'd have to setup your lemmas right)

#### Emilio Jesús Gallego Arias (Apr 03 2024 at 19:04):

IIRC `enum A` where `A` is a set of type `T` is just `filter A (enum T)` , where A is the membership fn `A : T -> bool`.

#### Julin Shaji (Apr 19 2024 at 17:05):

Cyril Cohen said:

My intuition is that the feature you are looking for is probably adequate as a feature request for CoqEAL/refinements or Trocq

Yeah, something like coqeal is what I was thinking.

#### Julin Shaji (Apr 19 2024 at 17:07):

Emilio Jesús Gallego Arias said:

Julin Shaji typical proof would go like this:

``````From mathcomp Require Import all_ssreflect.

Definition a : {set bool} := [set true; false].

Lemma enum_setU (T: finType) (A B : {set T}) x :
x \in enum (A :|: B) = (x \in enum A) || (x \in enum B).
Proof. (* todo *) Qed.

Lemma foo : perm_eq (enum a) [:: true; false].
Proof.
by rewrite /a uniq_perm ?enum_uniq // => x; rewrite enum_setU !enum_set1 !inE.
Qed.
``````

so indeed you may need some lemmas on the internals of set, like the one above. Cyril's suggestion to use a refinement infra makes sense too (but I guess you'd have to setup your lemmas right)

Yeah, but I guess for non-specific values, an approach like that of coqeal would be better..
I'm now trying to get familiar with it.

Last updated: Jul 25 2024 at 15:02 UTC