## Stream: math-comp users

### Topic: using finmap

#### 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.

#### 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:

#### 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.

#### 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?

#### 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: Jul 25 2024 at 16:02 UTC