# Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions

```I've had a look at your work, and found it interesting.

One thing that I noticed was that you defined what it means to be a
second_price_auction, and you proved various things about functions that
satisfy this definition, but you never showed that the definition was
satisfiable.

This isn't an inconsequential detail; at first, I thought you'd got the
definition wrong, and that "second_price_auction n x p" implied n < 2.
When I tried to prove it, I finally noticed that your allocation and
payment functions depend on the set of bids.  But it is easy to write
definitions that aren't satisfiable, or that imply trivialities.

So I decided to prove that your second_price_auction was satisfiable for
n > 0.  See attached for the proof.

Also, you made a comment about removing an element from a set.  Given a
set A, the set of all the elements of A except x can be written as
"A - {x}"

I have a feeling that there was something else I was going to comment
on, but I should go and have lunch, and write again if I remember it.

Tim
<><
```
```header {* Specific allocation and payment functions satisfying the requirements of a
second-price auction *}

theory Vickrey_Extras
imports Vickrey
begin

subsection {* More about @{const maximum_except} *}

lemma maximum_except_non_negative: "maximum_except n b i \<ge> 0"
proof (cases n)
case 0
thus "maximum_except n b i \<ge> 0" unfolding maximum_except_def by simp
next
case (Suc m)
with maximum_non_negative
show "maximum_except n b i \<ge> 0" unfolding maximum_except_def by simp
qed

subsection {* Choice of highest bidder *}

definition highest_bidder :: "participants \<Rightarrow> real_vector \<Rightarrow> participant" where
"highest_bidder n b \<equiv> \<some> i. in_range n i \<and> maximum n b = b i"

lemma highest_bidder_is_maximum:
assumes "n > 0" and "bids n b"
shows "in_range n (highest_bidder n b)" and "maximum n b = b (highest_bidder n b)"
proof -
from assms and maximum_is_component
have "\<exists> i. in_range n i \<and> maximum n b = b i" unfolding bids_def by simp
hence "in_range n (highest_bidder n b) \<and> maximum n b = b (highest_bidder n b)"
unfolding highest_bidder_def by (rule someI_ex)
thus "in_range n (highest_bidder n b)" and "maximum n b = b (highest_bidder n b)"
by simp_all
qed

lemma highest_bidder_in_arg_max_set:
assumes "n > 0" and "bids n b"
shows "highest_bidder n b \<in> arg_max_set n b"
unfolding arg_max_set_def
using assms and highest_bidder_is_maximum
by simp

subsection {* Allocation where the highest bidder wins *}

definition highest_bidder_wins :: "participants \<Rightarrow> allocation" where
"highest_bidder_wins n b i \<equiv> if i = highest_bidder n b then True else False"

lemma highest_bidder_wins_is_allocation:
assumes "n > 0" and "bids n b"
shows "allocation n b (highest_bidder_wins n)"
proof -
from assms have "in_range n (highest_bidder n b)" by (rule highest_bidder_is_maximum)
with `bids n b` show "allocation n b (highest_bidder_wins n)"
unfolding allocation_def and highest_bidder_wins_def by simp
qed

subsection {* Second-price payments *}

definition second_price_payments :: "participants \<Rightarrow> payments" where
"second_price_payments n b i
\<equiv> if i = highest_bidder n b then maximum_except n b i else 0"

lemma second_price_payments_non_negative:
"vickrey_payment n b (second_price_payments n)"
unfolding vickrey_payment_def and second_price_payments_def
using maximum_except_non_negative
by simp

subsection {* @{const highest_bidder_wins} and @{const second_price_payments}
satisfy @{const second_price_auction} *}

lemma highest_bidder_second_price_auction_winner:
assumes "n > 0" and "bids n b"
shows "second_price_auction_winner n b (highest_bidder_wins n)
(second_price_payments n) (highest_bidder n b)"
proof -
from assms
have "in_range n (highest_bidder n b)" by (rule highest_bidder_is_maximum)

from assms
have "highest_bidder n b \<in> arg_max_set n b" by (rule highest_bidder_in_arg_max_set)
with `in_range n (highest_bidder n b)`
show ?thesis
unfolding second_price_auction_winner_def
and highest_bidder_wins_def
and second_price_payments_def
by simp
qed

lemma other_bidders_second_price_auction_loser:
assumes "in_range n i" and "i \<noteq> highest_bidder n b"
shows "second_price_auction_loser n b (highest_bidder_wins n)
(second_price_payments n) i"
unfolding second_price_auction_loser_def
and highest_bidder_wins_def
and second_price_payments_def
using assms
by simp

theorem second_price_auction_example:
assumes "n > 0"
shows "second_price_auction n (highest_bidder_wins n) (second_price_payments n)"
proof -
{ fix b
assume "bids n b"
with `n > 0`
have "allocation n b (highest_bidder_wins n)"
by (rule highest_bidder_wins_is_allocation)

from `n > 0` and `bids n b`
have "in_range n (highest_bidder n b)" by (rule highest_bidder_is_maximum)

from `n > 0` and `bids n b`
have "second_price_auction_winner n b (highest_bidder_wins n)
(second_price_payments n) (highest_bidder n b)"
by (rule highest_bidder_second_price_auction_winner)
with `in_range n (highest_bidder n b)` and other_bidders_second_price_auction_loser
have "\<exists> i. in_range n i
\<and> second_price_auction_winner n b (highest_bidder_wins n)
(second_price_payments n) i
\<and> (\<forall> j. in_range n j \<and> j \<noteq> i
\<longrightarrow> second_price_auction_loser n b (highest_bidder_wins n)
(second_price_payments n) j)"
by (simp add: exI [of _ "highest_bidder n b"])
note `allocation n b (highest_bidder_wins n)`
and second_price_payments_non_negative [of n b]
and this
}
thus "second_price_auction n (highest_bidder_wins n) (second_price_payments n)"
unfolding second_price_auction_def
by simp
qed

theorem second_price_auction_example_equilibrium_weakly_dominant:
assumes "n > 0" and "valuation n v"
shows "equilibrium_weakly_dominant_strategy n v v
(highest_bidder_wins n) (second_price_payments n)"
proof -
from `n > 0`
have "second_price_auction n (highest_bidder_wins n) (second_price_payments n)"
by (rule second_price_auction_example)
with `valuation n v`
show "equilibrium_weakly_dominant_strategy n v v
(highest_bidder_wins n) (second_price_payments n)"
by (rule vickreyA)
qed

theorem second_price_auction_example_efficient:
assumes "n > 0" and "valuation n v"
shows "efficient n v v (highest_bidder_wins n)"
proof -
from `n > 0`
have "second_price_auction n (highest_bidder_wins n) (second_price_payments n)"
by (rule second_price_auction_example)
with `valuation n v`
show "efficient n v v (highest_bidder_wins n)" by (rule vickreyB)
qed

end```

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.