Stream: math-comp users

Topic: Set to list conversion


view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

But I had some doubts about refinements.

view this post on Zulip 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