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:

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

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

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:

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.

about `using finmap`

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

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