# Theory Argmax

```(*
Auction Theory Toolbox (http://formare.github.io/auctions/)

Authors:
* Marco B. Caminati http://caminati.co.nr
* Manfred Kerber <mnfrd.krbr@gmail.com>
* Christoph Lange <math.semantic.web@gmail.com>
* Colin Rowat <c.rowat@bham.ac.uk>

Dually licenced under
* Creative Commons Attribution (CC-BY) 3.0
(Rationale for this dual licence: http://arxiv.org/abs/1107.3212)
*)

section ‹Locus where a function or a list (of linord type) attains its maximum value›

theory Argmax
imports Main

begin

text ‹Structural induction is used in proofs on lists.›
lemma structInduct: assumes "P []" and "∀x xs. P (xs) ⟶ P (x#xs)"
shows "P l"
using assms list_nonempty_induct by (metis)

text ‹the subset of elements of a set where a function reaches its maximum›
fun argmax :: "('a ⇒ 'b::linorder) ⇒ 'a set ⇒ 'a set"
where "argmax f A = { x ∈ A . f x = Max (f ` A) }"

(* For reasons we do not understand we have to duplicate the definition as a lemma
in order to prove lm16 in CombinatorialAuctions.thy. *)
lemma argmaxLemma: "argmax f A = { x ∈ A . f x = Max (f ` A) }"
by simp

lemma maxLemma:
assumes "x ∈ X" "finite X"
shows "Max (f`X) >= f x"
(is "?L >= ?R") using assms
by (metis (opaque_lifting, no_types) Max.coboundedI finite_imageI image_eqI)

lemma lm01:
"argmax f A = A ∩ f -` {Max (f ` A)}"
by force

lemma lm02:
assumes "y ∈ f`A"
shows "A ∩ f -` {y} ≠ {}"
using assms by blast

lemma argmaxEquivalence:
assumes "∀x∈X. f x = g x"
shows "argmax f X = argmax g X"
using assms argmaxLemma Collect_cong image_cong
by (metis(no_types,lifting))

text ‹The arg max of a function over a non-empty set is non-empty.›
corollary argmax_non_empty_iff: assumes "finite X" "X ≠ {}"
shows "argmax f X ≠{}"
using assms Max_in finite_imageI image_is_empty lm01 lm02
by (metis(no_types))

text ‹The previous definition of argmax operates on sets. In the following we define a corresponding notion on lists. To this end, we start with defining a filter predicate and are looking for the elements of a list satisfying a given predicate;
but, rather than returning them directly, we return the (sorted) list of their indices.
This is done, in different ways, by @{term filterpositions} and @{term filterpositions2}.›

(* Given a list l, filterpositions yields the indices of its elements which satisfy a given pred P*)
definition filterpositions :: "('a => bool) => 'a list => nat list"
where "filterpositions P l = map snd (filter (P o fst) (zip l (upt 0 (size l))))"
(* That is, you take the list [a0, a1, ..., an] pair with the indices [0, 1, ..., n], i.e., you get
[(a0,0), (a1,1), ..., (an,n)] look where the predicate (P o fst) holds and return the list of the
corresponding snd elements. *)

(* Alternative definition, making use of list comprehension. In the next line the type info is
commented out, since the type inference can be left to Isabelle. *)
definition filterpositions2 (*  :: "('a => bool) => 'a list => nat list" *)
where "filterpositions2 P l = [n. n ← [0..<size l], P (l!n)]"

definition maxpositions (*:: "'a::linorder list => nat list"*)
where "maxpositions l = filterpositions2 (%x . x ≥ Max (set l)) l"

lemma lm03: "maxpositions l = [n. n←[0..<size l], l!n ≥ Max(set l)]"
unfolding maxpositions_def filterpositions2_def by fastforce

