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: Oct 13 2024 at 01:02 UTC