Stream: math-comp users

Topic: \max with orderType


view this post on Zulip Pierre Jouvelot (Apr 18 2022 at 10:02):

I'm having trouble setting up some bigop operations with order.v. What am I doing wrong below?

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import all_algebra.
From mathcomp Require Import fingroup.perm.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Bigop.

Import Order.Theory.

Variable (T : orderType tt).

Variable (k : nat) (t : k.+1.-tuple T).

Lemma bigmax_in n : \max_(i < k.+1 | i < n.+1) tnth t i \in t.

which yields the message:

The term "tnth t i" has type "Order.Total.sort T" while it is expected to have type "nat".

Is the \maxis not recognized properly?

view this post on Zulip Laurent Théry (Apr 18 2022 at 10:25):

You are using the bigop on the natural numbers (you can check with Locate "\max_ _ _ ".) In order to do a maxoperation you need a bottom element. So this is ok for nat (0 is the bottom element) but not with an ordered type. Maybe an alternative is to use join on a lattice with a bottom element.

view this post on Zulip Pierre Jouvelot (Apr 18 2022 at 10:30):

Thanks for the possible fix :) Is there no way to convey the fact that i'm using a non-empty set on which to perform the \max for the notation to make sense?

view this post on Zulip Laurent Théry (Apr 18 2022 at 17:15):

you may use [arg max_(i > ord0 | ((i : 'I_k.+1) < n.+1)%N) tnth t i]%O to get the index that holds the maximal value.

view this post on Zulip Pierre Jouvelot (Apr 18 2022 at 18:19):

This looks pretty slick. Thanks a lot.


Last updated: Jan 29 2023 at 18:03 UTC