(*
Auction Theory Toolbox (http://formare.github.io/auctions/)
Authors:
* Christoph Lange
Dually licenced under
* Creative Commons Attribution (CC-BY) 3.0
* ISC License (1-clause BSD License)
See LICENSE file for details
(Rationale for this dual licence: http://arxiv.org/abs/1107.3212)
*)
header {* Soundness verification of the combinatorial Vickrey auction *}
theory CombinatorialVickreyAuctionSoundness
imports
CombinatorialVickreyAuction
CombinatorialAuctionProperties
begin
section {* left-total *}
text {* The combinatorial Vickrey auction in relational form is left-total.
Note that in Isabelle/HOL's logic of total functions, an outcome (allocation @{term x} and
@{term p}) will always trivially exist, as they are return values of functions. It is more
interesting to prove that the outcome of our auction is \emph{well-defined}. *}
lemma left_total:
fixes t::tie_breaker_rel (* no need to assume anything about t *)
shows "left_total (nVCG_auctions t) valid_input"
proof (rule left_totalI)
fix G::goods and N::"participant set" and b::bids
assume assm: "valid_input G N b"
def x \ "winning_allocation_rel G N t b" (* these are function values and therefore guaranteed to exist *)
def p \ "payments_rel G N t b"
from assm x_def p_def have "nVCG_pred t G N b x p" unfolding nVCG_pred_def by blast
then show "\ x p . ((G, N, b), (x, p)) \ nVCG_auctions t"
unfolding nVCG_auctions_def using pred_imp_rel_all by metis
qed
section {* right-unique *}
text {* splits the outcome of a combinatorial Vickrey auction in relational form into
allocation and payment *}
lemma split_outcome:
assumes "((G', N', b'), (x'', p'')) \ nVCG_auctions t"
shows "x'' = winning_allocation_rel G' N' t b' \ p'' = payments_rel G' N' t b'"
proof -
from assms have "pred_tup (nVCG_pred t) ((G', N', b'), (x'', p''))"
unfolding nVCG_auctions_def rel_all_def by fast
then show "x'' = winning_allocation_rel G' N' t b' \ p'' = payments_rel G' N' t b'"
unfolding pred_tup_def nVCG_pred_def by blast
qed
text {* The combinatorial Vickrey auction in relational form is right-unique. This is easy to
show because its outcome is defined by two functions, which are right-unique by construction. *}
lemma right_unique:
fixes t::tie_breaker_rel (* no need to assume anything about t *)
shows "right_unique (nVCG_auctions t) valid_input"
proof (rule right_uniqueI)
fix G::goods and N::"participant set" and b::bids
(* As right-uniqueness is so easy to prove in this case,
it turns out that we don't need the additional assumption "valid_input G N b". *)
fix x::allocation_rel and x'::allocation_rel and p::payments and p'::payments
assume "((G, N, b), (x, p)) \ nVCG_auctions t"
then have xp: "x = winning_allocation_rel G N t b \ p = payments_rel G N t b" by (rule split_outcome)
assume "((G, N, b), (x', p')) \ nVCG_auctions t"
then have xp': "x' = winning_allocation_rel G N t b \ p' = payments_rel G N t b" by (rule split_outcome)
from xp xp' show "x = x' \ p = p'" by fast
qed
section {* well-defined outcome *}
text {* Payments are well-defined if every bidder has to pay a non-negative amount. *}
(* CL: not sure whether we should define this here, or in CombinatorialAuction. Maybe it is useful
for other combinatorial auctions too. *)
definition wd_payments :: "participant set \ payments \ bool"
where "wd_payments N p \ (\ n \ N . p n \ 0)"
text {* The outcome of the combinatorial Vickrey auction is well-defined, if the allocation
is well-defined and the payments are non-negative. *}
definition wd_alloc_pay :: "goods \ participant set \ bids \ allocation_rel \ payments \ bool"
where "wd_alloc_pay G N b x p \ wd_allocation G N x \ wd_payments N p"
text {* The combinatorial Vickrey auction is well-defined. *}
lemma wd_outcome:
fixes t::tie_breaker_rel
assumes "tie_breaker t"
shows "wd_outcome (nVCG_auctions t) valid_input wd_alloc_pay"
proof (rule wd_outcomeI)
fix G N b x p
assume "((G, N, b), (x, p)) \ nVCG_auctions t"
then have xp: "x = winning_allocation_rel G N t b \ p = payments_rel G N t b" by (rule split_outcome)
assume valid: "valid_input G N b"
from xp have x_unfolded: "x = t (arg_max' (value_rel b) (possible_allocations_rel G N))"
unfolding winning_allocation_rel.simps winning_allocations_rel_def
by simp
from xp (* to use Max_in, we need additional assumptions about N and G, so that \ is non-empty *)
have p_unfolded: "p = (\n . (Max ((value_rel b) ` (possible_allocations_rel G (N - {n}))))
- (\ m \ N - {n} . b m (eval_rel_or (x\) m {})))" by fastforce
have "wd_allocation G N x"
proof -
have "no_good_allocated_twice G x"
proof -
have alloc_non_empty: "arg_max' (value_rel b) (possible_allocations_rel G N) \ {}"
proof -
from valid have "card G > 0" and "card N > 0" unfolding valid_input_def by simp_all
from `card G > 0` have "G \ {}" by force
then have "is_partition_of {G} G" by (rule set_partitions_itself)
then have *: "{G} \ all_partitions G" unfolding all_partitions_def by (rule CollectI)
moreover have "injections {G} N \ {}"
proof -
have "finite {G}" by simp
moreover have "finite N" using `card N > 0` by (rule card_ge_0_finite)
moreover have "card {G} \ card N" using `card N > 0` by auto
ultimately show ?thesis by (rule injections_exist)
qed
ultimately have "(* \ { injections Y N | Y . Y \ all_partitions G } = *)
possible_allocations_rel G N \ {}"
by (auto simp add: Union_map_non_empty)
moreover have "finite (possible_allocations_rel G N)" sorry
(* prove using finite_UN_I *)
ultimately have "arg_max' (value_rel b) (possible_allocations_rel G N) \ {}"
by (rule arg_max'_non_empty_iff)
then show ?thesis by fast
qed
with assms x_unfolded have "x \ arg_max' (value_rel b) (possible_allocations_rel G N)"
using tie_breaker_def by smt
then have "x \ { x \ \ { injections Y N | Y . Y \ all_partitions G } .
value_rel b x = Max ((value_rel b) ` \ { injections Y N | Y . Y \ all_partitions G }) }" by simp
then have "x \ \ { injections Y N | Y . Y \ all_partitions G }
\ value_rel b x = Max ((value_rel b) ` \ { injections Y N | Y . Y \ all_partitions G })"
by (rule CollectD)
then have x_alloc: "x \ \ { injections Y N | Y . Y \ all_partitions G }" ..
have "is_partition_of (Domain x) G"
proof -
from x_alloc have "\ Y \ all_partitions G . x \ injections Y N" by (rule Union_map_member)
then obtain Y where part: "Y \ all_partitions G" and inj: "x \ injections Y N" by fast
from part have "is_partition_of Y G" unfolding all_partitions_def by (rule CollectD)
moreover have "Domain x = Y" using inj unfolding injections_def by simp
ultimately show ?thesis by blast
qed
show ?thesis sorry
qed
moreover have "\ Domain x \ G" sorry
moreover have "Range x \ N" sorry
ultimately show ?thesis unfolding wd_allocation_def by blast
qed
moreover have "wd_payments N p" unfolding wd_payments_def
proof
fix n assume "n \ N"
then show "p n \ 0" sorry
qed
ultimately show "wd_alloc_pay G N b x p" unfolding wd_alloc_pay_def ..
qed
section {* Overall soundness *}
text {* The combinatorial Vickrey auction is sound. *}
theorem sound:
fixes t::tie_breaker_rel (* no need to assume anything about t *)
assumes "tie_breaker t"
shows "sound (nVCG_auctions t) valid_input wd_alloc_pay"
proof -
note left_total
moreover note right_unique
moreover have "wd_outcome (nVCG_auctions t) valid_input wd_alloc_pay"
using assms by (rule wd_outcome)
ultimately show ?thesis unfolding sound_def by blast
qed
end