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
* ISC License (1-clause BSD License)
See LICENSE file for details
(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