(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Manfred Kerber * Christoph Lange * Colin Rowat * Makarius Wenzel * Marco B. Caminati 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) *) header {* Maximum components of vectors, and their properties *} theory Maximum imports Main (* "~~/src/HOL/Library/AList" *) begin text{* The maximum component value of a vector y of non-negative values is equal to the value of one of the components, and it is greater or equal than the values of all [other] components. We implement this as a computable function, whereas in Theorema we had two axioms: \begin{enumerate} \item The maximum component value is equal to the value of one of the components \item @{text maximum_is_greater_or_equal} \end{enumerate} Here, we derive those two statements as lemmas from the definition of the computable function. Having the maximum as a computable function might turn out to be useful when doing concrete auctions. *} subsection {* Maximum *} text{* This subsection uses Isabelle's set maximum functions, wrapping them for our use. *} definition maximum_defined :: "'a set \ bool" where "maximum_defined N \ card N > 0" lemma maximum_except_defined: fixes N i assumes "i \ N" "card N > 1" shows "maximum_defined (N - {i})" using assms unfolding maximum_defined_def by (smt card.remove card_infinite) definition maximum :: "'a set \ ('a \ 'b::linorder) \ 'b" where "maximum N y = Max (y  N)" text{* If two vectors are equal, their maximum components are equal too *} lemma maximum_equal: fixes N :: "'a set" and y :: "'a \ 'b::linorder" and z :: "'a \ 'b::linorder" assumes "\i \ N. y i = z i" shows "maximum N y = maximum N z" proof - have "y  N = z  N" by (rule image_cong) (auto simp: assms) then show ?thesis unfolding maximum_def by simp qed text{* The maximum component value is greater or equal than the values of all [other] components *} lemma maximum_is_greater_or_equal: fixes N :: "'a set" and y :: "'a \ 'b::linorder" and i :: 'a assumes "maximum_defined N" and "i \ N" shows "maximum N y \ y i" using assms unfolding maximum_defined_def maximum_def by (simp add: card_gt_0_iff) text{* The maximum component is one component *} lemma maximum_is_component: fixes N :: "'a set" and y :: "'a \ 'b::linorder" assumes defined: "maximum_defined N" shows "\i \ N. maximum N y = y i" proof - let ?A = "y  N" from defined have "finite ?A" and "?A \ {}" unfolding maximum_defined_def by (simp_all add: card_gt_0_iff) then have "Max ?A \ ?A" by (rule Max_in) then obtain i where "i \ N" and "Max ?A = y i" by blast then show ?thesis unfolding maximum_def by fast qed text{* Being a component of a non-negative vector and being greater or equal than all other components uniquely defines a maximum component. *} lemma maximum_sufficient: fixes N :: "'a set" and y :: "'a \ 'b::linorder" and m :: 'b assumes defined: "maximum_defined N" and greater_or_equal: "\i \ N. m \ y i" and is_component: "\i \ N. m = y i" shows "maximum N y = m" unfolding maximum_def proof - let ?A = "y  N" show "Max ?A = m" proof (rule Max_eqI) from defined show "finite ?A" unfolding maximum_defined_def by (simp add: card_gt_0_iff) show "m \ ?A" using is_component by blast fix a assume "a \ ?A" then show "a \ m" using greater_or_equal by blast qed qed (* TODO CL: rename once widely used *) text {* the subset of elements of a set where a function reaches its maximum *} fun arg_max' :: "('a \ 'b\linorder) \ 'a set \ 'a set" where "arg_max' f A = { x \ A . f x = Max (f  A) }" text {* The arg max of a function over a non-empty set is non-empty. *} lemma arg_max'_non_empty_iff: fixes f::"'a \ 'b::linorder" and A::"'a set" assumes "A \ {}" and "finite A" shows "arg_max' f A \ {}" proof - from assms have "Max (f  A) \ f  A" by simp then obtain x where "x \ A" and "f x = Max (f  A)" by (auto simp: image_iff) then have "\ x . x \ A \ f x = Max (f  A)" by blast then show ?thesis by simp qed text{* the set of all indices of maximum components of a vector *} definition arg_max :: "'a set \ ('a \ 'b::linorder) \ 'a set" where "arg_max N b = {i \ N . maximum N b = b i}" (* need the explicit restriction "i \ N" as Isabelle/HOL assumes b to also be defined beyond the set N *) text{* the set of all indices of maximum components of a vector (computable version) *} fun arg_max_alg_list :: "'a list \ ('a \ 'b::linorder) \ 'a list" where "arg_max_alg_list [] f = []" | "arg_max_alg_list [x] f = [x]" | "arg_max_alg_list (x # xs) f = (let arg_max_xs = arg_max_alg_list xs f; prev_max = f (hd arg_max_xs) in if f x > prev_max then [x] else if f x = prev_max then x # arg_max_xs else arg_max_xs)" (* concerning information entropy it may be stupid to apply this "arg max" to an index set [31,45,99] because the same set could be represented as [0,1,2], and then we could implement the whole function in a different way: not finding the domain elements at which a function reaches its maximum value, but finding the indices of the maximum elements of a list (which is indexed 0,1,2,\). The latter is realised by the max_positions function below. However, in the setting where this function will be applied, this doesn't make much of a difference. In an auction with 100 participants all we need to do is to number them in an economic way as 0,\,99, and then the winner determination and payment computation will end up calling arg_max with index sets [1,\,99], [0,2,\,99], [0,1,3,\,99], \ *) text{* the set of all indices of maximum components of a vector (computable version with same signature as @{term arg_max}) *} fun arg_max_alg :: "'a::linorder set \ ('a \ 'b::linorder) \ 'a set" where "arg_max_alg N b = set (arg_max_alg_list (sorted_list_of_set N) b)" text{* the indices of the maximum values of the elements of a list *} fun max_positions :: "'a::ord list \ nat list" where "max_positions [] = []" | "max_positions [x] = [0]" | "max_positions (x # xs) = (let prevout = max_positions xs; prev_max = xs ! (hd prevout); nextout=map Suc prevout (* increment position indices *) in if x > prev_max then [0::nat] else if x ('a \ 'b::linorder) \ 'b" where "maximum_alg_list [] b = undefined" (* TODO CL: throw exception as per https://github.com/formare/auctions/issues/17 *) | "maximum_alg_list [x] b = b x" | "maximum_alg_list (x # xs) b = (let max_xs = maximum_alg_list xs b in if b x > max_xs then b x else max_xs)" fun maximum_alg :: "'a::linorder set \ ('a \ 'b::linorder) \ 'b" where "maximum_alg N b = maximum_alg_list (sorted_list_of_set N) b" text{* The maximum component that remains after removing one component from a vector is greater or equal than the values of all remaining components *} lemma maximum_except_is_greater_or_equal: fixes N :: "'a set" and y :: "'a \ 'b::linorder" and j :: 'a and i :: 'a assumes defined: "maximum_defined N" and i: "i \ N \ i \ j" shows "maximum (N - {j}) y \ y i" proof - let ?M = "N - {j}" let ?A = "y  ?M" from i have *: "i \ ?M" by simp with defined have "finite ?A" and "?A \ {}" unfolding maximum_defined_def by (auto simp: card_gt_0_iff) with * have "Max ?A \ y i" by (auto simp: Max_ge_iff) then show ?thesis unfolding maximum_def . qed text{* One component of a vector is a maximum component iff it has a value greater or equal tha n the maximum of the remaining values. *} lemma maximum_remaining_maximum: fixes N :: "'a set" and y :: "'a \ 'b::linorder" and j :: 'a assumes defined': "maximum_defined (N - {j})" and j_max: "y j = maximum N y" shows "y j \ maximum (N - {j}) y" proof - have "y  (N - {j}) \ y  N" by blast with defined' have "maximum (N - {j}) y \ maximum N y" unfolding maximum_def maximum_defined_def by (simp add: card_gt_0_iff Max_mono) also note j_max [symmetric] finally show ?thesis . qed text{* Changing one component in a vector doesn't affect the maximum of the remaining component s. *} lemma remaining_maximum_invariant: fixes N :: "'a set" and y :: "'a \ 'b::linorder" and i :: 'a and a :: 'b shows "maximum (N - {i}) (y(i := a)) = maximum (N - {i}) y" proof - let ?M = "N - {i}" have "y  ?M = (y(i := a))  ?M" by auto then show ?thesis unfolding maximum_def by simp qed (* TODO CL: revise as per https://github.com/formare/auctions/issues/17 *) (* MC: Yet another approach below, focusing on reusing stuff (Max, zip, map, filter) rather than doing our own recursion to calculate argmax *) definition filterpositions (*Non(directly)recursive generalization for max_positions, possibly less efficient. Given a list l, yields the indices of its elements which satisfy a given pred P*) :: "('a => bool) => 'a list => nat list" where "filterpositions P l = map snd (filter (P o fst) (zip l (upt 0 (size l))))" (* MC: After some experimentations, the following, more expressive equivalent writing also appears to be computable:*) definition filterpositions2 :: "('a => bool) => 'a list => nat list" where "filterpositions2 P l = [n. n \ [0.. [0.. nat list" where "maxpositions l = filterpositions2 (%x . x \ Max (set l)) l" lemma ll5: fixes l shows "maxpositions l = [ n . n \ [0.. Max (set l)]" using assms unfolding maxpositions_def filterpositions2_def by fastforce definition argmax :: "('a => ('b::linorder)) => 'a list => 'a list" where "argmax f l = map (nth l) (maxpositions (map f l))" lemma ll7: fixes m P shows "[n . n <- [0.. set [0.. Max (f(set l))]" proof - have "maxpositions (map f l) = (* [n. n <- [0.. Max (set (map f l))]*) [n. n <- [0.. set[0.. Max (set (map f l))] (*[n. n <- [0.. (map f l)!n \ Max (set (map f l)))]*) " using ll7 unfolding filterpositions2_def maxpositions_def . also have "... = [n . n <- [0.. Max (set (map f l)))] " by simp also have " ... = [n . n <- [0.. (n(map f l)!n \ Max (set (map f l)))] " by metis also have " ... = [n . n <- [0.. (nf (l!n) \ Max (set (map f l)))] " using nth_map by simp also have "... = [n . n <- [0.. (f (l!n) \ Max (set (map f l)))] " by metis also have "... = [n . n <- [0.. set [0.. (f (l!n) \ Max (set (map f l)))] " by simp also have "... = [n . n <- [0.. set [0.. Max (set (map f l)))] " by metis also have "... = [n . n <- [0.. Max (set (map f l))]" using ll7 by presburger finally show ?thesis by auto qed lemma ll10: fixes f m P shows "(map f [n . n <- [0.. Max (f(set l))]" proof - have "maxpositions (map f l) = [n . n <- [0.. Max (f(set l))]" using ll9 by fast hence "map (nth l) (maxpositions (map f l)) = map (nth l) [n . n <- [0.. Max (f(set l))]" by presburger also have "... = [ l!n . n <- [0.. Max (f(set l))]" using ll10 by fast finally show ?thesis unfolding argmax_def . qed (* MC: map_commutes, filterpositions are fairly general and should be moved elsewhere *) 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]" proof - (* MC: There must surely be a much better proof for this simple fact *) fix f::"'a => 'b" fix Q let ?g="\n. (if Q (f n) then [f n] else [])" let ?lh="%l . concat (map ?g l)" let ?rh="%l . filter Q (map f l)" let ?I="%m . (\ l::('a list) . ((size l=m) \ (?lh l = ?rh l)))" have 10: "?I 0" by force have 11: "\ m::nat . ((?I m) \ (?I (Suc m)))" proof fix m::nat show "(?I m) \ (?I (Suc m))" proof assume 1: "?I m" show "?I (Suc m)" proof - { fix L::"'a list" let ?A="take 1 L" let ?a="hd L" let ?l="tl L" assume "size L=Suc m" hence 2: "L=?a#?l \ L=[?a]@?l \ size ?l=m" by (metis Suc_neq_Zero append_Cons append_Nil append_Nil2 append_eq_conv_conj diff_Suc_1 length_0_conv length_tl take_Suc) hence 0: "concat (map ?g ?l) = filter Q (map f ?l)" using 1 by blast hence "(concat (map ?g (?a#?l))) = (?g ?a)@(concat (map ?g ?l))" by fastforce also have "...= (?g ?a)@(filter Q (map f ?l))" using 0 by force also have "...= (filter Q [f ?a])@(filter Q (map f ?l))" by fastforce also have "...= (filter Q (map f [?a]))@(filter Q (map f ?l))" by force also have "...= (filter Q ((map f [?a])@(map f ?l)))" by fastforce also have "...= (filter Q (map f ([?a]@?l)))" by auto also have "...= ?rh L" using 2 by presburger finally have "?lh L = ?rh L" using 2 by metis } thus "?I (Suc m)" by fast qed qed qed { fix k have "?I k" proof (rule nat.induct) show "?I 0" using 10 by blast next fix m assume "?I m" thus "?I (Suc m)" using 11 by blast qed } hence "\ m . (?I m)" by fast hence 3: "\ l . (?lh l) = (?rh l)" by blast fix xs show "[ f n . n <- xs, Q (f n)] = [x <- (map f xs). Q x]" using 3 by blast qed theorem argmaxadequacy: (* MC: RHS of thesis should formally reassure about what argmax does. I didn't use it directly as a definition of the latter (both appear to be computable) because I find filterpositions of independent interest*) fixes f::"'a => ('b::linorder)" fixes l::"'a list" shows "argmax f l = [ x <- l. f x \ Max (f(set l))]" proof - let ?lh="argmax f l" let ?P="% y::('b::linorder) . y \ Max (f(set l))" let ?mh="[nth l n . n <- [0..