Stream: math-comp users

Topic: How to use bigop results for different ranges


view this post on Zulip Ana de Almeida Borges (Sep 27 2020 at 18:46):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:36):

Hi, would you mind clarifying the type of w , should it be seq nat ?

view this post on Zulip Ana de Almeida Borges (Sep 27 2020 at 21:37):

Yeah, or more generally seq T for some T : eqType. In my case I want it for w : seq 'I_n

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:38):

But \maxis not going to be defined for it right?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:39):

oh sorry it is F that should have nat as co-domain

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:39):

I'm sleeping :)

view this post on Zulip Ana de Almeida Borges (Sep 27 2020 at 21:39):

Isn't it? As long as F : T -> nat I think it should work.

view this post on Zulip Ana de Almeida Borges (Sep 27 2020 at 21:39):

Hahah ok

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:45):

I was looking into the new order.v and indeed I think that there should be some lemmas there that are what you want

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:45):

for example join_sup_seq

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:45):

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

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:46):

that's a bit convoluted but it is exactly that once you take max = join

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:47):

also meet_inf_seq , I ignore the difference

view this post on Zulip Ana de Almeida Borges (Sep 27 2020 at 21:50):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:51):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:51):

where R is an eqType indeed.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:51):

Oh indeed our messages crossed, there is indeed the above trick.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:52):

but I think a Pull Request adding leq_bigmax_seq would be nice

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:52):

why not

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:52):

I guess it is a hard choice among clutter and convenience sometimes

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:52):

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 "

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:52):

maybe a bigop FAQ?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:52):

I dunno

view this post on Zulip Ana de Almeida Borges (Sep 27 2020 at 21:55):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:56):

+1

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:56):

Yeah it's like doing a puzzle sometimes :/

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:56):

maybe some recent work on machine learning could build a good suggestor for that

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:57):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 27 2020 at 21:57):

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

view this post on Zulip Christian Doczkal (Sep 30 2020 at 11:15):

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

view this post on Zulip Ana de Almeida Borges (Sep 30 2020 at 11:22):

Thanks! I didn't realize the streams shown in my dashboard were not 100% of the existing streams. It was just Zulip noobery.

view this post on Zulip Notification Bot (Sep 30 2020 at 15:43):

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