*To*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Subject*: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Thu, 01 Nov 2012 15:07:10 +1300*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, formare-management at cs.bham.ac.uk*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121028 Thunderbird/16.0.2

> We would like to contribute our formalisation to the AFP, but are unsure about the procedure: once accepted and published, can we submit updates? Yes; see http://afp.sourceforge.net/updating.shtml > * It would be nice to be able to introduce proper types (not just type_synonyms) for things such as non-negative real vectors. Have you seen section 8.5.2 of tutorial.pdf in Isabelle's doc folder? Perhaps there's also other documentation in another file; if so, I hope someone else knows where and points you to it. I'm quite interested in what you're doing; after working with Isabelle for my Master's project, I'm now musing about auction theory: http://wp.me/p2IaW7-W (I'm not trained in economics, so please be gentle, but please do comment on my musings if you think I'm in error, or if you have anything else to say about them.) Consequently, I decided to have a look at your Vickrey theory. In preparation for this, I tried running Isabelle's document preparation system on Vickrey.thy (see chapter 4 of isar-ref.pdf, and possibly other parts of Isabelle's documentation). Unfortunately, it didn't work at first, for a couple of reasons. First, Vickrey.thy didn't end with "end", which was easy to fix. Second, your "text {* ... *}" portions don't always contain valid LaTeX. I made minimal changes to get your document to compile, but I haven't had time to read it yet. I've attached my edited version of your Vickrey.thy, so you can see what changes I've made. I've made almost no effort to make it look as you intended --- only to make it compile. Tim <><

