(*
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 {* Some properties that combinatorial auctions can have *}
theory CombinatorialAuctionProperties
imports CombinatorialAuction
begin
(* TODO CL: revise the following as per https://github.com/formare/auctions/issues/19 *)
section {* Soundness *}
subsection {* Well-defined outcome *}
text {* No good is allocated to more than one bidder. Given our formalisation of allocations
(relations between partitions of the set of goods and the set of bidders), this means that
for each good the image of the equivalence class(es), in which the good occurs, under
the allocation relation is @{const trivial}. *}
definition no_good_allocated_twice :: "goods \ allocation_rel \ bool"
where "no_good_allocated_twice G x \ (\ g \ G . trivial (x `` { P \ Domain x . g \ P }))"
text {* well-definedness of an allocation, given the goods and participants: all goods are
allocated within the set of participants; nothing is allocated twice. *}
(* TODO CL: allow for partial allocation: in this case, Domain x needs to be a
partition of a _subset_ of G *)
(* CL: Here, we do not care whether every good actually gets allocated. Our current implementation
does this, but I'm not sure this is a criterion against which the implementation should be verified. *)
definition wd_allocation :: "goods \ participant set \ allocation_rel \ bool"
where "wd_allocation G N x \
no_good_allocated_twice G x \
\ Domain x \ G (* only available goods are allocated *) \
Range x \ N (* goods are only allocated among the bidders *)"
type_synonym outcome_well_definedness = "goods \ participant set \ bids \ allocation_rel \ payments \ bool"
definition wd_outcome :: "combinatorial_auction_rel \ input_validity \ outcome_well_definedness \ bool"
where "wd_outcome A valid wd_outcome_pred \
(\ ((G::goods, N::participant set, b::bids), (x::allocation_rel, p::payments)) \ A .
valid G N b \ wd_outcome_pred G N b x p)"
text{* introduction rule for @{const wd_outcome}, to facilitate proofs of well-definedness of the outcome *}
lemma wd_outcomeI:
assumes "\ G N b x p . ((G, N, b), (x, p)) \ A \ valid G N b \ wd_outcome_pred G N b x p"
shows "wd_outcome A valid wd_outcome_pred"
(* CL: The following proof (tried before we added the "valid" premise) takes 82 ms on my machine:
using assms unfolding wd_outcome_def by (smt prod_caseI2 prod_caseI2') *)
unfolding wd_outcome_def
proof
fix T
assume "T \ A"
then obtain input out where T: "T = (input, out)" using PairE by blast
from T obtain G N b where input: "input = (G, N, b)" using prod_cases3 by blast
from T obtain x p where out: "out = (x, p)" using PairE by blast
from input out T `T \ A` have "((G, N, b), (x, p)) \ A" by fastforce
then have "valid G N b \ wd_outcome_pred G N b x p" using assms by fast
with input out T
show "case T of (input, out) \ (\ (G, N, b) (x, p) . valid G N b \ wd_outcome_pred G N b x p) input out"
using split_conv by force
qed
subsection {* Left-totality *}
text{* Left-totality of a combinatorial auction in relational form: for each valid bid vector
there exists some outcome (not necessarily unique nor well-defined). *}
definition left_total :: "combinatorial_auction_rel \ input_validity \ bool"
where "left_total A valid \ { (G, N, b) . valid G N b } \ Domain A"
text{* introduction rule for @{const left_total}, to facilitate left-totality proofs *}
lemma left_totalI:
assumes "\ G N b . valid G N b \ (\ x p . ((G, N, b), (x, p)) \ A)"
shows "left_total A valid"
using assms unfolding left_total_def by fast
subsection {* Right-uniqueness *}
text{* Right-uniqueness of a combinatorial auction in relational form: for each valid bid vector,
if there is an outcome, it is unique. This definition makes sense because we know @{thm runiq_restrict}. *}
definition right_unique :: "combinatorial_auction_rel \ input_validity \ bool"
where "right_unique A valid \ runiq (A || { (G, N, b) . valid G N b })"
lemma right_uniqueI:
assumes "\ G N b x x' p p' . valid G N b
\ ((G, N, b), (x, p)) \ A \ ((G, N, b), (x', p')) \ A
\ x = x' \ p = p'"
shows "right_unique A valid"
proof -
{
fix input
assume 1: "input \ {(G, N, b) . valid G N b}"
then obtain G N b where input: "input = (G, N, b)" by (auto simp: prod_cases3)
with 1 have adm: "valid G N b" by fast
fix out out'
assume 2: "(input, out) \ A \ (input, out') \ A"
then obtain x p x' p' where out: "out = (x, p)" and out': "out' = (x', p')" by fastforce
from input 2 out have rel: "((G, N, b), (x, p)) \ A" by fast
from input 2 out' have rel': "((G, N, b), (x', p')) \ A" by fast
from adm rel rel' out out' have "out = out'" using assms by force
}
then have "\ input \ {(G, N, b) . valid G N b} . \ out out' . (input, out) \ A \ (input, out') \ A \ out = out'" by blast
then show ?thesis unfolding right_unique_def using runiq_restrict by blast
qed
subsection {* Overall soundness *}
text {* A combinatorial auction in relational form is sound if it is left-total, right-unique
and yields a well-defined outcome. *}
definition sound :: "combinatorial_auction_rel \ input_validity \ outcome_well_definedness \ bool"
where "sound A valid wd_outcome_pred \
left_total A valid \
right_unique A valid \
wd_outcome A valid wd_outcome_pred"
end