(* argmaxList takes a function and a list as arguments and looks for the positions of the elements at which the function applied to the list element is maximal, e.g.,
for the list [9, 3, 5, 9, 13] and the function `modulo 8', the function applied to the list would give the list [1, 3, 5, 1, 5], that is, argmaxList will return [2, 4]. *)
definition argmaxList (*:: "('a => ('b::linorder)) => 'a list => 'a list"*)
where "argmaxList f l = map (nth l) (maxpositions (map f l))"

(* The following lemmas state some relationships between different representation such as map and list comprehension *)
lemma lm04: "[n . n <- l, P n] = [n . n <- l, n ∈ set l, P n]"
proof -
(*sledgehammer-generated proof.
Commented out the first three lines (they look quite useless), making it more readable.
assume "∀v0. SMT2.fun_app uu__ v0 = (if P v0 then [v0] else [])"
assume "∀v0. SMT2.fun_app uua__ v0 = (if v0 ∈ set l then if P v0 then [v0] else [] else [])"
obtain v3_0 :: "('a ⇒ 'a list) ⇒ 'a list ⇒ ('a ⇒ 'a list) ⇒ 'a" where *)
have "map (λuu. if P uu then [uu] else []) l =
map (λuu. if uu ∈ set l then if P uu then [uu] else [] else []) l" by simp
thus "concat (map (λn. if P n then [n] else []) l) =
concat (map (λn. if n ∈ set l then if P n then [n] else [] else []) l)" by presburger
qed

lemma lm05: "[n . n <- [0..<m], P n] = [n . n <- [0..<m], n ∈ set [0..<m], P n]"
using lm04 by fast
(* sledgehammer suggested:  concat_map_singleton map_ident  map_ext by smt*)

lemma lm06: fixes f m P
shows "(map f [n . n <- [0..<m], P n]) = [ f n . n <- [0..<m], P n]"
by (induct m) auto

(* Base case stating the property for the empty list *)
lemma map_commutes_a: "[f n . n <- [], Q (f n)] = [x <- (map f []). Q x]"
by simp

(* Step case where the element x is added to the list xs *)
lemma map_commutes_b: "∀ x xs. ([f n . n <- xs,     Q (f n)] = [x <- (map f xs).     Q x] ⟶
[f n . n <- (x#xs), Q (f n)] = [x <- (map f (x#xs)). Q x])"
by simp

(* General case comprising the two previous cases. *)
lemma map_commutes: fixes f::"'a => 'b" fixes Q::"'b => bool" fixes xs::"'a list"
shows "[f n . n <- xs, Q (f n)] = [x <- (map f xs). Q x]"
using map_commutes_a map_commutes_b structInduct by fast

lemma lm07: fixes f l
shows "maxpositions (map f l) =
[n . n <- [0..<size l], f (l!n) ≥ Max (f`(set l))]"
(is "maxpositions (?fl) = _") (* Pattern matching abbreviation ?fl corresponds to (map f l). Used in the proof, not part of lemma itself *)
proof -
have "maxpositions ?fl =
[n. n <- [0..<size ?fl], n∈ set[0..<size ?fl], ?fl!n ≥ Max (set ?fl)]"
using lm04 unfolding filterpositions2_def maxpositions_def .
also have "... =
[n . n <- [0..<size l], (n<size l), (?fl!n  ≥ Max (set ?fl))]" by simp
also have "... =
[n . n <- [0..<size l], (n<size l) ∧ (f (l!n)  ≥ Max (set ?fl))]"
using nth_map by (metis (poly_guards_query, opaque_lifting)) also have "... =
[n . n <- [0..<size l], (n∈ set [0..<size l]),(f (l!n)  ≥ Max (set ?fl))]"
using atLeastLessThan_iff le0 set_upt by (metis(no_types))
also have "... =
[n . n <- [0..<size l], f (l!n) ≥ Max (set ?fl)]" using lm05 by presburger
finally show ?thesis by auto
qed

lemma lm08: fixes f l
shows "argmaxList f l =
[ l!n . n <- [0..<size l], f (l!n) ≥ Max (f`(set l))]"
unfolding lm07 argmaxList_def by (metis lm06)

text‹The theorem expresses that argmaxList is the list of arguments greater equal the Max of the list.›

theorem argmaxadequacy: fixes f::"'a => ('b::linorder)" fixes l::"'a list"
shows "argmaxList f l = [ x <- l. f x ≥ Max (f`(set l))]"
(is "?lh=_") (* pattern match ?lh abbreviates "argmaxList f l" *)
proof -
let ?P="% y::('b::linorder) . y ≥ Max (f`(set l))"
let ?mh="[nth l n . n <- [0..<size l], ?P (f (nth l n))]"
let ?rh="[ x <- (map (nth l) [0..<size l]). ?P (f x)]"
have "?lh = ?mh" using lm08 by fast
also have "... = ?rh" using map_commutes by fast
also have "...= [x <- l. ?P (f x)]" using map_nth by metis
finally show ?thesis by force
qed

end

```