There are some results in the
ssreflect.bigop library specific to
finType, such as
leq_bigmax : forall (I : finType) (F : I -> nat) (i0 : I), F i0 <= \max_i F i
I would like to use such results when the range of
\bigop is different, for example when my goal is
x \in w -> F x <= \max_(y <- w) F y
What is the recommended way of doing this?
EDIT: added the
x \in w assumption to the goal
Hi, would you mind clarifying the type of
w , should it be
seq nat ?
Yeah, or more generally
seq T for some
T : eqType. In my case I want it for
w : seq 'I_n
\maxis not going to be defined for it right?
oh sorry it is F that should have nat as co-domain
I'm sleeping :)
Isn't it? As long as
F : T -> nat I think it should work.
I was looking into the new
order.v and indeed I think that there should be some lemmas there that are what you want
for example join_sup_seq
join_sup_seq: forall (disp : unit) (L : bLatticeType disp) (T : eqType) (r : seq T) (P : predPredType T) (F : T -> L) (x : T), x \in r -> P x -> (F x <= \join^d_(i <- r | P i) F i)%O
that's a bit convoluted but it is exactly that once you take max = join
meet_inf_seq , I ignore the difference
Cool, thank you!.
I somehow assumed there would be a generic / default way of moving between
I : finType and the other available bigop ranges (such as lists). Otherwise I feel like a lot of results are missing from the library.
You can see that proof just does reindex, so your lemma is recovered as:
Lemma ex x (w : seq R) (F : R -> nat) : x \in w -> F x <= \max_(y <- w) F y. Proof. by move=> /seq_tnthP[j->]; rewrite big_tnth leq_bigmax. Qed.
R is an eqType indeed.
Oh indeed our messages crossed, there is indeed the above trick.
but I think a Pull Request adding
leq_bigmax_seq would be nice
I guess it is a hard choice among clutter and convenience sometimes
another _huge_ question with math-comp is how to document your exact request "I somehow assumed there would be a generic / default way of moving between I : finType and the other available bigop ranges "
maybe a bigop FAQ?
Yeah, with math-comp I always feel like you need a huge well of this kind of knowledge. Many lemmas are "missing" for the simple reason that there is a simple and default way of going from existing lemmas to the would-be ones. There is this: https://github.com/math-comp/math-comp/wiki/gotchas which is more or less in the same vein.
Yeah it's like doing a puzzle sometimes :/
maybe some recent work on machine learning could build a good suggestor for that
for me, the most effective way is to read the library itself, for example that's how I remembed about
big_tnht I used to know about that, but I forgot.
What I recalled was that there was some place in order where they went from seqs to the finType case, so I searched and I could copy the code
@Ana de Almeida Borges , I just saw this discussion. I don't think I need to add to the topic, but I want to point out that this kind of topic would probably fit better in the "math-comp users" stream. I'm not sure how closely mathcomp users (like me) follow this stream.
Thanks! I didn't realize the streams shown in my dashboard were not 100% of the existing streams. It was just Zulip noobery.
This topic was moved here from #Coq users > How to use bigop results for different ranges by Cyril Cohen
Last updated: Feb 08 2023 at 08:02 UTC