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:
[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?
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
andhas
since there is a coercion from{fset T}
toseq 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: Mar 28 2024 at 16:02 UTC