Stream: math-comp users

Topic: using finmap


view this post on Zulip Christian Doczkal (Aug 24 2020 at 09:54):

I'm trying to port some of my code (that uses a precursor of finmap) to the finmap library. Here are two things I stumbled upon:

  1. At some places I use the fact that [fset x] = [:: x] :> seq _. I can prove this using fset_uniq and the following lemma:
Lemma uniq_pred1_seq1 (T : eqType) (s : seq T) (x : T) :
  uniq s -> s =i pred1 x -> s = [:: x].

which, somewhat surprisingly, I didn't find in mathcomp. Is there a more direct proof?

  1. My old library had limited support for boolean quantification over the elements of a finite set, which was basically just a nice notation for seq.all and a few lemmas (for explicit shapes of the quantification domain):
Notation "[ 'all' x 'in' s , p ]" := (all (fun x => p) s).
Notation "[ 'some' x 'in' s , p ]" := (has (fun x => p) s)

Could something like this be a useful addition? I know that I one can also use [forall x : A, P (val x)], with A : {finset T}, but then that introduces an unnecessary val, and the display hides the _ : A, making the goals hard to understand.

view this post on Zulip Cyril Cohen (Aug 24 2020 at 19:36):

Hi @Christian Doczkal

Lemma test (T : choiceType) (a : T) (P : pred T) : P a -> all P [fset a].
Proof. by move=> Pa; rewrite enum_fsetE enum_fset1/= Pa. Qed.

Here is a test that combine both problems you encountered. For 1. maybe enum_fset1 should be named enum_fset1type and the composition of enum_fsetE and enum_fset1type should be called enum_fset1 though... As for 2. as you can see you can use directly all and has since there is a coercion from {fset T} to seq T... :smiley_cat:

view this post on Zulip Christian Doczkal (Aug 25 2020 at 10:16):

Cyril Cohen said:

As for 2. as you can see you can use directly all and has since there is a coercion from {fset T} to seq T... :smiley_cat:

I'm (of course) aware of that, I would just prefer to have notations that avoid explicit fun _ => _ expressions and restore the usual order of quantification and add some lemmas on the interaction of all/has with domains of the form A op B where op is some fset-operation.

view this post on Zulip Reynald Affeldt (Sep 02 2020 at 10:26):

about using finmap: there is not operator to take the preimage of a fset, isn't there?

view this post on Zulip Cyril Cohen (Sep 02 2020 at 10:37):

affeldt-aist said:

about using finmap: there is not operator to take the preimage of a fset, isn't there?

Such an operation does not exist in general... so nop...


Last updated: Feb 08 2023 at 07:02 UTC