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:

- What is the role of
`i0`

in the argmin expression? - How do I get the element of
`A`

that minimises some value?

What I actually need is a function that produces the pair `(x, f x)`

for the `x`

that minimises the cardinality of `f x`

.

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

I see. Thank you :smile:

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

`[pick x in A]`

does that

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|].
```

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 see. Thank you both! `\big[minn/0]_(i : A) #|f i|`

is what I was looking for!

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.

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`

?

oops :my bad

(deleted)

Don´t see anything better than

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

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

Pierre Roux said:

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

`0`

?

Why is this always equal to `0`

?

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

Alright. I see.

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.

The `(a : A)`

isn't needed in `get_min_p2`

I think

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:

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), ... `

?

Laurent Théry said:

Ricardo said:

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

?

I see.

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:

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?

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?

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 with`o`

for example, to denote that it's the optional variant of extremum)

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

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