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 `\max`

is not recognized properly?

You are using the `bigop`

on the natural numbers (you can check with `Locate "\max_ _ _ ".`

) In order to do a `max`

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

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?

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.

This looks pretty slick. Thanks a lot.

Last updated: Jul 15 2024 at 20:02 UTC