(* TODO CL: ask whether jEdit's Isabelle mode disables word wrapping *) (* TODO CL: report Isabelle/jEdit bug: no auto-indentation *) (* TODO CL: report Isabelle/jEdit bug: when I set long lines to wrap at window boundary, wrapped part behaves badly: not editable *) (* TODO CL: report Isabelle/jEdit bug: can't copy goal in output pane to clipboard *) header {* Vickrey's Theorem: Second price auctions support an equilibrium in weakly dominant strategies, and are efficient, if each participant bids their valuation of the good. *} (* Authors: * Manfred Kerber <m.kerber at cs.bham.ac.uk> * Christoph Lange <c.lange at cs.bham.ac.uk> * Colin Rowat <c.rowat at bham.ac.uk> 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) *) theory Vickrey imports Main Real begin section{* Introduction *} text{* In second price (or Vickrey) auctions, bidders submit sealed bids; the highest bidder wins, and pays the highest bid of the \emph{remaining} bids; the losers pay nothing. (See \url{http://en.wikipedia.org/wiki/Vickrey_auction} for more information, including a discussion of variants used by eBay, Google and Yahoo!.) Vickrey proved that 'truth-telling' (i.e. submitting a bid equal to one's actual valuation of the good) was a weakly dominant strategy. This means that no bidder could do strictly better by bidding above or below its valuation \emph{whatever} the other bidders did. Thus, the auction is also efficient, awarding the item to the bidder with the highest valuation. Vickrey was awarded Economics' Nobel prize in 1996 for his work. High level versions of his theorem, and 12 others, were collected in Eric Maskin's 2004 review of Paul Milgrom's influential book on auction theory ("The unity of auction theory: Milgrom's master class", Journal of Economic Literature, 42(4), pp. 1102--1115). Maskin himself won the Nobel in 2007. *} section{* Preliminaries *} text{* some types defined for our convenience *} type_synonym bool_vector = "nat \<Rightarrow> bool" type_synonym real_vector = "nat \<Rightarrow> real" type_synonym participant = "nat" (* ordinal number *) type_synonym participants = "nat" (* cardinal number *) text{* TODO CL: discuss whether it's intuitive to name some types as in the following lines. However, being of one such type does not yet imply well-formedness; e.g. we could have an x::allocation, which, for some given n and b does not satisfy "allocation n b x". *} type_synonym allocation = "real_vector \<Rightarrow> participants \<Rightarrow> bool" type_synonym payments = "real_vector \<Rightarrow> participants \<Rightarrow> real" (* a payment vector is a function of a real_vector of bids *) subsection{* some range checks for vectors *} text{* To ease writing, we introduce a predicate for the range of participants. *} definition in_range :: "nat \<Rightarrow> nat \<Rightarrow> bool" where "in_range n i \<equiv> 1 \<le> i \<and> i \<le> n" text{* we could also, in a higher-order style, generally define a vector whose components satisfy a predicate, and then parameterize this predicate with $\geq 0$ and $> 0$*} definition non_negative_real_vector :: "nat \<Rightarrow> real_vector \<Rightarrow> bool" where "non_negative_real_vector n v \<equiv> \<forall> i::nat . in_range n i \<longrightarrow> v i \<ge> 0" definition positive_real_vector :: "nat \<Rightarrow> real_vector \<Rightarrow> bool" where "positive_real_vector n v \<equiv> \<forall> i::nat . in_range n i \<longrightarrow> v i > 0" section{* Deviation from a vector *} text{* We define a function that modifies a vector by using an alternative value for a given component. *} definition deviation :: "nat \<Rightarrow> real_vector \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real" where "deviation n bid alternative_value index j \<equiv> if j = index then alternative_value else bid j" text{* We define a function that, given one vector and an alternative one (in practice these will be strategy profiles), and a participant index i, returns a vector that has component i changed to the alternative value (i.e. in practice: the bid of participant i changed), whereas the others keep their original values. Actually this definition doesn't check whether its arguments are non-negative real vectors (i.e. well-formed strategy profiles). *} (* NOTE CL: I changed the order of arguments compared to our original Theorema attempts, as I think this one is more intuitive. TODO CL: ask whether there a way of writing the alternative as b_hat, as it looks in the paper version? TODO CL: discuss whether there any useful way we could use n for range-checking? Or don't we need n at all? *) definition deviation_vec :: "nat \<Rightarrow> real_vector \<Rightarrow> real_vector \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real" where "deviation_vec n bid alternative_vec index \<equiv> deviation n bid (alternative_vec index) index" (* the old component-wise definition had an error actually: "deviation_vec n bid alternative_vec index j \<equiv> deviation n bid (alternative_vec j) index j" ^^ should have been index so actually a component-wise definition was not necessary the error didn't cause trouble because of the "j = index" condition in deviation_def, but it prevented us from rewriting deviation_def into deviation without providing a component index, i.e. in curried form. The latter was desired after introducing remaining_maximum_invariant (which uses the more general "deviation" form instead of "deviation_vec") *) section{* Strategy (bids) *} text{* Strategy and strategy profile (the vector of the strategies of all participants) are not fully defined below. We ignore the distribu- tion and density function, as they do not play a role in the proof of the theorem. So, for now, we do not model the random mapping from a participant's valuation to its bid, but simply consider its bid as a non- negative number that doesn't depend on anything. *} definition bids :: "participants \<Rightarrow> real_vector \<Rightarrow> bool" where "bids n b \<equiv> non_negative_real_vector n b" subsection{* Deviation from a bid *} text{* A deviation from a bid is still a well-formed bid. *} lemma deviated_bid_well_formed : fixes n::participants and bid::real_vector and alternative_vec::real_vector and i::participant assumes bids_original: "bids n bid" and bids_alternative: "bids n alternative_vec" shows "bids n (deviation_vec n bid alternative_vec i)" proof - let ?dev = "deviation_vec n bid alternative_vec i" have "\<forall> k::participant . in_range n k \<longrightarrow> ?dev k \<ge> 0" proof fix k::participant show "in_range n k \<longrightarrow> ?dev k \<ge> 0" proof assume k_range: "in_range n k" show "?dev k \<ge> 0" proof (cases "?dev k = bid k") case True with k_range and bids_original show ?thesis unfolding deviation_def by (simp add: bids_def non_negative_real_vector_def) next case False then have "?dev k = alternative_vec k" by (auto simp add: deviation_vec_def deviation_def) (* "then" \<equiv> "from this", where "this" is the most recently established fact; note that in line with https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-October/msg00057.html and for easier general comprehensibility we are not using the abbreviations "hence" \<equiv> "then have" and "thus" \<equiv> "then show" here. *) with k_range and bids_alternative show ?thesis unfolding deviation_def by (simp add: bids_def non_negative_real_vector_def) qed qed qed then show ?thesis unfolding bids_def non_negative_real_vector_def . qed text{* A single-good auction is a mechanism specified by a function that maps a strategy profile to an outcome. *} section{* Allocation *} text{* A function x, which takes a vector of n bids, is an allocation if it returns True for one bidder and False for the others. *} (* TODO CL: discuss whether we should use different names for "definition allocation" and "type_synonym allocation", as they denote two different things *) (* TODO CL: record in our notes that the order of arguments of a function matters. Note that I, CL, reordered the arguments on 2012-08-24. When using the function x in a curried way, we can speak of (x b) as a vector of booleans, in a very straightforward way; with a different order of arguments we'd have to use (\<lambda> index::nat . x index b). *) definition allocation :: "participants \<Rightarrow> real_vector \<Rightarrow> allocation \<Rightarrow> bool" where "allocation n b x \<equiv> bids n b \<and> (\<exists>k:: participant. in_range n k \<and> x b k \<and> (\<forall>j:: participant. j\<noteq>k \<longrightarrow> \<not>x b j))" text{* An allocation function uniquely determines the winner. *} lemma allocation_unique : fixes n::participants and x::allocation and b::real_vector and winner::participant assumes allocation: "allocation n b x" and winner: "x b winner" shows "\<forall>j::participant. x b j \<longrightarrow> j = winner" by (metis allocation allocation_def winner) subsection{* Sample lemma: The allocation, in which the first participant wins (whatever the bids) is an allocation. *} definition all_bid_1 :: "real_vector" where "all_bid_1 \<equiv> \<lambda>x.1" lemma bid_all_bid_1: shows "bids 1 all_bid_1" apply(unfold bids_def all_bid_1_def) apply(unfold non_negative_real_vector_def) apply(auto) done definition first_wins :: "allocation" where "first_wins _ i \<equiv> i = 1" (* whatever the bids, the first participant wins *) (* for testing lemma only_wins_is_allocation: shows "allocation 1 all_bid_1 first_wins" apply(unfold allocation_def) apply(unfold first_wins_def) apply(blast) done *) (* TODO CL: note that this is a more tactic-free syntax; I think here it doesn't really make sense to write down explicit proof steps. *) lemma only_wins_is_allocation_declarative: shows "allocation 1 all_bid_1 first_wins" unfolding allocation_def and in_range_def and first_wins_def using bid_all_bid_1 by blast section{* Payment *} text{* Each participant pays some amount. *} definition vickrey_payment :: "participants \<Rightarrow> real_vector \<Rightarrow> payments \<Rightarrow> bool" where "vickrey_payment n b p \<equiv> \<forall>i:: participant. in_range n i \<longrightarrow> p b i \<ge> 0" section{* Outcome *} text{* The outcome of an auction is specified an allocation $\{0, 1\}^n$ and a vector of payments $R^n$ made by each participant; we don't introduce a dedicated definition for this. *} section{* Valuation *} text{* Each participant has a positive valuation of the good. *} definition valuation :: "participants \<Rightarrow> real_vector \<Rightarrow> bool" where "valuation n v \<equiv> \<forall>i:: participant. in_range n i \<longrightarrow> v i > 0" text{* Any well-formed valuation vector is a well-formed bid vector *} lemma valuation_is_bid : fixes n::participants and v::real_vector assumes "valuation n v" shows "bids n v" (* Sledgehammer finds a proof by (metis assms bids_def non_negative_real_vector_def order_less_imp_le valuation_def) but we prefer manual Isar style here. *) proof - have bids_def_unfolded: "\<forall>i:: participant. in_range n i \<longrightarrow> v i \<ge> 0" proof fix i::participant show "in_range n i \<longrightarrow> v i \<ge> 0" proof assume "in_range n i" with assms have "v i > 0" unfolding valuation_def by simp then show "v i \<ge> 0" by simp (* If we had been searching the library for an applicable theorem, we could have used find_theorems (200) "_ > _ \<Longrightarrow> _ \<ge> _" where 200 is some upper search bound, and would have found less_imp_le *) qed qed show ?thesis using bids_def_unfolded unfolding bids_def non_negative_real_vector_def by simp qed section{* Payoff *} text{* The payoff of the winner $(x_i=1)$, determined by a utility function u, is the difference between its valuation and the actual payment. For the losers, it is the negative payment. *} (* TODO CL: ask whether there is a built-in function that converts bool to {0,1} *) definition payoff :: "real \<Rightarrow> bool \<Rightarrow> real \<Rightarrow> real" where "payoff Valuation Allocation Payment \<equiv> Valuation * (if Allocation then 1 else 0) - Payment" (* for testing *) value "payoff 5 True 2" (* I ascribed the value 5 to the good, won the auction, and had to pay 2. *) text{* For convenience in the subsequent formalisation, we also define the payoff as a vector, component-wise. *} definition payoff_vector :: "real_vector \<Rightarrow> bool_vector \<Rightarrow> real_vector \<Rightarrow> participant \<Rightarrow> real" where "payoff_vector v concrete_x concrete_p i \<equiv> payoff (v i) (concrete_x i) (concrete_p i)" section{* Maximum and related functions *} text{* The maximum component value of a vector y of non-negative reals 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: 1. The maximum component value is equal to the value of one of the components 2. maximum\_is\_greater\_or\_equal Here, we derive those two statements as lemmas from the definition of the computable function. *} primrec maximum :: "nat \<Rightarrow> real_vector \<Rightarrow> real" where "maximum 0 _ = 0" | "maximum (Suc n) y = max 0 (max (maximum n y) (y (Suc n)))" (* we don't enforce that y is non-negative, but this computation only makes sense for a non-negative y *) text{* If two vectors are equal, their maximum components are equal too *} lemma maximum_equal : fixes n::nat and y::real_vector and z::real_vector shows "(\<forall>i::nat . in_range n i \<longrightarrow> y i = z i) \<longrightarrow> maximum n y = maximum n z" proof (induct n) case 0 show ?case by simp next case (Suc n) show ?case proof assume assms: "\<forall>i::nat . in_range (Suc n) i \<longrightarrow> y i = z i" then have equal_so_far: "maximum n y = maximum n z" by (simp add: Suc.hyps le_SucI in_range_def) from assms have equal_here: "y (Suc n) = z (Suc n)" using Suc.hyps by (metis Suc_eq_plus1 le_add2 le_refl in_range_def) with equal_so_far show "maximum (Suc n) y = maximum (Suc n) z" unfolding maximum_def by (simp add: Suc.hyps) qed qed text{* The maximum component, as defined above, is non-negative *} lemma maximum_non_negative : fixes n::nat and y::real_vector shows "maximum n y \<ge> 0" proof (induct n) case 0 show ?case by simp next case (Suc n) have "maximum (Suc n) y = max 0 (max (maximum n y) (y (Suc n)))" unfolding maximum_def by simp also have "\<dots> \<ge> 0" by auto finally show ?case . 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::nat and y::real_vector shows "\<forall> i::nat . in_range n i \<longrightarrow> maximum n y \<ge> y i" proof (induct n) case 0 show ?case by (simp add: in_range_def) next case (Suc n) show ?case (* This is a shorter alternative to first proving have "\<forall> i::nat . in_range (Suc n) i \<longrightarrow> maximum (Suc n) y \<ge> y i" and then trivially showing ?case *) proof fix i::nat show "in_range (Suc n) i \<longrightarrow> maximum (Suc n) y \<ge> y i" proof assume 1: "in_range (Suc n) i" have "max (maximum n y) (y (Suc n)) \<ge> y i" (* TODO CL: ask whether there is a way of automatically decomposing the initial goal until we arrive at this expression *) proof (cases "i = Suc n") case True then show ?thesis by (simp add: le_max_iff_disj) next case False with 1 (* TODO CL: ask whether there is a nicer way to write this, without having to number assumption 1 *) have "in_range n i" by (simp add: less_eq_Suc_le in_range_def) then have "maximum n y \<ge> y i" by (simp add: Suc.hyps) then show ?thesis by (simp add: le_max_iff_disj) qed then show "maximum (Suc n) y \<ge> y i" unfolding maximum_def by simp qed qed qed text{* The maximum component is one component *} lemma maximum_is_component : fixes n::nat and y::real_vector shows "n > 0 \<and> non_negative_real_vector n y \<longrightarrow> (\<exists> i::nat . in_range n i \<and> maximum n y = y i)" (* reuse for "Suc n" inside proof didn't work when declaring premise with "assumes" *) proof (induct n) case 0 show ?case by simp next case (Suc n) show ?case proof assume non_negative: "(Suc n) > 0 \<and> non_negative_real_vector (Suc n) y" show "\<exists> i::nat . in_range (Suc n) i \<and> maximum (Suc n) y = y i" proof (cases "y (Suc n) \<ge> maximum n y") case True from non_negative have "y (Suc n) \<ge> 0" unfolding in_range_def non_negative_real_vector_def by simp with True have "y (Suc n) = max 0 (max (maximum n y) (y (Suc n)))" by simp also have "\<dots> = maximum (Suc n) y" unfolding maximum_def by simp finally have "y (Suc n) = maximum (Suc n) y" . then show ?thesis using in_range_def by auto next case False have hyp: "n > 0 \<and> non_negative_real_vector n y \<longrightarrow> (\<exists> i::nat . in_range n i \<and> maximum n y = y i)" by (rule Suc.hyps) have non_empty: "n > 0" proof - (* by contradiction *) { assume "n = 0" with False and non_negative have "y (Suc n) = maximum n y" unfolding non_negative_real_vector_def maximum_def in_range_def by simp with False have "False" by simp } then show "n > 0" by blast qed from non_negative have pred_non_negative: "non_negative_real_vector n y" unfolding non_negative_real_vector_def in_range_def by simp with non_empty and hyp obtain i::nat where pred_max: "in_range n i \<and> maximum n y = y i" by auto with non_negative have y_i_non_negative: "0 \<le> y i" unfolding non_negative_real_vector_def in_range_def by simp have "y i = maximum n y" using pred_max by simp also have "\<dots> = max (maximum n y) (y (Suc n))" using False by simp (* TODO CL: ask for the difference between "from" and "using" (before/after goal). In any case I got the impression that "with \<dots> also have" breaks the chain of calculational reasoning. *) also have "\<dots> = max 0 (max (maximum n y) (y (Suc n)))" using non_negative and y_i_non_negative by (auto simp add: calculation min_max.le_iff_sup) also have "\<dots> = maximum (Suc n) y" unfolding maximum_def using non_empty by simp finally have max: "y i = maximum (Suc n) y" . from pred_max have "in_range (Suc n) i" by (simp add: in_range_def) with max show ?thesis by auto qed qed 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::nat and y::real_vector and m::real shows "non_negative_real_vector n y \<and> n > 0 \<and> (\<forall> i::nat . in_range n i \<longrightarrow> m \<ge> y i) \<and> (\<exists> i::nat . in_range n i \<and> m = y i) \<longrightarrow> m = maximum n y" proof (induct n) case 0 show ?case by simp next case (Suc n) show ?case proof assume assms: "non_negative_real_vector (Suc n) y \<and> Suc n > 0 \<and> (\<forall> i::nat . in_range (Suc n) i \<longrightarrow> m \<ge> y i) \<and> (\<exists> i::nat . in_range (Suc n) i \<and> m = y i)" (* now break this down into its conjunctives *) from assms have non_negative: "non_negative_real_vector (Suc n) y" .. (* ".." means: apply a canonical rule for the current context *) from assms have non_empty: "Suc n > 0" by simp from assms have greater_or_equal: "\<forall> i::nat . in_range (Suc n) i \<longrightarrow> m \<ge> y i" by simp from assms have is_component: "\<exists> i::nat . in_range (Suc n) i \<and> m = y i" by simp (* further preliminaries *) from non_negative have pred_non_negative: "non_negative_real_vector n y" unfolding non_negative_real_vector_def in_range_def by simp (* then go on *) from non_empty have max_def: "maximum (Suc n) y = max 0 (max (maximum n y) (y (Suc n)))" unfolding maximum_def by simp also have "\<dots> = m" proof (cases "n = 0") case True with is_component have m_is_only_component: "m = y 1" unfolding in_range_def by auto with non_negative have "m \<ge> 0" unfolding non_negative_real_vector_def in_range_def by simp (* we could break this down into further textbook-style steps, but their proofs turn out to be ugly as well, so we leave it at this high level *) then have "max 0 (max (maximum 0 y) (y 1)) = m" by (auto simp add: m_is_only_component) with True show ?thesis by auto (* this was (metis One_nat_def), but auto has access to simplification rules by default *) next case False show ?thesis proof cases assume last_is_max: "y (Suc n) = m" have "\<dots> \<ge> maximum n y" proof - from False and pred_non_negative and maximum_is_component have "\<exists> k::nat . in_range n k \<and> maximum n y = y k" by auto then obtain k::nat where "in_range n k \<and> maximum n y = y k" by auto with greater_or_equal show ?thesis unfolding in_range_def by (simp add: le_Suc_eq) (* TODO CL: ask whether we should have kept using metis here. Sledgehammer always suggests metis. When auto or simp also works (which is the case here, but not always), is is more efficient? *) qed then show ?thesis using last_is_max by (metis less_max_iff_disj linorder_not_le maximum_non_negative min_max.sup_absorb1 min_max.sup_commute) next assume "y (Suc n) \<noteq> m" with is_component have pred_is_component: "\<exists>k::nat . in_range n k \<and> m = y k" unfolding in_range_def by (metis le_antisym not_less_eq_eq) from greater_or_equal have "\<forall>k::nat . in_range n k \<longrightarrow> m \<ge> y k" unfolding in_range_def by simp (* these, plus pred_non_negative, form the left hand side of the induction hypothesis *) then have "m = maximum n y" by (metis False Suc gr0I pred_is_component pred_non_negative) then show ?thesis using in_range_def by (metis Suc_eq_plus1 greater_or_equal le_refl maximum_non_negative min_max.sup_absorb1 min_max.sup_absorb2 not_add_less2 not_leE) qed qed finally show "m = maximum (Suc n) y" .. qed qed (* 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 *) text{* Increasing the (actually: a) maximum component value keeps it the maximum. *} lemma increment_keeps_maximum : fixes n::nat and y::real_vector and y'::real_vector and max_index::nat and max::real and max'::real shows "non_negative_real_vector n y \<and> n > 0 \<and> in_range n max_index \<and> maximum n y = y max_index \<and> y max_index < max' \<and> y' = (\<lambda> i::nat . if i = max_index then max' else y i) \<longrightarrow> maximum n y' = y' max_index" proof assume assms: "non_negative_real_vector n y \<and> n > 0 \<and> in_range n max_index \<and> maximum n y = y max_index \<and> y max_index < max' \<and> y' = (\<lambda> i::nat . if i = max_index then max' else y i)" (* now break this down into its conjunctives *) from assms have non_negative: "non_negative_real_vector n y" by simp from assms have non_empty: "n > 0" by simp from assms have index_range: "in_range n max_index" by simp from assms have old_maximum: "maximum n y = y max_index" by simp from assms have new_lt: "y max_index < max'" by simp from assms have increment: "y' = (\<lambda> i::nat . if i = max_index then max' else y i)" by simp (* now go on *) then have new_component: "y' max_index = max'" by simp from non_negative and index_range and new_lt have "\<dots> \<ge> 0" unfolding non_negative_real_vector_def by (auto simp add: linorder_not_less order_less_trans) with non_negative and increment have new_non_negative: "non_negative_real_vector n y'" unfolding non_negative_real_vector_def by simp from old_maximum and new_lt and increment have greater_or_equal: "\<forall> i::nat . in_range n i \<longrightarrow> max' \<ge> y' i" by (metis linorder_not_less maximum_is_greater_or_equal order_less_trans order_refl) from increment have "max' = y' max_index" by simp (* now we have all prerequisites for applying maximum_sufficient *) with new_non_negative and non_empty and greater_or_equal and index_range show "maximum n y' = y' max_index" using maximum_sufficient by metis qed text{* a test vector whose maximum component value we determine *} value "maximum 2 (\<lambda> x::nat . 1)" value "maximum 5 (\<lambda> x::nat . x)" text{* We define the set of maximal components of a vector y: *} (* TODO CL: discuss whether we should define this in a computable way. If so, how? *) (* TODO CL: discuss whether this function should return a set, or a vector. How to construct such a vector? Or should we define it as a predicate? *) definition arg_max_set :: "nat \<Rightarrow> real_vector \<Rightarrow> (nat set)" where "arg_max_set n b \<equiv> {i. in_range n i \<and> maximum n b = b i}" (* for testing *) lemma test_arg_max_set: shows "{1,2} \<subseteq> arg_max_set 3 (\<lambda>x. if x < 3 then 100 else 0)" (* the 1st and 2nd elements in a vector [100,100,\<dots>] are maximal. *) apply(unfold arg_max_set_def in_range_def) apply(simp add: maximum_def) done text{* an alternative proof of the same lemma --- still too trivial to test how declarative proofs \emph{actually} work *} lemma test_arg_max_set_declarative: shows "{1,2} \<subseteq> arg_max_set 3 (\<lambda>x. if x < 3 then 100 else 0)" (* the 1st and 2nd elements in a vector [100,100,\<dots>] are maximal. *) unfolding arg_max_set_def in_range_def by (simp add: maximum_def) text{* constructing a new vector from a given one, by skipping one component *} definition skip_index :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> 'a)" where "skip_index vector index = (\<lambda> i::nat . vector (if i < index then i else Suc i))" text{* skipping one component in a non-negative vector keeps it non-negative *} (* TODO CL: discuss whether we should actually prove the more general lemma that skipping one component in a vector whose components each satisfy p still satisfies p (for a suitable p) *) lemma skip_index_keeps_non_negativity : fixes n::nat and v::real_vector assumes non_empty: "n > 0" and non_negative: "non_negative_real_vector n v" shows "\<forall>i::nat . in_range n i \<longrightarrow> non_negative_real_vector (n-(1::nat)) (skip_index v i)" proof fix i::nat show "in_range n i \<longrightarrow> non_negative_real_vector (n-(1::nat)) (skip_index v i)" proof assume "in_range n i" have "\<forall>j::nat. in_range (n-(1::nat)) j \<longrightarrow> (skip_index v i) j \<ge> 0" proof fix j::nat show "in_range (n-(1::nat)) j \<longrightarrow> (skip_index v i) j \<ge> 0" proof assume j_range: "in_range (n-(1::nat)) j" show "(skip_index v i) j \<ge> 0" proof (cases "j < i") case True then have "(skip_index v i) j = v j" unfolding skip_index_def by simp with j_range and non_negative show ?thesis unfolding non_negative_real_vector_def in_range_def by (auto simp add: leD less_imp_diff_less not_leE) next case False then have "(skip_index v i) j = v (Suc j)" unfolding skip_index_def by simp with j_range and non_negative show ?thesis unfolding non_negative_real_vector_def in_range_def by (auto simp add: leD less_imp_diff_less not_leE) qed qed qed then show "non_negative_real_vector (n-(1::nat)) (skip_index v i)" unfolding non_negative_real_vector_def by simp qed qed text{* when two vectors differ in one component, skipping that component makes the vectors equal *} lemma equal_by_skipping : fixes n::nat and v::real_vector and w::real_vector and j::nat assumes non_empty: "n > 0" and j_range: "in_range n j" and equal_except: "\<forall>i::nat . in_range n i \<and> i \<noteq> j \<longrightarrow> v i = w i" shows "\<forall>k::nat . in_range (n-(1::nat)) k \<longrightarrow> (skip_index v j) k = (skip_index w j) k" proof fix k::nat show "in_range (n-(1::nat)) k \<longrightarrow> (skip_index v j) k = (skip_index w j) k" proof assume k_range: "in_range (n-(1::nat)) k" show "(skip_index v j) k = (skip_index w j) k" proof (cases "k < j") case True then have "(skip_index v j) k = v k" and "(skip_index w j) k = w k" unfolding skip_index_def by auto with equal_except and k_range and True show ?thesis using in_range_def by (metis diff_le_self le_trans less_not_refl) next case False then have "(skip_index v j) k = v (Suc k)" and "(skip_index w j) k = w (Suc k)" unfolding skip_index_def by auto with equal_except and k_range and False show ?thesis using in_range_def by (metis One_nat_def diff_0_eq_0 diff_Suc_Suc diff_less le_neq_implies_less lessI less_imp_diff_less linorder_not_less not_less_eq_eq) qed qed qed text{* We define the maximum component value that remains after removing the i-th component from the non-negative real vector y: *} (* TODO CL: discuss whether we can, or should, enforce that j is \<le> n *) (* TODO CL: ask whether there is an easier or more efficient way of stating this *) primrec maximum_except :: "nat \<Rightarrow> real_vector \<Rightarrow> nat \<Rightarrow> real" where "maximum_except 0 _ _ = 0" | "maximum_except (Suc n) y j = maximum n (skip_index y j)" (* we take y but skip its j-th component *) (* for testing *) value "maximum_except 3 (\<lambda> x::nat . 4-x) 1" (* the maximum component value of the vector [3,2,1], except the first element, is 2 *) 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::nat and y::real_vector and j::nat shows "n \<ge> 1 \<and> in_range n j \<longrightarrow> (\<forall> i::nat . in_range n i \<and> i \<noteq> j \<longrightarrow> maximum_except n y j \<ge> y i)" proof assume j_range: "n \<ge> 1 \<and> in_range n j" show "\<forall>i::nat. in_range n i \<and> i \<noteq> j \<longrightarrow> maximum_except n y j \<ge> y i" proof fix i::nat show "in_range n i \<and> i \<noteq> j \<longrightarrow> maximum_except n y j \<ge> y i" proof let ?y_with_j_skipped = "skip_index y j" from j_range obtain pred_n where pred_n: "n = Suc pred_n" by (metis not0_implies_Suc not_one_le_zero) (* wouldn't work with simp or rule alone *) assume i_range: "in_range n i \<and> i \<noteq> j" then show "maximum_except n y j \<ge> y i" proof (cases "i < j") case True then have can_skip_j: "y i = ?y_with_j_skipped i" unfolding skip_index_def by simp from True and j_range and i_range and pred_n have "in_range pred_n i" unfolding in_range_def by simp then have "maximum pred_n ?y_with_j_skipped \<ge> ?y_with_j_skipped i" by (simp add: maximum_is_greater_or_equal) with can_skip_j and pred_n show ?thesis by simp next case False with i_range have case_False_nice: "i > j" by simp then obtain pred_i where pred_i: "i = Suc pred_i" by (rule lessE) (* TODO CL: ask why this works. I do not really understand what lessE does. *) from case_False_nice and pred_i (* wouldn't work with "from False" *) have can_skip_j_and_shift_left: "y i = ?y_with_j_skipped pred_i" unfolding skip_index_def by simp from case_False_nice and i_range and j_range and pred_i and pred_n have (* actually 2 \<le> i, but we don't need this *) "in_range pred_n pred_i" unfolding in_range_def by simp then have "maximum pred_n ?y_with_j_skipped \<ge> ?y_with_j_skipped pred_i" by (simp add: maximum_is_greater_or_equal) with can_skip_j_and_shift_left and pred_n show ?thesis by simp qed qed qed qed text{* One component of a vector is a maximum component iff it has a value greater or equal than the maximum of the remaining values. *} lemma maximum_greater_or_equal_remaining_maximum : (* TODO CL: discuss the name of this lemma; maybe there is something more appropriate *) fixes n::nat and y::real_vector and j::nat shows "non_negative_real_vector n y \<and> n > 0 \<and> in_range n j \<longrightarrow> (y j \<ge> maximum_except n y j \<longleftrightarrow> y j = maximum n y)" proof assume assms: "non_negative_real_vector n y \<and> n > 0 \<and> in_range n j" (* now break this down into its conjunctives *) from assms have non_negative: "non_negative_real_vector n y" .. from assms have non_empty: "n > 0" by simp (* TODO CL: ask why ".." doesnt work here *) from assms have range: "in_range n j" by simp (* now go on *) show "y j \<ge> maximum_except n y j \<longleftrightarrow> y j = maximum n y" proof assume ge_remaining: "y j \<ge> maximum_except n y j" from non_empty and range have "\<forall> i::nat . in_range n i \<and> i \<noteq> j \<longrightarrow> maximum_except n y j \<ge> y i" by (simp add: maximum_except_is_greater_or_equal) with ge_remaining have "\<forall> i::nat . in_range n i \<and> i \<noteq> j \<longrightarrow> y j \<ge> y i" by auto then have greater_or_equal: "\<forall> i::nat . in_range n i \<longrightarrow> y j \<ge> y i" by auto from range have is_component: "\<exists> i::nat . in_range n i \<and> y j = y i" by auto (* when we first tried non_empty: "n \<ge> 1" sledgehammer didn't find a proof for this *) with non_negative and non_empty and greater_or_equal show "y j = maximum n y" by (simp add: maximum_sufficient) (* TODO CL: ask whether it makes a difference to use "by auto" vs. "by simp" (or even "by arith") when either would work, and what's the difference between "from foo show bar by simp" vs. "show bar by (simp add: foo)" *) next (* nice to see that support for \<longleftrightarrow> is built in *) assume j_max: "y j = maximum n y" from non_empty have maximum_except_unfolded: "maximum_except n y j = maximum (n-(1::nat)) (skip_index y j)" by (metis Suc_diff_1 maximum_except.simps(2)) show "y j \<ge> maximum_except n y j" proof (cases "n = 1") case True with maximum_except_unfolded and maximum_def have "maximum_except n y j = 0" by auto with j_max and non_negative show ?thesis by (simp add: maximum_non_negative) next case False from j_max have ge: "\<forall>k::nat . in_range n k \<longrightarrow> y j \<ge> y k" by (simp add: maximum_is_greater_or_equal) from False and non_empty have "n > 1" by auto then have pred_non_empty: "(n-(1::nat)) > 0" by simp from non_empty and non_negative and range have pred_non_negative: "non_negative_real_vector (n-(1::nat)) (skip_index y j)" by (metis skip_index_keeps_non_negativity) from pred_non_empty and pred_non_negative and maximum_is_component have "\<exists> i::nat . in_range (n-(1::nat)) i \<and> maximum (n-(1::nat)) (skip_index y j) = (skip_index y j) i" by simp then obtain i::nat where maximum_except_component: "in_range (n-(1::nat)) i \<and> maximum (n-(1::nat)) (skip_index y j) = (skip_index y j) i" .. then have i_range: "in_range (n-(1::nat)) i" .. from maximum_except_component and maximum_except_unfolded have maximum_except_component_nice: "maximum_except n y j = (skip_index y j) i" by simp have skip_index_range: "\<dots> = y i \<or> (skip_index y j) i = y (Suc i)" unfolding skip_index_def by auto from i_range have 1: "in_range n i" unfolding in_range_def by arith from i_range have 2: "in_range n (Suc i)" unfolding in_range_def by arith from skip_index_range and 1 and 2 have "\<exists> k::nat . in_range n k \<and> (skip_index y j) i = y k" by auto (* The following (found by remote_vampire) was nearly impossible for metis to prove: *) (* from i_range and range and skip_index_def and maximum_except_component (* not sure why we need this given that we have maximum_except_component *) have "\<exists> k::nat . in_range n k \<and> (skip_index y j) i = y k" by (metis (full_types) One_nat_def Suc_neq_Zero Suc_pred' leD less_Suc0 less_Suc_eq_le linorder_le_less_linear) *) then obtain k::nat where "in_range n k \<and> (skip_index y j) i = y k" .. with ge and maximum_except_component_nice show "y j \<ge> maximum_except n y j" by simp qed qed qed text{* Changing one component in a vector doesn't affect the maximum of the remaining components. *} lemma remaining_maximum_invariant : (* TODO CL: discuss the name of this lemma; maybe there is something more appropriate *) fixes n::nat and y::real_vector and i::nat and a::real assumes non_empty: "n > 0" and range: "in_range n i" shows "maximum_except n y i = maximum_except n (deviation n y a i) i" proof - from range have "\<forall>j::nat . in_range n j \<and> j \<noteq> i \<longrightarrow> y j = deviation n y a i j" unfolding deviation_def by simp with non_empty and range have "\<forall>k::nat . in_range (n-(1::nat)) k \<longrightarrow> skip_index y i k = skip_index (deviation n y a i) i k" by (simp add: equal_by_skipping) then have "maximum (n-(1::nat)) (skip_index y i) = maximum (n-(1::nat)) (skip_index (deviation n y a i) i)" by (simp add: maximum_equal) with non_empty show ?thesis by (metis Suc_pred' maximum_except.simps(2)) qed section{* Second-price auction *} text{* Agent i being the winner of a second-price auction (see below for complete definition) means * he/she is one of the participants with the highest bids * he/she wins the auction * and pays the maximum price that remains after removing the winner's own bid from the vector of bids. *} definition second_price_auction_winner :: "participants \<Rightarrow> real_vector \<Rightarrow> allocation \<Rightarrow> payments \<Rightarrow> participant \<Rightarrow> bool" where "second_price_auction_winner n b x p i \<equiv> in_range n i \<and> i \<in> arg_max_set n b \<and> x b i \<and> (p b i = maximum_except n b i)" text{* Agent i being a loser of a second-price auction (see below for complete definition) means * he/she loses the auction * and pays nothing *} definition second_price_auction_loser :: "participants \<Rightarrow> real_vector \<Rightarrow> allocation \<Rightarrow> payments \<Rightarrow> participant \<Rightarrow> bool" where "second_price_auction_loser n b x p i \<equiv> in_range n i \<and> \<not>x b i \<and> p b i = 0" text{* A second-price auction is an auction whose outcome satisfies the following conditions: 1. 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.) 2. The price that the winner pays is the maximum bid that remains after removing the winner's own bid from the vector of bids. 3. The losers do not pay anything. *} definition second_price_auction :: "participants \<Rightarrow> allocation \<Rightarrow> payments \<Rightarrow> bool" where "second_price_auction n x p \<equiv> \<forall> b::real_vector . bids n b \<longrightarrow> allocation n b x \<and> vickrey_payment n b p \<and> (\<exists>i::participant. in_range n i \<and> second_price_auction_winner n b x p i \<and> (\<forall>j::participant. in_range n j \<and> j \<noteq> i \<longrightarrow> second_price_auction_loser n b x p j))" 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. *} lemma second_price_auction_has_only_one_winner : fixes n::participants and x::allocation and p::payments and b::real_vector and winner::participant assumes spa: "second_price_auction n x p" and bids: "bids n b" and winner: "second_price_auction_winner n b x p winner" shows "\<forall>j::participant. second_price_auction_winner n b x p j \<longrightarrow> j = winner" proof fix j::participant from winner have wins: "x b winner" by (simp add: second_price_auction_winner_def) show "second_price_auction_winner n b x p j \<longrightarrow> j = winner" proof assume "second_price_auction_winner n b x p j" then have j_wins: "x b j" by (simp add: second_price_auction_winner_def) from spa and bids have "allocation n b x" by (simp add: second_price_auction_def) with wins and j_wins show "j = winner" by (simp add: allocation_unique) qed qed 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::participants and x::allocation and p::payments and b::real_vector and winner::participant assumes spa: "second_price_auction n x p" and bids: "bids n b" and wins: "x b winner" (* note that we need not assume anything about the range of winner *) shows "second_price_auction_winner n b x p winner" proof - from wins and spa and bids and second_price_auction_winner_def and second_price_auction_has_only_one_winner show ?thesis by (metis allocation_unique second_price_auction_def) qed 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::participants and x::allocation and p::payments and b::real_vector assumes spa: "second_price_auction n x p" and bids: "bids n b" shows "\<forall>i::participant . in_range n i \<and> \<not> x b i \<longrightarrow> second_price_auction_loser n b x p i" proof fix i::participant show "in_range n i \<and> \<not> x b i \<longrightarrow> second_price_auction_loser n b x p i" proof assume assms: "in_range n i \<and> \<not> x b i" from assms have range: "in_range n i" .. from assms have loses: "\<not> x b i" .. show "second_price_auction_loser n b x p i" proof - (* by contradiction *) { assume False: "\<not> second_price_auction_loser n b x p i" from spa and bids and second_price_auction_def have "(\<exists>j::participant. in_range n j \<and> second_price_auction_winner n b x p j \<and> (\<forall>k::participant. in_range n k \<and> k \<noteq> j \<longrightarrow> second_price_auction_loser n b x p k))" by simp with False and range have "second_price_auction_winner n b x p i" by auto (* Before we had introduced in_range as a predicate consistently used both in the winner and the loser branch, even metis wan't able to prove this without exceeding the unification bound. *) with second_price_auction_winner_def have "x b i" by simp with loses have "False" .. } then show ?thesis by blast qed qed qed text{* If there is only one bidder with a maximum bid, that bidder wins. *} lemma only_max_bidder_wins : fixes n::participants and max_bidder::participant and b::real_vector and x::allocation and p::payments assumes spa: "second_price_auction n x p" and bids: "bids n b" and range: "in_range n max_bidder" (* and max_bidder: "b max_bidder = maximum n b" *) (* we actually don't need this :-) *) and only_max_bidder: "b max_bidder > maximum_except n b max_bidder" shows "second_price_auction_winner n b x p max_bidder" proof - have no_other_max: "\<forall>j::participant. in_range n j \<and> j \<noteq> max_bidder \<longrightarrow> j \<notin> arg_max_set n b" proof fix j::participant show "in_range n j \<and> j \<noteq> max_bidder \<longrightarrow> j \<notin> arg_max_set n b" proof assume j_not_max: "in_range n j \<and> j \<noteq> max_bidder" show "j \<notin> arg_max_set n b" proof - from j_not_max and range have "b j \<le> maximum_except n b max_bidder" using in_range_def maximum_except_is_greater_or_equal by (metis le_trans) with only_max_bidder have b_j_lt_max: "b j < b max_bidder" by simp then show ?thesis proof - (* by contradiction *) { assume "b j = maximum n b" with range have "b j \<ge> b max_bidder" by (simp add: maximum_is_greater_or_equal) with b_j_lt_max have False by simp } then show ?thesis unfolding arg_max_set_def by (metis (lifting, full_types) mem_Collect_eq) (* recommended by sledgehammer using e *) qed qed qed qed from bids and spa have x_is_allocation: "\<exists>i:: participant. in_range n i \<and> x b i \<and> (\<forall>j:: participant. j\<noteq>i \<longrightarrow> \<not>x b j)" unfolding second_price_auction_def allocation_def in_range_def by simp from bids and spa have "\<exists>i::participant. second_price_auction_winner n b x p i \<and> (\<forall>j::participant. in_range n j \<and> j \<noteq> i \<longrightarrow> second_price_auction_loser n b x p j)" unfolding second_price_auction_def by blast with (* max_bidder and *) (* turns out that we didn't need this :-) *) no_other_max and x_is_allocation show ?thesis by (metis (full_types) second_price_auction_winner_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::participants and v::real_vector and x::allocation and b::real_vector and p::payments and i::participant assumes spa: "second_price_auction n x p" and bids: "bids n b" and wins: "x b i" shows "payoff_vector v (x b) (p b) i = v i - maximum_except n b i" proof - have "payoff_vector v (x b) (p b) i = payoff (v i) (x b i) (p b i)" unfolding payoff_vector_def by simp also have "\<dots> = payoff (v i) True (p b i)" using wins by simp also have "\<dots> = v i - p b i" unfolding payoff_def by simp also have "\<dots> = v i - maximum_except n b i" using wins and spa and bids by (metis allocated_implies_spa_winner second_price_auction_winner_def) finally show ?thesis by simp qed text{* a formula for computing the payoff of a loser of a second-price auction *} lemma second_price_auction_loser_payoff : fixes n::participants and v::real_vector and x::allocation and b::real_vector and p::payments and i::participant assumes spa: "second_price_auction n x p" and bids: "bids n b" and range: "in_range n i" and loses: "\<not> x b i" shows "payoff_vector v (x b) (p b) i = 0" proof - from loses and spa and bids and range have "second_price_auction_loser n b x p i" by (simp add: not_allocated_implies_spa_loser) then show ?thesis unfolding second_price_auction_loser_def payoff_vector_def payoff_def by (metis (full_types) diff_0_right mult_zero_right) qed 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::participants and v::real_vector and x::allocation and b::real_vector and p::payments and i::participant (* how this was created by factoring out stuff from vickreyA proof cases 1a and 2a: 1. wrote "lemma \<dots> fixes \<dots> shows 2. pasted proof steps 3. added assumptions as needed *) assumes non_empty: "n > 0" and spa: "second_price_auction n x p" and bids: "bids n b" and range: "in_range n i" and wins: "x b i" shows "let i_sticks_with_valuation = deviation_vec n b v i in payoff_vector v (x b) (p b) i = v i - maximum_except n i_sticks_with_valuation i" proof - let ?i_sticks_with_valuation = "deviation_vec n b v i" (* i gets the good, so i also satisfies the further properties of a second price auction winner: *) from wins and spa and bids have "payoff_vector v (x b) (p b) i = v i - maximum_except n b i" by (simp add: second_price_auction_winner_payoff) (* i's deviation doesn't change the maximum remaining bid (which is the second highest bid when i wins) *) also have "\<dots> = v i - maximum_except n ?i_sticks_with_valuation i" unfolding deviation_vec_def using non_empty and range and remaining_maximum_invariant by auto finally show ?thesis by simp qed section{* Efficiency *} text{* A single good auction (this is the one we are talking about here) is efficient, if the winner is among the participants who have the highest valuation of the good. *} definition efficient :: "participants \<Rightarrow> real_vector \<Rightarrow> real_vector \<Rightarrow> allocation \<Rightarrow> bool" where "efficient n v b x \<equiv> (valuation n v \<and> bids n b) \<and> (\<forall>i::participant. in_range n i \<and> x b i \<longrightarrow> i \<in> arg_max_set n v)" section{* Equilibrium in weakly dominant strategies *} text{* Given some auction, a strategy profile supports an equilibrium in weakly dominant strategies if each participant maximises its payoff by playing its component in that profile, whatever the other participants do. *} definition equilibrium_weakly_dominant_strategy :: "participants \<Rightarrow> real_vector \<Rightarrow> real_vector \<Rightarrow> allocation \<Rightarrow> payments \<Rightarrow> bool" where "equilibrium_weakly_dominant_strategy n v b x p \<equiv> valuation n v \<and> bids n b \<and> allocation n b x \<and> vickrey_payment n b p \<and> (\<forall> i::participant . in_range n i \<longrightarrow> (\<forall> whatever_bid::real_vector . bids n whatever_bid \<and> whatever_bid i \<noteq> b i \<longrightarrow> ( let i_sticks_with_valuation = deviation_vec n whatever_bid b i (* here, all components are (whatever_bid j), just the i-th component remains (b i) *) in payoff_vector v (x i_sticks_with_valuation) (p i_sticks_with_valuation) i \<ge> payoff_vector v (x whatever_bid) (p whatever_bid) i)))" (* TODO CL: discuss whether we should define _dominant_ in addition to _weakly_ dominant. If so, can we refactor the definitions in some way that makes this less redundant? *) section{* Vickrey's Theorem *} subsection{* Part 1: A second-price auction supports an equilibrium in weakly dominant strategies if all participants bid their valuation. *} theorem vickreyA : fixes n::participants and v::real_vector and x::allocation and p::payments assumes val: "valuation n v" and spa: "second_price_auction n x p" shows "equilibrium_weakly_dominant_strategy n v v (* \<leftarrow> i.e. b *) x p" proof - let ?b = v (* From now on, we refer to v as ?b if we mean the _bids_ (which happen to be equal to the valuations) *) from val have bids: "bids n v" by (rule valuation_is_bid) have equilibrium_weakly_dominant_strategy_unfolded: "\<forall> i::participant . in_range n i \<longrightarrow> (\<forall> whatever_bid::real_vector . bids n whatever_bid \<and> whatever_bid i \<noteq> ?b i \<longrightarrow> ( let i_sticks_with_valuation = deviation_vec n whatever_bid ?b i in payoff_vector v (x i_sticks_with_valuation) (p i_sticks_with_valuation) i \<ge> payoff_vector v (x whatever_bid) (p whatever_bid) i))" proof fix i::participant show "in_range n i \<longrightarrow> (\<forall> whatever_bid::real_vector. bids n whatever_bid \<and> whatever_bid i \<noteq> ?b i \<longrightarrow> (let i_sticks_with_valuation = deviation_vec n whatever_bid ?b i in payoff_vector v (x i_sticks_with_valuation) (p i_sticks_with_valuation) i \<ge> payoff_vector v (x whatever_bid) (p whatever_bid) i))" proof (cases "n = 0") case True then show ?thesis by (simp add: in_range_def) next case False then have non_empty: "n > 0" .. show ?thesis proof assume i_range: "in_range n i" let ?b_bar = "maximum n ?b" show "\<forall> whatever_bid::real_vector. bids n whatever_bid \<and> whatever_bid i \<noteq> ?b i \<longrightarrow> (let i_sticks_with_valuation = deviation_vec n whatever_bid ?b i in payoff_vector v (x i_sticks_with_valuation) (p i_sticks_with_valuation) i \<ge> payoff_vector v (x whatever_bid) (p whatever_bid) i)" proof fix whatever_bid::real_vector let ?i_sticks_with_valuation = "deviation_vec n whatever_bid ?b i" (* Agent i sticks to bidding his/her valuation, whatever the others bid. Given this, we have to show that agent i is best off. *) have "bids n whatever_bid \<and> whatever_bid i \<noteq> ?b i \<longrightarrow> payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i \<ge> payoff_vector v (x whatever_bid) (p whatever_bid) i" proof assume alternative_bid: "bids n whatever_bid \<and> whatever_bid i \<noteq> ?b i" then have alternative_is_bid: "bids n whatever_bid" .. from bids and alternative_is_bid have i_sticks_is_bid: "bids n ?i_sticks_with_valuation" by (simp add: deviated_bid_well_formed) (* interesting part starts here *) show "payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i \<ge> payoff_vector v (x whatever_bid) (p whatever_bid) i" proof cases (* case 1 of the short proof *) assume i_wins: "x ?i_sticks_with_valuation i" (* i gets the good, so i also satisfies the further properties of a second price auction winner: *) with spa and i_sticks_is_bid have "i \<in> arg_max_set n ?i_sticks_with_valuation" by (metis allocated_implies_spa_winner second_price_auction_winner_def) (* TODO CL: ask whether it is possible to get to "have 'a' and 'b'" directly, without first saying "have 'a \<and> b' and then breaking it down "by auto". In an earlier version we had not only deduced i_in_max_set but also the payoff here. *) then have "?i_sticks_with_valuation i = maximum n ?i_sticks_with_valuation" by (simp add: arg_max_set_def) also have "\<dots> \<ge> maximum_except n ?i_sticks_with_valuation i" using i_sticks_is_bid and bids_def (* \<equiv> non_negative_real_vector n ?i_sticks_with_valuation *) and non_empty and i_range by (metis calculation maximum_greater_or_equal_remaining_maximum) finally have i_ge_max_except: "?i_sticks_with_valuation i \<ge> maximum_except n ?i_sticks_with_valuation i" by auto (* Now we show that i's payoff is \<ge> 0 *) from spa and i_sticks_is_bid and i_wins have "payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i = v i - maximum_except n ?i_sticks_with_valuation i" by (simp add: second_price_auction_winner_payoff) also have "\<dots> = ?i_sticks_with_valuation i - maximum_except n ?i_sticks_with_valuation i" unfolding deviation_vec_def deviation_def by simp finally have payoff_expanded: "payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i = ?i_sticks_with_valuation i - maximum_except n ?i_sticks_with_valuation i" by simp (* TODO CL: ask whether/how it is possible to name one step of a calculation (for reusing it) without breaking the chain (which is what we did here) *) also have "... \<ge> 0" using i_ge_max_except by simp finally have non_negative_payoff: "payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i \<ge> 0" by simp show ?thesis proof cases (* case 1a of the short proof *) assume "x whatever_bid i" with spa and alternative_is_bid and non_empty and i_range have "payoff_vector v (x whatever_bid) (p whatever_bid) i = ?i_sticks_with_valuation i - maximum_except n ?i_sticks_with_valuation i" using winners_payoff_on_deviation_from_valuation by (metis deviation_vec_def deviation_def) (* Now we show that i's payoff hasn't changed *) also have "\<dots> = payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i" using payoff_expanded by simp finally show ?thesis by simp (* = \<longrightarrow> \<le> *) next (* case 1b of the short proof *) assume "\<not> x whatever_bid i" (* i doesn't get the good, so i also satisfies the further properties of a second price auction loser: *) with spa and alternative_is_bid and i_range have "payoff_vector v (x whatever_bid) (p whatever_bid) i = 0" by (rule second_price_auction_loser_payoff) also have "\<dots> \<le> payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i" using non_negative_payoff by simp finally show ?thesis by simp qed next (* case 2 of the short proof *) assume i_loses: "\<not> x ?i_sticks_with_valuation i" (* i doesn't get the good, so i's payoff is 0 *) with spa and i_sticks_is_bid and i_range have zero_payoff: "payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i = 0" by (rule second_price_auction_loser_payoff) (* i's bid can't be higher than the second highest bid, as otherwise i would have won *) have i_bid_at_most_second: "?i_sticks_with_valuation i \<le> maximum_except n ?i_sticks_with_valuation i" proof - (* by contradiction *) { assume "\<not> ?i_sticks_with_valuation i \<le> maximum_except n ?i_sticks_with_valuation i" then have "?i_sticks_with_valuation i > maximum_except n ?i_sticks_with_valuation i" by simp with spa and i_sticks_is_bid and i_range have "second_price_auction_winner n ?i_sticks_with_valuation x p i" using only_max_bidder_wins (* a lemma we had from the formalisation of the earlier 10-case proof *) by auto with i_loses have False using second_price_auction_winner_def by auto } then show ?thesis by blast qed show ?thesis proof cases (* case 2a of the short proof *) assume "x whatever_bid i" with spa and alternative_is_bid and non_empty and i_range have "payoff_vector v (x whatever_bid) (p whatever_bid) i = ?i_sticks_with_valuation i - maximum_except n ?i_sticks_with_valuation i" using winners_payoff_on_deviation_from_valuation by (metis deviation_vec_def deviation_def) (* Now we can compute i's payoff *) also have "\<dots> \<le> 0" using i_bid_at_most_second by arith also have "\<dots> = payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i" using zero_payoff by arith finally show ?thesis by auto next (* case 2b of the short proof *) assume "\<not> x whatever_bid i" (* i doesn't get the good, so i's payoff is 0 *) with spa and alternative_is_bid and i_range have "payoff_vector v (x whatever_bid) (p whatever_bid) i = 0" by (rule second_price_auction_loser_payoff) also have "\<dots> = payoff_vector v (x ?i_sticks_with_valuation) (p ?i_sticks_with_valuation) i" using zero_payoff by simp finally show ?thesis by simp qed qed qed then show "bids n whatever_bid \<and> whatever_bid i \<noteq> ?b i \<longrightarrow> (let i_sticks_with_valuation = deviation_vec n whatever_bid ?b i in payoff_vector v (x i_sticks_with_valuation) (p i_sticks_with_valuation) i \<ge> payoff_vector v (x whatever_bid) (p whatever_bid) i)" (* TODO CL: ask why ?thesis doesn't work here *) by simp qed qed qed qed with spa val bids second_price_auction_def show ?thesis unfolding equilibrium_weakly_dominant_strategy_def by auto qed subsection{* Part 2: A second-price auction is efficient if all participants bid their valuation. *} (* TODO CL: document that we use local renamings (let) to make definition unfoldings resemble the original definitions *) theorem vickreyB : fixes n::participants and v::real_vector and x::allocation and p::payments assumes val: "valuation n v" and spa: "second_price_auction n x p" shows "efficient n v v x" proof - let ?b = v from val have bids: "bids n v" by (rule valuation_is_bid) have efficient_def_unfolded: "\<forall>k::participant. in_range n k \<and> x ?b k \<longrightarrow> k \<in> arg_max_set n v" unfolding efficient_def proof fix k:: participant show "in_range n k \<and> x ?b k \<longrightarrow> k \<in> arg_max_set n v" proof assume (* k_wins: *)"in_range n k \<and> x ?b k" with spa and bids show "k \<in> arg_max_set n v" using allocated_implies_spa_winner second_price_auction_winner_def by auto (* alternative proof with fewer prerequisites (before we had the lemmas used above): *) (* show "k \<in> arg_max_set n v" proof - from bids and spa have second_price_auction_participant: "\<exists>i::participant. second_price_auction_winner n ?b x p i \<and> (\<forall>j::participant. in_range n j \<and> j \<noteq> i \<longrightarrow> second_price_auction_loser n ?b x p j)" unfolding second_price_auction_def in_range_def by auto then obtain i::participant where i_winner: "second_price_auction_winner n ?b x p i \<and> (\<forall>j::participant. in_range n j \<and> j \<noteq> i \<longrightarrow> second_price_auction_loser n ?b x p j)" by blast then have i_values_highest: "i \<in> arg_max_set n v" unfolding second_price_auction_winner_def by simp (* note ?b = v *) have k_values_highest: "k \<in> arg_max_set n v" proof cases assume "k = i" with i_values_highest show ?thesis by blast next assume "k \<noteq> i" then show ?thesis using i_winner and k_wins by (auto simp add: second_price_auction_loser_def) qed show ?thesis using k_values_highest . qed *) qed qed with bids show ?thesis using efficient_def_unfolded val unfolding efficient_def by blast qed (* unused theorems (which might nevertheless be useful for the toolbox): * move cursor over the word "unused_thms" for jEdit to display the list * This has to be at the end of the file to make sure that the whole theory has been processed. *) unused_thms end

**Attachment:
signature.asc**

**Follow-Ups**:

- Previous by Date: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Date: Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Previous by Thread: Re: [isabelle] [ForMaRE] Re: Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Thread: [isabelle] Type restrictions; document preparation [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list