## Stream: math-comp users

### Topic: arg min

#### Ricardo (Feb 28 2023 at 02:31):

Hi. I'm trying to understand how to use the notation [arg min_(i < i0 in A) M] from fintype. I have an fset A : {fset T1} and a function f : A -> {fset T2} and I want to know what's the element x of A that minimises the value #|f x|. Ideally I'd write something like

[arg min(x in A) #|f x|]


However, I (expectedly) get Syntax error: '<' expected after [term level 10] (in [term]). If I write

Variable i0 : A.
Check [arg min_(x < i0 in A) #|f x|].


I get The term "mem A" has type "mem_pred T1" while it is expected to have type "mem_pred A".

The whole thing is

From mathcomp Require Import all_ssreflect finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope fset.
Coercion fset_sub_finType : finSet >-> finType.

Variables (T1 T2 : choiceType) (A : {fset T1}).
Hypothesis (f : A -> {fset T2}).
Variable i0 : A.
Check #|f i0|.
Check [arg min_(x < i0 in A) #|f x|]. (* fails *)
Check [arg min_(x in A) #|f x|]. (* also fails *)


Two questions:

1. What is the role of i0 in the argmin expression?
2. How do I get the element of A that minimises some value?

#### Ricardo (Feb 28 2023 at 02:35):

What I actually need is a function that produces the pair (x, f x) for the x that minimises the cardinality of f x.

#### Paolo Giarrusso (Feb 28 2023 at 05:33):

in A is optional, while < i0 or > i0 isn't — so arg min_(i < i0) — according to the top-level doc (but also the code: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fintype.v#L137-L152).

i0 is used to show the "search space" is not empty, which is necessary for this notation to return an A that fulfills the spec.

#### Ricardo (Feb 28 2023 at 16:39):

I see. Thank you :smile:

#### Ricardo (Feb 28 2023 at 16:40):

Is there a version of argmin that returns an option so that when the search space is empty it gives None?

#### Ricardo (Feb 28 2023 at 17:46):

[pick x in A] does that

#### Laurent Théry (Feb 28 2023 at 19:01):

maybe something like this

From mathcomp Require Import all_ssreflect finmap.

Variable T1 T2 : finType.
Variable A : {fset T1}.
Variable f : A -> {fset T2}.
Check [pick i : A | #|f i| == \big[minn/0]_(i : A) #|f i|].


#### Paolo Giarrusso (Feb 28 2023 at 20:20):

The implementation core is essentially this, and you only need to take out the odflt i0 bit. I'm not sure why math-comp doesn't expose this already, even if of course you can't expose everything

Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I -> T) :=
[pred i | P i & [forall (j | P j), ord (F i) (F j)]].

Definition extremum := odflt i0 (pick (arg_pred ord P F)).


#### Ricardo (Mar 01 2023 at 03:24):

I see. Thank you both! \big[minn/0]_(i : A) #|f i| is what I was looking for!

#### Ricardo (Mar 01 2023 at 03:34):

Paolo Giarrusso said:

I'm not sure why math-comp doesn't expose this already, even if of course you can't expose everything

I agree it'd be great if math-comp would expose this.

#### Pierre Roux (Mar 01 2023 at 07:13):

Ricardo said:

I see. Thank you both! \big[minn/0]_(i : A) #|f i| is what I was looking for!

Are you sure? It seems to me that this is always equal to 0?

(deleted)

#### Laurent Théry (Mar 01 2023 at 09:06):

Don´t see anything better than

Definition get_min :=
oapp (fun x => #| f [arg min_(i < x) #|f i |] |) 0 [pick i : A].


#### Laurent Théry (Mar 01 2023 at 09:07):

Lemma get_min_p1 (a : A) : get_min <= #| f a|.
Proof.
rewrite /get_min; case: pickP => /= [b _|/(_ a)//].
by case: arg_minnP => // j _; apply.
Qed.

Lemma get_min_p2 (a : A) : exists (b : A), get_min = #| f b|.
Proof.
rewrite /get_min; case: pickP => /= [b _|/(_ a)//].
by case: arg_minnP => // i _ H; exists i.
Qed.


#### Ricardo (Mar 01 2023 at 15:58):

Pierre Roux said:

Are you sure? It seems to me that this is always equal to 0?

Why is this always equal to 0?

#### Laurent Théry (Mar 01 2023 at 16:06):

because big[+/0]_(i < n) x_i = x_0 + (x_1 .... + (x_n.-1 + 0))...))

Alright. I see.

#### Ricardo (Mar 01 2023 at 17:09):

In some languages there are two types of fold, one that takes an initial value and one that doesn't. So the semantics would be fold f xs is equal to Some x for x = f x0 (f x1 ... (f xn.-1 xn) ...) if the lenght of xs is bigger than 1, x = x0 if the length is equal to 1, and None if xs is empty.

#### Ricardo (Mar 01 2023 at 17:11):

The (a : A) isn't needed in get_min_p2 I think

#### Laurent Théry (Mar 02 2023 at 09:48):

Ricardo said:

In some languages there are two types of fold, one that takes an initial value and one that doesn't. So the semantics would be fold f xs is equal to Some x for x = f x0 (f x1 ... (f xn.-1 xn) ...) if the lenght of xs is bigger than 1, x = x0 if the length is equal to 1, and None if xs is empty.

Yep but in the bigop library the fold that has been chosen is the one that gives nice inductive proofs. :wink:

#### Laurent Théry (Mar 02 2023 at 09:51):

Ricardo said:

The (a : A) isn't needed in get_min_p2 I think

are you sure? If A is empty, how can you get exists (b: A), ... ?

#### Ricardo (Mar 06 2023 at 00:43):

Laurent Théry said:

Ricardo said:
are you sure? If A is empty, how can you get exists (b: A), ... ?

I see.

#### Ricardo (Mar 07 2023 at 01:14):

Laurent Théry said:

Don´t see anything better than

Definition get_min :=
oapp (fun x => #| f [arg min_(i < x) #|f i |] |) 0 [pick i : A].


I understand this definition now. Thank you @Laurent Théry for this :orange_heart:

#### Ricardo (Mar 07 2023 at 03:28):

Paolo Giarrusso said:

The implementation core is essentially this, and you only need to take out the odflt i0 bit. I'm not sure why math-comp doesn't expose this already, even if of course you can't expose everything

Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I -> T) :=
[pred i | P i & [forall (j | P j), ord (F i) (F j)]].

Definition extremum := odflt i0 (pick (arg_pred ord P F)).


I'm writing a variant of extremum that doesn't have the odflt i0 bit. I have the following.

Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I -> T) :=
[pred i | P i & [forall (j | P j), ord (F i) (F j)]].
Section Extremum.
Context {T : eqType} {I : finType}
(ord : rel T) (P : pred I) (F : I -> T).
Definition extremum := pick (arg_pred ord P F).
End Extremum.


I feel like it'd be good to pair it with a variant of extremum_spec so that one can prove Lemma extremumP : extremum_spec ord P F extremum. However, I'm not sure how to write extremum_spec to make this work or if I perhaps should keep extremum_spec as it is and add a hypothesis to extremumP that asks for the non-emptiness of I. I can write something like this right after the definition of extremum.

Lemma extremumP : if extremum is Some e
then extremum_spec ord P F e else True.
Proof. rewrite /extremum.
case: pickP => [i /andP[Pi /'forall_implyP/= min_i] | no_i].
by split=> // j; apply/implyP. done.
Qed.


Only the first two lines of the proof of extremumP in fintype.v were necessary to prove this variant. Does this make sense?

#### Ricardo (Mar 16 2023 at 06:25):

I'm having this now.

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Variant extremum_spec {T : eqType} (ord : rel T)
{I : finType} (P : pred I) (F : I -> T)
: option I -> Type :=
| Extremum i of P i & (forall j : I, P j -> ord (F i) (F j))
: extremum_spec ord P F (Some i)
| NoExtremum of P =1 xpred0 : extremum_spec ord P F None.

Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I -> T) :=
[pred i | P i & [forall (j | P j), ord (F i) (F j)]].

Section Extremum.
Variables (T : eqType) (ord : rel T)
(I : finType) (P : pred I) (F : I -> T).
Definition extremum : option I := pick (arg_pred ord P F).

Hypothesis ord_refl : reflexive ord.
Hypothesis ord_trans : transitive ord.
Hypothesis ord_total : total ord.
Lemma extremumP : extremum_spec ord P F extremum.
Proof using ord_refl ord_total ord_trans.
rewrite /extremum.
case: pickP => [i /andP[Pi /'forall_implyP xtrm]|].
constructor => //.
rewrite /eqfun /= => no_i. constructor.
rewrite /eqfun => i. apply: negbTE. move/negbT: (no_i i).
rewrite negb_and => /orP[notPi | /negP noXtm] //.
apply/negP. move=> Pi.
have := sort_sorted ord_total [seq F k | k <- enum P].
set s := sort _ _ => ss.
have s_gt0 : size s > 0.
- rewrite size_sort size_map -cardE. apply/card_gt0P. by exists i.
pose t0 := nth (F i) s 0.
have: t0 \in s by rewrite mem_nth.
rewrite mem_sort => /mapP/sig2_eqW[it0].
rewrite mem_enum => it0P def_t0.
have /negP[/=] := no_i it0.
rewrite [P _]it0P/=. apply/'forall_implyP => j Pj.
have /(nthP (F i))[k g_lt <-] : F j \in s
by rewrite mem_sort map_f ?mem_enum.
by rewrite -def_t0 sorted_leq_nth.
Qed.
End Extremum.

Section ArgMinMax.
Variables (I : finType) (P : pred I) (F : I -> nat).
Definition arg_min := extremum leq P F.
Definition arg_max := extremum geq P F.
End ArgMinMax.

Notation "[ 'arg' 'min_' ( i | P ) F ]" :=
(arg_min (fun i => P%B) (fun i => F))
(at level 0, i at level 10,
format "[ 'arg'  'min_' ( i  |  P )  F ]") : nat_scope.
Notation "[ 'arg' 'min_' ( i 'in' A ) F ]" :=
[arg min_(i | i \in A) F]
(at level 0, i at level 10,
format "[ 'arg'  'min_' ( i  'in'  A )  F ]") : nat_scope.
Notation "[ 'arg' 'max_' ( i | P ) F ]" :=
(arg_max (fun i => P%B) (fun i => F))
(at level 0, i at level 10,
format "[ 'arg'  'max_' ( i  |  P )  F ]") : nat_scope.
Notation "[ 'arg' 'max_' ( i 'in' A ) F ]" :=
[arg max_(i | i \in A) F]
(at level 0, i at level 10,
format "[ 'arg'  'max_' ( i  'in'  A )  F ]") : nat_scope.


@Cyril Cohen and others, do you think this could be a good addition to fintype?

#### Cyril Cohen (Mar 16 2023 at 08:59):

Sure, but it cannot subsume extremum (there is no backward compatibility here), so it must be an additional piece of theory. (you could prefix everything witho for example, to denote that it's the optional variant of extremum)

#### Cyril Cohen (Mar 16 2023 at 10:33):

And since we will keep both in the end, we can prove one using the other:

Variant oextremum_spec {T : eqType} (ord : rel T)
{I : finType} (P : pred I) (F : I -> T) : option I -> Type :=
| OExtremum i of P i & (forall j : I, P j -> ord (F i) (F j))
: oextremum_spec ord P F (Some i)
| NoOExtremum of P =1 xpred0 : oextremum_spec ord P F None.

Section OExtremum.
Variables (T : eqType) (ord : rel T) (I : finType) (P : pred I) (F : I -> T).

Let r (x y : option T) :=  match x, y with
Some u, Some v => ord u v | _, None => true | _, _ => false end.

Definition oextremum := [arg[r]_(i < None | oapp P true i) omap F i].

Hypothesis ord_refl : reflexive ord.
Hypothesis ord_trans : transitive ord.
Hypothesis ord_total : total ord.

Lemma oextremumP : oextremum_spec ord P F oextremum.
Proof using ord_refl ord_total ord_trans.
rewrite /oextremum; case: extremumP => //=; first by case.
- by move=> [?|] [?|] [?|]//; apply: ord_trans.
- by move=> [a|] [b|]/=.
case=> [i Pi imax|_ nomax]; first by constructor=> // *; apply: (imax (Some _)).
by constructor=> i; apply/negP => Pi; have /= := nomax (Some i) Pi.
Qed.

End OExtremum.


#### Ricardo (Mar 16 2023 at 23:47):

Wouldn't it be more natural to define extremum in terms of oextremum?

Definition oextremum : option I := pick (arg_pred ord P F).
Definition extremum i0 : I := odflt i0 oextremum.


or

Definition extremum i0 : I := odflt i0 (pick (arg_pred ord P F)).
Let r (x y : option T) :=  match x, y with
Some u, Some v => ord u v | _, None => true | _, _ => false end.
Definition oextremum := [arg[r]_(i < None | oapp P true i) omap F i].


Last updated: Jul 25 2024 at 16:02 UTC