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

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`

?

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

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

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`

.

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.

But I had some doubts about refinements.

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