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`

But `\max`

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

Hahah ok

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

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

where `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

why not

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?

I dunno

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.

+1

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