(* Auction Theory Toolbox (http://formare.github.io/auctions/) Authors: * Marco B. Caminati http://caminati.co.nr * Manfred Kerber <mnfrd.krbr@gmail.com> * Christoph Lange <math.semantic.web@gmail.com> * Colin Rowat <c.rowat@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) *) section ‹VCG auction: definitions and theorems› theory CombinatorialAuction imports UniformTieBreaking begin subsection ‹Definition of a VCG auction scheme, through the pair @{term "(vcga, vcgp)"}› (* b is a bid vector and participants is the set of all participants present in b *) abbreviation "participants b == Domain (Domain b)" (* goods is the list of goods auctioned *) abbreviation "goods == sorted_list_of_set o Union o Range o Domain" (* The seller is represented as integer 0, the other particants as integers 1, ..., n *) abbreviation "seller == (0::integer)" (* allAllocations' and allAllocations'' are variants of allAllocations. All three formulations are equivent. *) abbreviation "allAllocations' N Ω == injectionsUniverse ∩ {a. Domain a ⊆ N & Range a ∈ all_partitions Ω}" abbreviation "allAllocations'' N Ω == allocationsUniverse ∩ {a. Domain a ⊆ N & ⋃(Range a) = Ω}" lemma allAllocationsEquivalence: "allAllocations N Ω = allAllocations' N Ω & allAllocations N Ω = allAllocations'' N Ω" using allocationInjectionsUnivervseProperty allAllocationsIntersection by metis lemma allAllocationsVarCharacterization: "(a ∈ allAllocations'' N Ω) = (a ∈ allocationsUniverse& Domain a ⊆ N & ⋃(Range a) = Ω)" by force (* remove the seller from the set of all allocations *) abbreviation "soldAllocations N Ω == (Outside' {seller}) ` (allAllocations (N ∪ {seller}) Ω)" (* soldAllocations' and soldAllocations'' are variants of soldAllocations reflecting the different formulations of allAllocations. soldAllocations''' is yet another variant. These variants are used since for different proofs different variants are easier to use. *) abbreviation "soldAllocations' N Ω == (Outside' {seller}) ` (allAllocations' (N ∪ {seller}) Ω)" abbreviation "soldAllocations'' N Ω == (Outside' {seller}) ` (allAllocations'' (N ∪ {seller}) Ω)" abbreviation "soldAllocations''' N Ω == allocationsUniverse ∩ {aa. Domain aa⊆N-{seller} & ⋃(Range aa)⊆Ω}" lemma soldAllocationsEquivalence: "soldAllocations N Ω = soldAllocations' N Ω & soldAllocations' N Ω = soldAllocations'' N Ω" using allAllocationsEquivalence by metis corollary soldAllocationsEquivalenceVariant: "soldAllocations = soldAllocations' & soldAllocations' = soldAllocations'' & soldAllocations = soldAllocations''" using soldAllocationsEquivalence by metis lemma allocationSellerMonotonicity: "soldAllocations (N-{seller}) Ω ⊆ soldAllocations N Ω" using Outside_def by simp lemma allocationsUniverseCharacterization: "(a ∈ allocationsUniverse) = (a ∈ allAllocations'' (Domain a) (⋃(Range a)))" by blast lemma allocationMonotonicity: assumes "N1 ⊆ N2" shows "allAllocations'' N1 Ω ⊆ allAllocations'' N2 Ω" using assms by auto lemma allocationWithOneParticipant: assumes "a ∈ allAllocations'' N Ω" shows "Domain (a -- x) ⊆ N-{x}" using assms Outside_def by fastforce lemma soldAllocationIsAllocation: assumes "a ∈ soldAllocations N Ω" shows "a ∈ allocationsUniverse" proof - obtain aa where "a =aa -- seller & aa ∈ allAllocations (N∪{seller}) Ω" using assms by blast then have "a ⊆ aa & aa ∈ allocationsUniverse" unfolding Outside_def using allAllocationsIntersectionSubset by blast then show ?thesis using subsetAllocation by blast qed lemma soldAllocationIsAllocationVariant: assumes "a ∈ soldAllocations N Ω" shows "a ∈ allAllocations'' (Domain a) (⋃(Range a))" proof - show ?thesis using assms soldAllocationIsAllocation by auto blast+ qed lemma onlyGoodsAreSold: assumes "a ∈ soldAllocations'' N Ω" shows "⋃ (Range a) ⊆ Ω" using assms Outside_def by blast lemma soldAllocationIsRestricted: "a ∈ soldAllocations'' N Ω = (∃aa. aa -- (seller) = a ∧ aa ∈ allAllocations'' (N ∪ {seller}) Ω)" by blast (* Note that +* enlarges the function by one additional pair *) lemma restrictionConservation: "(R +* ({x}×Y)) -- x = R -- x" unfolding Outside_def paste_def by blast lemma allocatedToBuyerMeansSold: assumes "a ∈ allocationsUniverse" "Domain a ⊆ N-{seller}" "⋃ (Range a) ⊆ Ω" shows "a ∈ soldAllocations'' N Ω" proof - let ?i = "seller" let ?Y = "{Ω-⋃ (Range a)}-{{}}" let ?b = "{?i}×?Y" let ?aa = "a∪?b" let ?aa' = "a +* ?b" have 1: "a ∈ allocationsUniverse" using assms(1) by fast have "?b ⊆ {(?i,Ω-⋃(Range a))} - {(?i, {})}" by fastforce then have 2: "?b ∈ allocationsUniverse" using allocationUniverseProperty subsetAllocation by (metis(no_types)) have 3: "⋃ (Range a) ∩ ⋃ (Range ?b) = {}" by blast have 4: "Domain a ∩ Domain ?b ={}" using assms by fast have "?aa ∈ allocationsUniverse" using 1 2 3 4 by (rule allocationUnion) then have "?aa ∈ allAllocations'' (Domain ?aa) (⋃ (Range ?aa))" unfolding allocationsUniverseCharacterization by metis then have "?aa ∈ allAllocations'' (N∪{?i}) (⋃ (Range ?aa))" using allocationMonotonicity assms paste_def by auto moreover have "Range ?aa = Range a ∪ ?Y" by blast then moreover have "⋃ (Range ?aa) = Ω" using Un_Diff_cancel Un_Diff_cancel2 Union_Un_distrib Union_empty Union_insert by (metis (lifting, no_types) assms(3) cSup_singleton subset_Un_eq) moreover have "?aa' = ?aa" using 4 by (rule paste_disj_domains) ultimately have "?aa' ∈ allAllocations'' (N∪{?i}) Ω" by simp moreover have "Domain ?b ⊆ {?i}" by fast have "?aa' -- ?i = a -- ?i" by (rule restrictionConservation) moreover have "... = a" using Outside_def assms(2) by auto ultimately show ?thesis using soldAllocationIsRestricted by auto qed lemma allocationCharacterization: "a ∈ allAllocations N Ω = (a ∈ injectionsUniverse & Domain a ⊆ N & Range a ∈ all_partitions Ω)" by (metis (full_types) posssibleAllocationsRelCharacterization) (* The lemmas lm01, lm02, lm03, and lm04 are used in order to prove lemma soldAllocationVariantEquivalence *) lemma lm01: assumes "a ∈ soldAllocations'' N Ω" shows "Domain a ⊆ N-{seller} & a ∈ allocationsUniverse" proof - let ?i = "seller" obtain aa where 0: "a = aa -- ?i & aa ∈ allAllocations'' (N ∪ {?i}) Ω" using assms(1) soldAllocationIsRestricted by blast then have "Domain aa ⊆ N ∪ {?i}" using allocationCharacterization by blast then have "Domain a ⊆ N - {?i}" using 0 Outside_def by blast moreover have "a ∈ soldAllocations N Ω" using assms soldAllocationsEquivalenceVariant by metis then moreover have "a ∈ allocationsUniverse" using soldAllocationIsAllocation by blast ultimately show ?thesis by blast qed corollary lm02: assumes "a ∈ soldAllocations'' N Ω" shows "a ∈ allocationsUniverse & Domain a ⊆ N-{seller} & ⋃ (Range a) ⊆ Ω" proof - have "a ∈ allocationsUniverse" using assms lm01 [of a] by blast moreover have "Domain a ⊆ N-{seller}" using assms lm01 by blast moreover have "⋃ (Range a) ⊆ Ω" using assms onlyGoodsAreSold by blast ultimately show ?thesis by blast qed corollary lm03: "(a ∈ soldAllocations'' N Ω) = (a ∈ allocationsUniverse & a ∈ {aa. Domain aa ⊆ N-{seller} & ⋃ (Range aa) ⊆ Ω})" (is "?L = ?R") proof - have "(a∈soldAllocations'' N Ω) = (a∈allocationsUniverse& Domain a ⊆ N-{seller} & ⋃ (Range a) ⊆ Ω)" using lm02 allocatedToBuyerMeansSold by (metis (mono_tags)) then have "?L = (a∈allocationsUniverse& Domain a ⊆ N-{seller} & ⋃ (Range a) ⊆ Ω)" by fast moreover have "... = ?R" using mem_Collect_eq by (metis (lifting, no_types)) ultimately show ?thesis by auto qed corollary lm04: "a ∈ soldAllocations'' N Ω = (a∈ (allocationsUniverse ∩ {aa. Domain aa ⊆ N-{seller} & ⋃ (Range aa) ⊆ Ω}))" using lm03 by (metis (mono_tags) Int_iff) corollary soldAllocationVariantEquivalence: "soldAllocations'' N Ω = soldAllocations''' N Ω" (is "?L=?R") proof - { fix a have "a ∈ ?L = (a ∈ ?R)" by (rule lm04) } thus ?thesis by blast qed (* We use lm05 in order to show a variant for soldAllocations without ''' *) lemma lm05: assumes "a ∈ soldAllocations''' N Ω" shows "a -- n ∈ soldAllocations''' (N-{n}) Ω" proof - let ?bb = seller let ?d = Domain let ?r = Range let ?X1 = "{aa. ?d aa ⊆ N-{n}-{?bb} & ⋃(?r aa)⊆Ω}" let ?X2 = "{aa. ?d aa ⊆ N-{?bb} & ⋃(?r aa) ⊆ Ω}" have "a∈?X2" using assms(1) by fast then have 0: "?d a ⊆ N-{?bb} & ⋃(?r a) ⊆ Ω" by blast then have "?d (a--n) ⊆ N-{?bb}-{n}" using outside_reduces_domain by (metis Diff_mono subset_refl) moreover have "... = N-{n}-{?bb}" by fastforce ultimately have "?d (a--n) ⊆ N-{n}-{?bb}" by blast moreover have "⋃ (?r (a--n)) ⊆ Ω" unfolding Outside_def using 0 by blast ultimately have "a -- n ∈ ?X1" by fast moreover have "a--n ∈ allocationsUniverse" using assms(1) Int_iff allocationsUniverseOutside by (metis(lifting,mono_tags)) ultimately show ?thesis by blast qed lemma allAllocationsEquivalenceExtended: "soldAllocations = soldAllocations' & soldAllocations' = soldAllocations'' & soldAllocations'' = soldAllocations'''" using soldAllocationVariantEquivalence soldAllocationsEquivalenceVariant by metis (* The following corollary shows that an allocation is invariant to subtracting a single bidder. This is used a fundamental step to prove the non-negativity of price in VCG. *) corollary soldAllocationRestriction: assumes "a ∈ soldAllocations N Ω" shows "a -- n ∈ soldAllocations (N-{n}) Ω" proof - let ?A' = soldAllocations''' have "a ∈ ?A' N Ω" using assms allAllocationsEquivalenceExtended by metis then have "a -- n ∈ ?A' (N-{n}) Ω" by (rule lm05) thus ?thesis using allAllocationsEquivalenceExtended by metis qed corollary allocationGoodsMonotonicity: assumes "Ω1 ⊆ Ω2" shows "soldAllocations''' N Ω1 ⊆ soldAllocations''' N Ω2" using assms by blast corollary allocationGoodsMonotonicityVariant: assumes "Ω1 ⊆ Ω2" shows "soldAllocations'' N Ω1 ⊆ soldAllocations'' N Ω2" proof - have "soldAllocations'' N Ω1 = soldAllocations''' N Ω1" by (rule soldAllocationVariantEquivalence) moreover have "... ⊆ soldAllocations''' N Ω2" using assms(1) by (rule allocationGoodsMonotonicity) moreover have "... = soldAllocations'' N Ω2" using soldAllocationVariantEquivalence by metis ultimately show ?thesis by auto qed (* maximalStrictAllocationsAlg are the allocations maximizing the revenue. They also include the unallocated goods assigned to the seller (bidder 0).*) abbreviation "maximalStrictAllocations N Ω b == argmax (sum b) (allAllocations ({seller}∪N) Ω)" (* randomBids builds up a bid vector from a random number so that bidding with this bid vector resolves any ties. Details are defined in UniformTieBreaking.thy *) abbreviation "randomBids N Ω b random == resolvingBid (N∪{seller}) Ω b random" (* vcgas gives the one-element set with the winning allocation after tie breaking. (argmax∘sum) b ... determines the set of all maximal allocations. (argmax∘sum) (randomBids ...) restricts that by tie-breaking to a singleton. Outside' {seller} removes the seller from the only allocation in the singleton. *) abbreviation "vcgas N Ω b r == Outside' {seller} `((argmax∘sum) (randomBids N Ω b r) ((argmax∘sum) b (allAllocations (N ∪ {seller}) (set Ω))))" (* Takes the element out of the one elemnt set (vcgas ...) *) abbreviation "vcga N Ω b r == the_elem (vcgas N Ω b r)" (* alternative definition of vcga *) abbreviation "vcga' N Ω b r == (the_elem (argmax (sum (randomBids N Ω b r)) (maximalStrictAllocations N (set Ω) b))) -- seller" (* The following three auxiliary lemmas, lm06, lm07, and lm08 are used to prove lemma vcgaEquivalence as well as in the theorem that cardinality of vcgas is one.*) lemma lm06: assumes "card ((argmax∘sum) (randomBids N Ω b r) ((argmax∘sum) b (allAllocations (N∪{seller}) (set Ω)))) = 1" shows "vcga N Ω b r = (the_elem ((argmax∘sum) (randomBids N Ω b r) ((argmax∘sum) b (allAllocations ({seller}∪N) (set Ω))))) -- seller" using assms cardOneTheElem by auto corollary lm07: assumes "card ((argmax∘sum) (randomBids N Ω b r) ((argmax∘sum) b (allAllocations (N∪{seller}) (set Ω)))) = 1" shows "vcga N Ω b r = vcga' N Ω b r" (is "?l = ?r") proof - have "?l = (the_elem ((argmax∘sum) (randomBids N Ω b r) ((argmax∘sum) b (allAllocations ({seller}∪N) (set Ω))))) -- seller" using assms by (rule lm06) moreover have "... = ?r" by force ultimately show ?thesis by blast qed lemma lm08: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "card ((argmax∘sum) (randomBids N Ω bids random) ((argmax∘sum) bids (allAllocations (N∪{seller}) (set Ω)))) = 1" (is "card ?l=_") proof - let ?N = "N∪{seller}" let ?b' = "randomBids N Ω bids random" let ?s = sum let ?a = argmax let ?f = "?a ∘ ?s" have 1: "?N≠{}" by auto have 2: "finite ?N" using assms(3) by simp have "?a (?s ?b') (?a (?s bids) (allAllocations ?N (set Ω))) = {chosenAllocation ?N Ω bids random}" (is "?L=?R") using 1 assms(1) assms(2) 2 by (rule winningAllocationUniqueness) moreover have "?L= ?f ?b' (?f bids (allAllocations ?N (set Ω)))" by auto ultimately have "?l = {chosenAllocation ?N Ω bids random}" by simp moreover have "card ...=1" by simp ultimately show ?thesis by simp qed lemma vcgaEquivalence: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "vcga N Ω b r = vcga' N Ω b r" using assms lm07 lm08 by blast (* After showing that the cardinality of vcgas is 1, we know that the_elem to determine vcga will return a definite value. *) theorem vcgaDefiniteness: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "card (vcgas N Ω b r) = 1" proof - have "card ((argmax∘sum) (randomBids N Ω b r) ((argmax∘sum) b (allAllocations (N∪{seller}) (set Ω)))) = 1" (is "card ?X = _") using assms lm08 by blast moreover have "(Outside'{seller}) ` ?X = vcgas N Ω b r" by blast ultimately show ?thesis using cardOneImageCardOne by blast qed (* The following lemma is a variant of the vcgaDefiniteness theorem. *) lemma vcgaDefinitenessVariant: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "card (argmax (sum (randomBids N Ω b r)) (maximalStrictAllocations N (set Ω) b)) = 1" (is "card ?L=_") proof - let ?n = "{seller}" have 1: "(?n ∪ N)≠{}" by simp have 2: "finite (?n∪N)" using assms(3) by fast have "terminatingAuctionRel (?n∪N) Ω b r = {chosenAllocation (?n∪N) Ω b r}" using 1 assms(1) assms(2) 2 by (rule winningAllocationUniqueness) moreover have "?L = terminatingAuctionRel (?n∪N) Ω b r" by auto ultimately show ?thesis by auto qed theorem winningAllocationIsMaximal: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "the_elem (argmax (sum (randomBids N Ω b r)) (maximalStrictAllocations N (set Ω) b)) ∈ (maximalStrictAllocations N (set Ω) b)" (is "the_elem ?X ∈ ?R") proof - have "card ?X=1" using assms by (rule vcgaDefinitenessVariant) moreover have "?X ⊆ ?R" by auto ultimately show ?thesis using cardinalityOneTheElem by blast qed corollary winningAllocationIsMaximalWithoutSeller: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "vcga' N Ω b r ∈ (Outside' {seller})`(maximalStrictAllocations N (set Ω) b)" using assms winningAllocationIsMaximal by blast lemma maximalAllactionWithoutSeller: "(Outside' {seller})`(maximalStrictAllocations N Ω b) ⊆ soldAllocations N Ω" using Outside_def by force lemma onlyGoodsAreAllocatedAuxiliary: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "vcga' N Ω b r ∈ soldAllocations N (set Ω)" (is "?a ∈ ?A") proof - have "?a ∈ (Outside' {seller})`(maximalStrictAllocations N (set Ω) b)" using assms by (rule winningAllocationIsMaximalWithoutSeller) thus ?thesis using maximalAllactionWithoutSeller by fastforce qed theorem onlyGoodsAreAllocated: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "vcga N Ω b r ∈ soldAllocations N (set Ω)" (is "_∈?r") proof - have "vcga' N Ω b r ∈ ?r" using assms by (rule onlyGoodsAreAllocatedAuxiliary) then show ?thesis using assms vcgaEquivalence by blast qed (* Let b be a bid vector such that the seller's bid for each possible set of goods is 0 then the revenue does not depend on the presence of the seller. *) corollary neutralSeller: assumes "∀X. X ∈ Range a ⟶b (seller, X)=0" "finite a" shows "sum b a = sum b (a--seller)" proof - let ?n = seller have "finite (a||{?n})" using assms restrict_def by (metis finite_Int) moreover have "∀z ∈ a||{?n}. b z=0" using assms restrict_def by fastforce ultimately have "sum b (a||{?n}) = 0" using assms by (metis sum.neutral) thus ?thesis using sumOutside assms(2) by (metis add.comm_neutral) qed corollary neutralSellerVariant: assumes "∀a∈A. finite a & (∀ X. X∈Range a ⟶ b (seller, X)=0)" shows "{sum b a| a. a∈A} = {sum b (a -- seller)| a. a∈A}" using assms neutralSeller by (metis (lifting, no_types)) lemma vcgaIsMaximalAux1: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "∃a. ((a ∈ (maximalStrictAllocations N (set Ω) b)) ∧ (vcga' N Ω b r = a -- seller) & (a ∈ argmax (sum b) (allAllocations ({seller}∪N) (set Ω))))" using assms winningAllocationIsMaximalWithoutSeller by fast lemma vcgaIsMaximalAux2: assumes "distinct Ω" "set Ω ≠ {}" "finite N" "∀a ∈ allAllocations ({seller}∪N) (set Ω). ∀ X ∈ Range a. b (seller, X)=0" (is "∀a∈?X. _") shows "sum b (vcga' N Ω b r) = Max{sum b a| a. a ∈ soldAllocations N (set Ω)}" proof - let ?n = seller let ?s = sum let ?a = "vcga' N Ω b r" obtain a where 0: "a ∈ maximalStrictAllocations N (set Ω) b & ?a = a--?n & (a ∈ argmax (sum b) (allAllocations({seller}∪N)(set Ω)))" (is "_ & ?a=_ & a∈?Z") using assms(1,2,3) vcgaIsMaximalAux1 by blast have 1: "∀a ∈ ?X. finite a & (∀ X. X∈Range a ⟶ b (?n, X)=0)" using assms(4) List.finite_set allocationFinite by metis have 2: "a ∈ ?X" using 0 by auto have "a ∈ ?Z" using 0 by fast then have "a ∈ ?X∩{x. ?s b x = Max (?s b ` ?X)}" using injectionsUnionCommute by simp then have "a ∈ {x. ?s b x = Max (?s b ` ?X)}" using injectionsUnionCommute by simp moreover have "?s b ` ?X = {?s b a| a. a∈?X}" by blast ultimately have "?s b a = Max {?s b a| a. a∈?X}" by auto moreover have "{?s b a| a. a∈?X} = {?s b (a--?n)| a. a∈?X}" using 1 by (rule neutralSellerVariant) moreover have "... = {?s b a| a. a ∈ Outside' {?n}`?X}" by blast moreover have "... = {?s b a| a. a ∈ soldAllocations N (set Ω)}" by simp ultimately have "Max {?s b a| a. a ∈ soldAllocations N (set Ω)} = ?s b a" by simp moreover have "... = ?s b (a--?n)" using 1 2 neutralSeller by (metis (lifting, no_types)) ultimately show "?s b ?a=Max{?s b a| a. a ∈ soldAllocations N (set Ω)}" using 0 by simp qed text ‹Adequacy theorem: The allocation satisfies the standard pen-and-paper specification of a VCG auction. See, for example, \<^cite>‹‹\S~1.2› in "cramton"›.› theorem vcgaIsMaximal: assumes "distinct Ω" "set Ω ≠ {}" "finite N" "∀ X. b (seller, X) = 0" shows "sum b (vcga' N Ω b r) = Max{sum b a| a. a ∈ soldAllocations N (set Ω)}" using assms vcgaIsMaximalAux2 by blast corollary vcgaIsAllocationAllocatingGoodsOnly: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "vcga' N Ω b r ∈ allocationsUniverse & ⋃ (Range (vcga' N Ω b r)) ⊆ set Ω" proof - let ?a = "vcga' N Ω b r" let ?n = seller obtain a where 0: "?a = a -- seller & a ∈ maximalStrictAllocations N (set Ω) b" using assms winningAllocationIsMaximalWithoutSeller by blast then moreover have 1: "a ∈ allAllocations ({?n}∪N) (set Ω)" by auto moreover have "maximalStrictAllocations N (set Ω) b ⊆ allocationsUniverse" by (metis (lifting, mono_tags) winningAllocationPossible allAllocationsUniverse subset_trans) ultimately moreover have "?a = a -- seller & a ∈ allocationsUniverse" by blast then have "?a ∈ allocationsUniverse" using allocationsUniverseOutside by auto moreover have "⋃ (Range a) = set Ω" using allAllocationsIntersectionSetEquals 1 by metis then moreover have "⋃ (Range ?a) ⊆ set Ω" using Outside_def 0 by fast ultimately show ?thesis using allocationsUniverseOutside Outside_def by blast qed (* The price a participant n has to pay is the revenue achieved if n had not participated minus the value of the goods allocated not to n. *) abbreviation "vcgp N Ω b r n == Max (sum b ` (soldAllocations (N-{n}) (set Ω))) - (sum b (vcga N Ω b r -- n))" (* Since vcga is well-defined the following theorem is trivial. *) theorem vcgpDefiniteness: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "∃! y. vcgp N Ω b r n = y" using assms vcgaDefiniteness by simp lemma soldAllocationsFinite: assumes "finite N" "finite Ω" shows "finite (soldAllocations N Ω)" using assms allAllocationsFinite finite.emptyI finite.insertI finite_UnI finite_imageI by metis text‹The price paid by any participant is non-negative.› theorem NonnegPrices: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "vcgp N Ω b r n >= (0::price)" proof - let ?a = "vcga N Ω b r" let ?A = soldAllocations let ?f = "sum b" have "?a ∈ ?A N (set Ω)" using assms by (rule onlyGoodsAreAllocated) then have "?a -- n ∈ ?A (N-{n}) (set Ω)" by (rule soldAllocationRestriction) moreover have "finite (?A (N-{n}) (set Ω))" using assms(3) soldAllocationsFinite finite_set finite_Diff by blast ultimately have "Max (?f`(?A (N-{n}) (set Ω))) ≥ ?f (?a -- n)" (is "?L >= ?R") by (rule maxLemma) then show "?L - ?R >=0" by linarith qed lemma allocationDisjointAuxiliary: assumes "a ∈ allocationsUniverse" and "n1 ∈ Domain a" and "n2 ∈ Domain a" and "n1 ≠ n2" shows "a,,n1 ∩ a,,n2 = {}" proof - have "Range a ∈ partitionsUniverse" using assms nonOverlapping by blast moreover have "a ∈ injectionsUniverse & a ∈ partitionValuedUniverse" using assms by (metis (lifting, no_types) IntD1 IntD2) ultimately moreover have "a,,n1 ∈ Range a" using assms by (metis (mono_tags) eval_runiq_in_Range mem_Collect_eq) ultimately moreover have "a,,n1 ≠ a,,n2" using assms converse.intros eval_runiq_rel mem_Collect_eq runiq_basic by (metis (lifting, no_types)) ultimately show ?thesis using is_non_overlapping_def by (metis (lifting, no_types) assms(3) eval_runiq_in_Range mem_Collect_eq) qed lemma allocationDisjoint: assumes "a ∈ allocationsUniverse" and "n1 ∈ Domain a" and "n2 ∈ Domain a" and "n1 ≠ n2" shows "a,,,n1 ∩ a,,,n2 = {}" using assms allocationDisjointAuxiliary imageEquivalence by fastforce text‹No good is assigned twice.› (* We assume implicitely that n1, n2 are participants, Ω a goods list and N the participant set with "n1 ∈ Domain (vcga' N Ω b r)" "n2 ∈ Domain (vcga' N Ω b r)". However, formally these assumptions are not needed for the theorem. *) theorem PairwiseDisjointAllocations: assumes "distinct Ω" "set Ω ≠ {}" "finite N" "n1 ≠ n2" shows "(vcga' N Ω b r),,,n1 ∩ (vcga' N Ω b r),,,n2 = {}" proof - have "vcga' N Ω b r ∈ allocationsUniverse" using vcgaIsAllocationAllocatingGoodsOnly assms by blast then show ?thesis using allocationDisjoint assms by fast qed text ‹Nothing outside the set of goods is allocated.› theorem OnlyGoodsAllocated: assumes "distinct Ω" "set Ω ≠ {}" "finite N" "g ∈ (vcga N Ω b r),,,n" shows "g ∈ set Ω" proof - let ?a = "vcga' N Ω b r" have "?a ∈ allocationsUniverse" using assms(1,2,3) vcgaIsAllocationAllocatingGoodsOnly by blast then have 1: "runiq ?a" using assms(1,2,3) by blast have 2: "n ∈ Domain ?a" using assms vcgaEquivalence by fast with 1 have "?a,,n ∈ Range ?a" using eval_runiq_in_Range by fast with 1 2 have "?a,,,n ∈ Range ?a" using imageEquivalence by fastforce then have "g ∈ ⋃ (Range ?a)" using assms vcgaEquivalence by blast moreover have "⋃ (Range ?a) ⊆ set Ω" using assms(1,2,3) vcgaIsAllocationAllocatingGoodsOnly by fast ultimately show ?thesis by blast qed subsection ‹Computable versions of the VCG formalization› (* The computable versions are used to extract code. Furthermore we prove the equivalence with their classical counterparts. This computes the set of all maximal allocations including the seller. *) abbreviation "maximalStrictAllocationsAlg N Ω b == argmax (sum b) (set (allAllocationsAlg ({seller}∪N) Ω))" (* This computes the maximal allocation after tie breaking. *) definition "chosenAllocationAlg N Ω b (r::integer) == (randomEl (takeAll (%x. x∈ (argmax ∘ sum) b (set (allAllocationsAlg N Ω))) (allAllocationsAlg N Ω)) r)" (* This is the computable version of maxbid in UniformTieBreaking.thy. It takes an allocation, the bidders and the goods and computes a bid such for each good a bidder bids 1 if they get that good in allocation a, else they bid 0.*) definition "maxbidAlg a N Ω == (bidMaximizedBy a N Ω) Elsee 0" (* This is the completed version of summedBidVectorRel by returning 0 if summedBidVectorRel is not defined. *) definition "summedBidVectorAlg bids N Ω == (summedBidVectorRel bids N Ω) Elsee 0" (* Computable version of tiebids. If computes a bid vector that when the VCG algorithm runs on it yields the singleton {a}. *) definition "tiebidsAlg a N Ω == summedBidVectorAlg (maxbidAlg a N Ω) N Ω" (* Computable version of resolvingBid, that is, is computes the bid vector in random values that returns the chosen winning allocation *) definition "resolvingBidAlg N Ω bids random == tiebidsAlg (chosenAllocationAlg N Ω bids random) N (set Ω)" (* The same as above, but adding the seller who receives all unallocated goods. *) definition "randomBidsAlg N Ω b random == resolvingBidAlg (N∪{seller}) Ω b random" (* Computable allocation without those participants who do not receive anything. *) definition "vcgaAlgWithoutLosers N Ω b r == (the_elem (argmax (sum (randomBidsAlg N Ω b r)) (maximalStrictAllocationsAlg N Ω b))) -- seller" (* Adding losers to an arbitrary allocation *) abbreviation "addLosers participantset allocation == (participantset × {{}}) +* allocation" (* Computable version of vcga. It computes the winning allocation incl. losers. *) definition "vcgaAlg N Ω b r = addLosers N (vcgaAlgWithoutLosers N Ω b r)" (* Computable version of soldAllocations *) abbreviation "soldAllocationsAlg N Ω == (Outside' {seller}) ` set (allAllocationsAlg (N ∪ {seller}) Ω)" (* Computable version of vcgp, which computes the prices each participant has to pay. Note that losers do not pay anything, hence vcgaAlgWithoutLosers is here equivalent to vcgaAlg. The price a participant n has to pay is the revenue achieved if n had not participated minus the value of the goods allocated not to n.*) definition "vcgpAlg N Ω b r n (winningAllocation::allocation) = Max (sum b ` (soldAllocationsAlg (N-{n}) Ω)) - (sum b (winningAllocation -- n))" lemma functionCompletion: assumes "x ∈ Domain f" shows "toFunction f x = (f Elsee 0) x" unfolding toFunctionWithFallbackAlg_def by (metis assms toFunction_def) (* This technical lemma shows the equivalence of Elsee and toFunction inside a sum expression under certain assumptions. It is used for the proof of the bridging theorem that the two versions of the definition of maximalStrictAllocations are equivalent.*) lemma lm09: assumes "fst pair ∈ N" "snd pair ∈ Pow Ω - {{}}" shows "sum (%g. (toFunction (bidMaximizedBy a N Ω)) (fst pair, g)) (finestpart (snd pair)) = sum (%g. ((bidMaximizedBy a N Ω) Elsee 0) (fst pair, g)) (finestpart (snd pair))" proof - let ?f1 = "%g.(toFunction (bidMaximizedBy a N Ω))(fst pair, g)" let ?f2 = "%g.((bidMaximizedBy a N Ω) Elsee 0)(fst pair, g)" { fix g assume "g ∈ finestpart (snd pair)" then have 0: "g ∈ finestpart Ω" using assms finestpartSubset by (metis Diff_iff Pow_iff in_mono) have "?f1 g = ?f2 g" proof - have "⋀x⇩_{1}x⇩_{2}. (x⇩_{1}, g) ∈ x⇩_{2}× finestpart Ω ∨ x⇩_{1}∉ x⇩_{2}" by (metis 0 mem_Sigma_iff) then have "(pseudoAllocation a <| (N × finestpart Ω)) (fst pair, g) = maxbidAlg a N Ω (fst pair, g)" unfolding toFunctionWithFallbackAlg_def maxbidAlg_def by (metis (no_types) domainCharacteristicFunction UnCI assms(1) toFunction_def) thus ?thesis unfolding maxbidAlg_def by blast qed } thus ?thesis using sum.cong by simp qed (* lm10, lm11, lm12, l13 are variants of lm09 *) corollary lm10: assumes "pair ∈ N × (Pow Ω - {{}})" shows "summedBid (toFunction (bidMaximizedBy a N Ω)) pair = summedBid ((bidMaximizedBy a N Ω) Elsee 0) pair" proof - have "fst pair ∈ N" using assms by force moreover have "snd pair ∈ Pow Ω - {{}}" using assms(1) by force ultimately show ?thesis using lm09 by blast qed corollary lm11: "∀ pair ∈ N × (Pow Ω - {{}}). summedBid (toFunction (bidMaximizedBy a N Ω)) pair = summedBid ((bidMaximizedBy a N Ω) Elsee 0) pair" using lm10 by blast corollary lm12: "(summedBid (toFunction (bidMaximizedBy a N Ω))) ` (N × (Pow Ω - {{}}))= (summedBid ((bidMaximizedBy a N Ω) Elsee 0)) ` (N × (Pow Ω - {{}}))" (is "?f1 ` ?Z = ?f2 ` ?Z") proof - have "∀ z ∈ ?Z. ?f1 z = ?f2 z" by (rule lm11) thus ?thesis by (rule functionEquivalenceOnSets) qed corollary lm13: "summedBidVectorRel (toFunction (bidMaximizedBy a N Ω)) N Ω = summedBidVectorRel ((bidMaximizedBy a N Ω) Elsee 0) N Ω" using lm12 by metis corollary maxbidEquivalence: "summedBidVectorRel (maxbid a N Ω) N Ω = summedBidVectorRel (maxbidAlg a N Ω) N Ω" unfolding maxbidAlg_def using lm13 by metis lemma summedBidVectorEquivalence: assumes "x ∈ (N × (Pow Ω - {{}}))" shows "summedBidVector (maxbid a N Ω) N Ω x = summedBidVectorAlg (maxbidAlg a N Ω) N Ω x" (is "?f1 ?g1 N Ω x = ?f2 ?g2 N Ω x") proof - let ?h1 = "maxbid a N Ω" let ?h2 = "maxbidAlg a N Ω" have "summedBidVectorRel ?h1 N Ω = summedBidVectorRel ?h2 N Ω" using maxbidEquivalence by metis moreover have "summedBidVectorAlg ?h2 N Ω = (summedBidVectorRel ?h2 N Ω) Elsee 0" unfolding summedBidVectorAlg_def by fast ultimately have " summedBidVectorAlg ?h2 N Ω=summedBidVectorRel ?h1 N Ω Elsee 0" by simp moreover have "... x = (toFunction (summedBidVectorRel ?h1 N Ω)) x" using assms functionCompletion summedBidVectorCharacterization by (metis (mono_tags)) ultimately have "summedBidVectorAlg ?h2 N Ω x = (toFunction (summedBidVectorRel ?h1 N Ω)) x" by (metis (lifting, no_types)) thus ?thesis by simp qed (* TPTP ? *) corollary chosenAllocationEquivalence: assumes "card N > 0" and "distinct Ω" shows "chosenAllocation N Ω b r = chosenAllocationAlg N Ω b r" using assms allAllocationsBridgingLemma by (metis (no_types) chosenAllocationAlg_def comp_apply) corollary tiebidsBridgingLemma: assumes "x ∈ (N × (Pow Ω - {{}}))" shows "tiebids a N Ω x = tiebidsAlg a N Ω x" (is "?L=_") proof - have "?L = summedBidVector (maxbid a N Ω) N Ω x" by fast moreover have "...= summedBidVectorAlg (maxbidAlg a N Ω) N Ω x" using assms by (rule summedBidVectorEquivalence) ultimately show ?thesis unfolding tiebidsAlg_def by fast qed definition "tiebids'=tiebids" corollary tiebidsBridgingLemma': assumes "x ∈ (N × (Pow Ω - {{}}))" shows "tiebids' a N Ω x = tiebidsAlg a N Ω x" using assms tiebidsBridgingLemma tiebids'_def by metis abbreviation "resolvingBid' N G bids random == tiebids' (chosenAllocation N G bids random) N (set G)" lemma resolvingBidEquivalence: assumes "x ∈ (N × (Pow (set Ω) - {{}}))" "card N > 0" "distinct Ω" shows "resolvingBid' N Ω b r x = resolvingBidAlg N Ω b r x" using assms chosenAllocationEquivalence tiebidsBridgingLemma' resolvingBidAlg_def by metis lemma sumResolvingBidEquivalence: assumes "card N > 0" "distinct Ω" "a ⊆ (N × (Pow (set Ω) - {{}}))" shows "sum (resolvingBid' N Ω b r) a = sum (resolvingBidAlg N Ω b r) a" (is "?L=?R") proof - have "∀x∈a. resolvingBid' N Ω b r x = resolvingBidAlg N Ω b r x" using assms resolvingBidEquivalence by blast thus ?thesis using sum.cong by force qed lemma resolvingBidBridgingLemma: assumes "card N > 0" "distinct Ω" "a ⊆ (N × (Pow (set Ω) - {{}}))" shows "sum (resolvingBid N Ω b r) a = sum (resolvingBidAlg N Ω b r) a" (is "?L=?R") proof - have "?L=sum (resolvingBid' N Ω b r) a" unfolding tiebids'_def by fast moreover have "...=?R" using assms by (rule sumResolvingBidEquivalence) ultimately show ?thesis by simp qed lemma allAllocationsInPowerset: "allAllocations N Ω ⊆ Pow (N × (Pow Ω - {{}}))" by (metis PowI allocationPowerset subsetI) corollary resolvingBidBridgingLemmaVariant1: assumes "card N > 0" "distinct Ω" "a ∈ allAllocations N (set Ω)" shows "sum (resolvingBid N Ω b r) a = sum (resolvingBidAlg N Ω b r) a" proof - have "a ⊆ N × (Pow (set Ω) - {{}})" using assms(3) allAllocationsInPowerset by blast thus ?thesis using assms(1,2) resolvingBidBridgingLemma by blast qed corollary resolvingBidBridgingLemmaVariant2: assumes "finite N" "distinct Ω" "a ∈ maximalStrictAllocations N (set Ω) b" shows "sum (randomBids N Ω b r) a = sum (randomBidsAlg N Ω b r) a" proof - have "card (N∪{seller}) > 0" using assms(1) sup_eq_bot_iff insert_not_empty by (metis card_gt_0_iff finite.emptyI finite.insertI finite_UnI) moreover have "distinct Ω" using assms(2) by simp moreover have "a ∈ allAllocations (N∪{seller}) (set Ω)" using assms(3) by fastforce ultimately show ?thesis unfolding randomBidsAlg_def by (rule resolvingBidBridgingLemmaVariant1) qed corollary tiebreakingGivesSingleton: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "card (argmax (sum (randomBidsAlg N Ω b r)) (maximalStrictAllocations N (set Ω) b)) = 1" proof - have "∀ a ∈ maximalStrictAllocations N (set Ω) b. sum (randomBids N Ω b r) a = sum (randomBidsAlg N Ω b r) a" using assms(3,1) resolvingBidBridgingLemmaVariant2 by blast then have "argmax (sum (randomBidsAlg N Ω b r)) (maximalStrictAllocations N (set Ω) b) = argmax (sum (randomBids N Ω b r)) (maximalStrictAllocations N (set Ω) b)" using argmaxEquivalence by blast moreover have "card ... = 1" using assms by (rule vcgaDefinitenessVariant) ultimately show ?thesis by simp qed theorem maximalAllocationBridgingTheorem: assumes "finite N" "distinct Ω" shows "maximalStrictAllocations N (set Ω) b = maximalStrictAllocationsAlg N Ω b" proof - let ?N = "{seller} ∪ N" have "card ?N>0" using assms(1) by (metis (full_types) card_gt_0_iff finite_insert insert_is_Un insert_not_empty) thus ?thesis using assms(2) allAllocationsBridgingLemma by metis qed theorem vcgaAlgDefinedness: assumes "distinct Ω" "set Ω ≠ {}" "finite N" shows "card (argmax (sum (randomBidsAlg N Ω b r)) (maximalStrictAllocationsAlg N Ω b)) = 1" proof - have "card (argmax (sum (randomBidsAlg N Ω b r)) (maximalStrictAllocations N (set Ω) b)) = 1" using assms by (rule tiebreakingGivesSingleton) moreover have "maximalStrictAllocations N (set Ω) b = maximalStrictAllocationsAlg N Ω b" using assms(3,1) by (rule maximalAllocationBridgingTheorem) ultimately show ?thesis by metis qed end