Pierre Jouvelot (Apr 18 2022 at 10:02): 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?
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.
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?
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.
Pierre Jouvelot (Apr 18 2022 at 18:19):This looks pretty slick. Thanks a lot.
Last updated: Oct 13 2024 at 01:02 UTC