(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Manfred Kerber * Christoph Lange * Colin Rowat * Makarius Wenzel 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 {* Case check of Second price single good auctions *} theory SecondPriceAuctionSoundness imports FullySpecifiedSecondPriceAuctionSoundness RelationUtils begin (* TODO CL: This lemma also works when admissibility is defined as "card N > 0" because when we compute the second-highest bid for the payments vector, card N = 0 will boil down to the question of whether Max {} exists. Isabelle says that it exists; to see this try lemma max_exists : "\x . x = Max {}" by blast This is an inherent trait of Isabelle's HOL implementation: all functions are total in principle, just sometimes underspecified, so that you don't know _what_ "Max {}" is. To see this try value "Max {}" vs. value "Max {1::nat, 2}" Isabelle supports partial functions. One can either use explicit undefinedness (using the Option datatype with the None and Some constructors), but that would affect and thus bloat large parts of our formalisation. In "isabelle doc functions" section 7 there is also something that looks like a more sophisticated support for partial functions. For now, spa_is_left_total doesn't catch the case "card N = 1", but spa_vickrey_payment, which is part of our checks whether the outcome is well-defined, doesn't work for "case N = 1". For precise details, see the comment in spa_vickrey_payment. So, @CR, this is really a good justification for why we need spa_vickrey_payment. Indeed the whole battery of case checks now covers: "for each admissible input there is (that's left-totality) a unique (that's right-uniqueness), well-defined (that's spa_vickrey_payment and spa_allocates) outcome." *) text{* Our relational definition of second price auction is left-total. *} lemma spa_is_left_total : fixes A :: single_good_auction (* A is the set of all second price auctions. Assuming "second_price_auction A" would merely mean that all elements of A are second price auctions, which is not enough here. *) assumes spa: "rel_all_sga_pred spa_pred A" shows "sga_left_total A spa_admissible_input" proof - (* We define ourselves an arbitrary tie breaker *) have foo: "\t . \N . wb_tie_breaker_on t N" (* TODO CL: If the following ever gets deleted _here_, preserve it somewhere else in the toolbox. *) proof - def t \ "op>::(participant \ participant \ bool)" then have wb_tie: "\N . wb_tie_breaker_on t N" unfolding wb_tie_breaker_on_def strict_linear_order_on_def trans_def irrefl_def total_on_def by (smt bot_least insert_subset mem_Collect_eq prod.cases) then show ?thesis by blast qed then obtain t where wb_tie: "\N . wb_tie_breaker_on t N" by (smt someI_ex) (* Note that it is not necessary to prove that fs_spa_pred' is satisfiable. *) def fs_spa_pred'' \ "\ tup . (\ N b x p . tup = ((N, b), (x, p)) \ (fs_spa_pred' t) N b x p)" then have "\ A . (\ tup . tup \ A \ fs_spa_pred'' tup)" by (metis mem_Collect_eq) with fs_spa_pred''_def have "\ A . (\ a b c d . ((a, b), (c, d)) \ A \ (fs_spa_pred' t) a b c d)" by simp then obtain B where B_fs_spa: "rel_all_sga_pred (fs_spa_pred' t) B" unfolding rel_all_sga_pred_def .. with spa have sup: "B \ A" using rel_all_fs_spa_is_spa by simp from B_fs_spa wb_tie fs_spa_is_left_total have B_left_total: "sga_left_total B spa_admissible_input" by simp then show ?thesis unfolding sga_left_total_def using sup by (rule suprel_left_total_on) qed (* alternative direct proof: proof (rule sga_left_totalI) fix N :: "participant set" and b :: bids assume admissible: "spa_admissible_input N b" from admissible obtain winner::participant where winner_def: "winner \ N \ winner \ arg_max N b" using spa_admissible_input_def arg_max_def maximum_defined_def maximum_is_component by (smt mem_Collect_eq) def x \ "\ i::participant . if i = winner then 1::real else 0" def p \ "\ i::participant . if i = winner then maximum (N - {i}) b else 0" from x_def p_def winner_def admissible have "spa_pred N b x p" unfolding second_price_auction_winner_outcome_def second_price_auction_loser_outcome_def spa_pred_def by force with spa show "\ (x :: allocation) (p :: payments) . ((N, b), (x, p)) \ A" unfolding rel_all_sga_pred_def by fast qed *) text{* We consider two outcomes of a second price auction equivalent if \begin{enumerate} \item the bids of the participants to which the good is allocated are equal \item the bids of the participants with positive payments are equal \end{enumerate} This should be as weak as possible, as not to accidentally restate the full definition of a second price auction. *} definition spa_equivalent_outcome :: "participant set \ bids \ allocation \ payments \ allocation \ payments \ bool" where "spa_equivalent_outcome N b x p x' p' \ b  { i \ N . x i = 1 } = b  { i \ N . x' i = 1 } \ b  { i \ N . p i > 0 } = b  { i \ N . p' i > 0 }" (* This definition is more general in that it allow for divisible goods. *) text{* Under certain conditions we can show that the bids of the participant set with positive payments are equal (one direction of the equality) *} lemma positive_payment_bids_eq_suff : fixes N :: "participant set" and winner :: participant and b :: bids and p :: payments and p' :: payments assumes admissible: "spa_admissible_input N b" and range: "winner \ N \ winner \ arg_max N b" and pay: "p winner = maximum (N - {winner}) b \ (\j \ N . j \ winner \ p j = 0)" and range': "winner' \ N \ winner' \ arg_max N b" and pay': "p' winner' = maximum (N - {winner'}) b \ (\j \ N . j \ winner' \ p' j = 0)" shows "b  { i \ N . p i > 0 } \ b  { i \ N . p' i > 0 }" proof (intro subsetI) from admissible have bids: "bids N b" and ge2: "card N > 1" using spa_admissible_input_def by auto fix bid assume premise: "bid \ b  { i \ N . p i > 0 }" with range pay range' have bw': "bid = b winner'" unfolding arg_max_def by force from premise pay have p_positive: "p winner > 0" by auto with ge2 range pay have bwpos: "b winner > 0" using arg_max_def maximum_except_defined maximum_remaining_maximum by (smt mem_Collect_eq) from ge2 range' have md: "maximum_defined (N - {winner'})" using maximum_except_defined by (auto simp only: conjE) have "maximum (N - {winner'}) b > 0" proof (rule ccontr) assume assm: "\ maximum (N - {winner'}) b > 0" { fix i assume i_range: "i \ (N - {winner'})" with bids have bipos: "b i \ 0" unfolding bids_def non_negative_def le_def zero_def by blast from md have "maximum (N - {winner'}) b \ b i" using i_range by (rule maximum_is_greater_or_equal) then have "maximum (N - {winner'}) b = 0" using assm bipos by simp } with assm range range' pay pay' have foow': "maximum (N - {winner'}) b = 0" using maximum_is_component md by metis show False proof cases assume "winner' = winner" then show False using p_positive pay foow' by auto next assume "winner' \ winner" with range have "winner \ N - {winner'}" by fast then have x: "maximum (N - {winner'}) b \ b winner" using range md by (simp only: maximum_is_greater_or_equal) with foow' have bwzn: "b winner \ 0" by auto from range have "maximum N b = b winner" unfolding arg_max_def by auto with md x maximum_remaining_maximum bwpos bwzn show False by auto qed qed then show "bid \ b  { i \ N . p' i > 0 }" using range' pay' bw' by auto qed lemma spa_winner_from_rel: assumes "rel_all_sga_pred spa_pred A" and "((N, b), (x, p)) \ A" obtains winner where "winner \ N \ winner \ arg_max N b" and "x winner = 1 \ (\ j \ N . j \ winner \ x j = 0)" and "p winner = maximum (N - {winner}) b \ (\j \ N . j \ winner \ p j = 0)" proof - from assms obtain winner::participant where "winner \ N \ winner \ arg_max N b" and "x winner = 1 \ (\ j \ N . j \ winner \ x j = 0)" and "p winner = maximum (N - {winner}) b \ (\j \ N . j \ winner \ p j = 0)" unfolding rel_all_sga_pred_def spa_pred_def second_price_auction_winner_outcome_def second_price_auction_loser_outcome_def by smt (* Interestingly the corresponding step in fs_spa_winner_from_rel works by blast. *) then show ?thesis .. qed text{* Our relational definition of second price auction is right-unique. *} lemma spa_is_right_unique : fixes A :: single_good_auction (* A is the set of all second price auctions. Assuming "second_price_auction A" would merely mean that all elements of A are second price auctions, which is not enough here. *) assumes spa: "rel_all_sga_pred spa_pred A" shows "sga_right_unique A spa_admissible_input spa_equivalent_outcome" proof (rule sga_right_uniqueI) fix N :: "participant set" and b :: bids assume admissible: "spa_admissible_input N b" fix x :: allocation and x' :: allocation and p :: payments and p' :: payments assume "((N, b), (x, p)) \ A" with spa obtain winner::participant where range: "winner \ N \ winner \ arg_max N b" and alloc: "x winner = 1 \ (\ j \ N . j \ winner \ x j = 0)" and pay: "p winner = maximum (N - {winner}) b \ (\j \ N . j \ winner \ p j = 0)" by (rule spa_winner_from_rel) assume "((N, b), (x', p')) \ A" with spa obtain winner'::participant where range': "winner' \ N \ winner' \ arg_max N b" and alloc': "x' winner' = 1 \ (\ j \ N . j \ winner' \ x' j = 0)" and pay': "p' winner' = maximum (N - {winner'}) b \ (\j \ N . j \ winner' \ p' j = 0)" by (rule spa_winner_from_rel) have "b  { i \ N . x i = 1 } = b  { i \ N . x' i = 1 }" (is "?lhs = ?rhs") proof (* CL: any way to collapse these two cases into one? Preferably in Isar style? *) from range alloc range' alloc' show "?lhs \ ?rhs" unfolding arg_max_def by auto next from range' alloc' range alloc show "?rhs \ ?lhs" unfolding arg_max_def by auto qed moreover have "b  { i \ N . p i > 0 } = b  { i \ N . p' i > 0 }" (is "?lhs = ?rhs") proof (* CL: any way to collapse these two cases into one? Preferably in Isar style? *) from admissible range pay range' pay' show "?lhs \ ?rhs" by (rule positive_payment_bids_eq_suff) next from admissible range' pay' range pay show "?rhs \ ?lhs" by (rule positive_payment_bids_eq_suff) qed ultimately show "spa_equivalent_outcome N b x p x' p'" unfolding spa_equivalent_outcome_def .. qed (* TODO CL: merge with fs_spa_well_defined_outcome *) lemma spa_well_defined_outcome : fixes A :: single_good_auction assumes "rel_all_sga_pred spa_pred A" shows "sga_well_defined_outcome A sga_outcome_allocates" using assms unfolding rel_all_sga_pred_def fs_spa_pred'_def using spa_allocates sga_outcome_allocates_def sga_well_defined_outcome_def by (smt prod_caseI2 prod_caseI2') theorem spa_case_check : fixes A :: single_good_auction assumes spa: "rel_all_sga_pred spa_pred A" shows "sga_case_check A spa_admissible_input spa_equivalent_outcome sga_outcome_allocates" proof - from spa have "sga_left_total A spa_admissible_input" by (rule spa_is_left_total) moreover from spa have "sga_right_unique A spa_admissible_input spa_equivalent_outcome" by (rule spa_is_right_unique) moreover from spa have "sga_well_defined_outcome A sga_outcome_allocates" by (rule spa_well_defined_outcome) ultimately show ?thesis unfolding sga_case_check_def by simp qed end