Julin Shaji (Apr 02 2024 at 04:53): 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.
But I had some doubts about refinements.
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: Oct 13 2024 at 01:02 UTC