(*
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..