(*
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 {* Second price single good auctions and some of their properties *}
theory SecondPriceAuction
imports SingleGoodAuction Maximum
begin
section {* Payment *}
text{* Same as with the @{text allocation} we now model this as a plain vector. *}
definition vickrey_payment :: "participant set \ payments \ bool"
where "vickrey_payment N p \ (\i \ N . p i \ 0)"
section {* TODO pick a good section title *}
text{* Agent @{text i} being the winner of a second-price auction (see below for complete definition) means
\begin{itemize}
\item he/she is one of the participants with the highest bids
\item he/she wins the auction
\item and pays the maximum price that remains after removing the winner's own bid from the vector of bids.
\end{itemize} *}
definition second_price_auction_winner_outcome ::
"participant set \ bids \ allocation \ payments \ participant \ bool"
where
"second_price_auction_winner_outcome N b x p i \
x i = 1 \ p i = maximum (N - {i}) b"
definition second_price_auction_winner ::
"participant set \ bids \ allocation \ payments \ participant \ bool"
where
"second_price_auction_winner N b x p i \
i \ N \ i \ arg_max N b \
second_price_auction_winner_outcome N b x p i"
text{* Agent @{text i} being a loser of a second-price auction (see below for complete definition) means
\begin{itemize}
\item he/she loses the auction
\item and pays nothing
\end{itemize} *}
definition second_price_auction_loser_outcome ::
"participant set \ allocation \ payments \ participant \ bool"
where "second_price_auction_loser_outcome N x p i \
x i = 0 \
p i = 0"
definition second_price_auction_loser ::
"participant set \ allocation \ payments \ participant \ bool"
where "second_price_auction_loser N x p i \ i \ N \
second_price_auction_loser_outcome N x p i"
definition spa_admissible_input :: "participant set \ bids \ bool"
where "spa_admissible_input N b \ card N > 1 \ bids N b"
text{* A second-price auction is an auction whose outcome satisfies the following conditions:
\begin{enumerate}
\item One of the participants with the highest bids wins. (We do not formalise the random selection of one distinct participants from the set of highest bidders,
in case there is more than one.)
\item The price that the winner pays is the maximum bid that remains after removing the winner's own bid from the vector of bids.
\item The losers do not pay anything.
\end{enumerate} *}
definition spa_pred :: "participant set \ bids \ allocation \ payments \ bool"
where
"spa_pred N b x p \
spa_admissible_input N b \
(\i \ N. i \ arg_max N b \ second_price_auction_winner_outcome N b x p i \
(\j \ N . j \ i \ second_price_auction_loser_outcome N x p j))"
definition second_price_auction :: "single_good_auction \ bool"
where "second_price_auction = rel_sat_sga_pred spa_pred"
text{* definition of a second price auction, projected to the allocation *}
lemma spa_allocation :
fixes N :: "participant set" and b :: bids
and x :: allocation and p :: payments
assumes "spa_pred N b x p"
shows "\ i \ N . x i = 1 \ (\ j \ N . j \ i \ x j = 0)"
using assms
unfolding spa_pred_def second_price_auction_def
second_price_auction_winner_outcome_def
second_price_auction_loser_outcome_def
by auto
lemma sga_pred_imp_lift_to_rel_all:
fixes p q A B
assumes PA: "rel_all_sga_pred p A"
and QB: "rel_all_sga_pred q B"
and p_imp_q: "\ N b x p' . ((N, b), (x, p')) \ A \ p N b x p' \ q N b x p'"
shows "A \ B" using PA QB p_imp_q unfolding rel_all_sga_pred_def by force
text{* Our second price auction (@{text spa_pred}) is well-defined in that its outcome is an allocation. *}
lemma spa_allocates :
fixes N :: "participant set" and b :: bids
and x :: allocation and p :: payments
assumes spa: "spa_pred N b x p"
shows "allocation N x"
proof -
from spa have "card N > 0" unfolding spa_pred_def spa_admissible_input_def by simp
from spa obtain i where i_def: "i \ N \ x i = 1" using spa_allocation by blast
(* the losers' allocations are all 0 *)
with spa have j_def: "\j \ N - {i} . x j = 0" using spa_allocation by (metis member_remove remove_def)
then have "(\ k \ N . x k) = 1"
using `card N > 0` i_def
by (metis (mono_tags) card_ge_0_finite monoid_add_class.add.right_neutral setsum.neutral setsum.remove setsum_infinite)
then show ?thesis unfolding allocation_def non_negative_def le_def zero_def by (smt spa spa_allocation)
qed
text{* definition of a second price auction, projected to the payments *}
lemma spa_payments :
fixes N :: "participant set" and b :: bids
and x :: allocation and p :: payments
assumes "spa_pred N b x p"
shows "\ i \ N . p i = maximum (N - {i}) b \ (\ j \ N . j \ i \ p j = 0)"
using assms
unfolding spa_pred_def second_price_auction_winner_outcome_def second_price_auction_loser_outcome_def
by blast
(* TODO CL: In the general auction case it may make sense to check that the payments (including the seller's payment)
sum up to 0.
*)
text{* Our second price auction (@{text spa_pred}) is well-defined in that its outcome specifies non-negative payments for everyone. *}
lemma spa_vickrey_payment :
fixes N :: "participant set" and b :: bids
and x :: allocation and p :: payments
assumes spa: "spa_pred N b x p"
shows "vickrey_payment N p"
proof -
from spa have card_N: "card N > 1" unfolding spa_pred_def spa_admissible_input_def by simp
then have maximum_defined: "maximum_defined N" unfolding spa_pred_def maximum_defined_def by auto
from spa obtain i where i_range: "i \ N"
and i_pay: "p i = maximum (N - {i}) b"
and losers_pay: "\ j \ N . j \ i \ p j = 0"
using spa_payments by blast
(* Note that if "card N = 1" were allowed, there would be no such k. This seems fine for now,
but in the next step it becomes apparent what we need "card N = 1" and thus this k_def for:
for obtaining the fact `greater`, which talks about the second-highest bid and assumes
that it is defined. *)
from card_N and i_range obtain k where k_def: "k \ N \ k \ i"
using maximum_except_defined maximum_is_component
by (metis Diff_iff insertCI)
with maximum_defined have greater: "maximum (N - {i}) b \ b k" by (rule maximum_except_is_greater_or_equal)
also have "\ \ 0" using spa spa_pred_def second_price_auction_def spa_admissible_input_def bids_def non_negative_def le_def zero_def by (smt greater k_def)
with i_pay and calculation have "p i \ 0" by simp
with i_range and losers_pay have "\ k \ N . p k \ 0" by auto
with vickrey_payment_def show ?thesis ..
qed
lemma spa_is_sga_pred :
fixes N :: "participant set" and b :: bids
and x :: allocation and p :: payments
assumes "spa_pred N b x p"
shows "sga_pred N b x p"
using assms
unfolding spa_pred_def spa_admissible_input_def sga_pred_def by simp
lemma sga_pred_imp_lift_to_rel_sat:
fixes P Q p q A
assumes P_def: "P = rel_sat_sga_pred p"
and Q_def: "Q = rel_sat_sga_pred q"
and PA: "P A"
and p_imp_q: "\ N b x p' . ((N, b), (x, p')) \ A \ p N b x p' \ q N b x p'"
shows "Q A" using PA p_imp_q unfolding P_def Q_def rel_sat_sga_pred_def by blast
lemma spa_is_sga :
fixes A :: single_good_auction
assumes spa: "second_price_auction A"
shows "single_good_auction A"
using second_price_auction_def single_good_auction_def spa spa_is_sga_pred
by (rule sga_pred_imp_lift_to_rel_sat)
lemma spa_allocates_binary :
fixes N :: "participant set" and b :: bids
and x :: allocation and p :: payments
and i :: participant
assumes "spa_pred N b x p"
and "i \ N"
shows "x i = 0 \ x i = 1"
using assms
unfolding spa_pred_def second_price_auction_def second_price_auction_winner_outcome_def second_price_auction_loser_outcome_def
by fast
(*
text{* We chose not to \emph{define} that a second-price auction has only one winner, as it is not necessary. Therefore we have to prove it. *}
(* TODO CL: discuss whether it makes sense to keep this lemma -- it's not used for "theorem vickreyA" but might still be useful for the toolbox *)
lemma second_price_auction_has_only_one_winner:
fixes n::participants and x::allocation and p::payments and b::"real vector"
and winner::participant and j::participant
assumes "second_price_auction n x p"
and "bids n b"
and "second_price_auction_winner n b x p winner"
and "second_price_auction_winner n b x p j"
shows "j = winner"
using assms
unfolding second_price_auction_def second_price_auction_winner_def
using allocation_unique
by blast
*)
text{* The participant who gets the good also satisfies the further properties of a second-price auction winner. *}
lemma allocated_implies_spa_winner:
fixes N :: "participant set" and b :: bids
and x :: allocation and p :: payments
and winner :: participant
assumes "spa_pred N b x p"
and "winner \ N"
and "x winner = 1"
shows "second_price_auction_winner N b x p winner"
using assms
unfolding spa_pred_def second_price_auction_def second_price_auction_winner_def second_price_auction_loser_outcome_def
allocation_def
by (metis zero_neq_one)
(* CL: With the generalised allocation_def, this proof needed a bit more complexity,
as "x winner = 1" implies "x i = 0" for all other participants is rather implicit now. *)
text{* A participant who doesn't gets the good satisfies the further properties of a second-price auction loser. *}
lemma not_allocated_implies_spa_loser:
fixes N :: "participant set" and b :: bids
and x :: allocation and p :: payments
and loser :: participant
assumes spa: "spa_pred N b x p"
and range: "loser \ N"
and loses: "x loser = 0"
shows "second_price_auction_loser N x p loser"
proof -
from loses have "\ second_price_auction_winner N b x p loser"
unfolding second_price_auction_winner_def second_price_auction_winner_outcome_def by simp
with spa range show ?thesis
unfolding spa_pred_def second_price_auction_winner_def second_price_auction_loser_def
by fast
qed
text{* If there is only one bidder with a maximum bid, that bidder wins. *}
lemma only_max_bidder_wins:
fixes N :: "participant set" and max_bidder :: participant
and b :: bids and x :: allocation and p :: payments
assumes defined: "maximum_defined N"
and spa: "spa_pred N b x p"
and range: "max_bidder \ N"
and only_max_bidder: "b max_bidder > maximum (N - {max_bidder}) b"
shows "second_price_auction_winner N b x p max_bidder"
proof -
from spa have spa_unfolded:
"spa_admissible_input N b \ (\i. i \ arg_max N b \ second_price_auction_winner_outcome N b x p i \
(\j \ N. j \ i \ second_price_auction_loser_outcome N x p j))"
unfolding spa_pred_def second_price_auction_def by blast
{
fix j :: participant
assume j_not_max: "j \ N \ j \ max_bidder"
have "j \ arg_max N b"
proof
assume "j \ arg_max N b"
then have maximum: "b j = maximum N b" unfolding arg_max_def by simp
from defined j_not_max range have "b j \ maximum (N - {max_bidder}) b"
using maximum_except_is_greater_or_equal by metis
with only_max_bidder have *: "b j < b max_bidder" by simp
from defined range maximum have "b j \ b max_bidder"
by (simp add: maximum_is_greater_or_equal)
with * show False by simp
qed
}
with spa_unfolded show ?thesis
by (auto simp: second_price_auction_winner_def arg_max_def)
qed
text{* a formula for computing the payoff of the winner of a second-price auction *}
lemma second_price_auction_winner_payoff:
fixes N :: "participant set" and v :: valuations and x :: allocation
and b :: bids and p :: payments and winner :: participant
assumes defined: "maximum_defined N"
and spa: "spa_pred N b x p"
and i_range: "i \ N"
and wins: "x i = 1"
shows "payoff (v i) (x i) (p i) = v i - maximum (N - {i}) b"
proof -
have "payoff (v i) (x i) (p i) = v i - p i"
using wins unfolding payoff_def by simp
also have "\ = v i - maximum (N - {i}) b"
using defined spa i_range wins
using allocated_implies_spa_winner
unfolding second_price_auction_winner_def second_price_auction_winner_outcome_def
by simp
finally show ?thesis .
qed
text{* a formula for computing the payoff of a loser of a second-price auction *}
lemma second_price_auction_loser_payoff:
fixes N :: "participant set" and v :: valuations and x :: allocation
and b :: bids and p :: payments and loser :: participant
assumes "spa_pred N b x p"
and "i \ N"
and "x i = 0"
shows "payoff (v i) (x i) (p i) = 0"
using assms not_allocated_implies_spa_loser
unfolding second_price_auction_loser_def second_price_auction_loser_outcome_def payoff_def
by simp
text{* If a participant wins a second-price auction by not bidding his/her valuation,
the payoff equals the valuation minus the remaining maximum bid. *}
lemma winners_payoff_on_deviation_from_valuation:
fixes N :: "participant set" and v :: valuations and x :: allocation
and b :: bids and p :: payments and winner :: participant
assumes "spa_pred N b x p"
and "i \ N"
and "x i = 1"
and "maximum_defined N"
shows "payoff (v i) (x i) (p i) = v i - maximum (N - {i}) (b(i := v i))"
using assms second_price_auction_winner_payoff remaining_maximum_invariant
by metis
end