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



"But it is easy to write definitions that aren't satisfiable, or that imply trivialities."

I agree absolutely. People often imagine that it's impossible to make a mistake if you use a formal proof assistant, but erroneous definitions and unrealistic models are commonplace.

Larry Paulson


On 12 Nov 2012, at 23:08, "Tim (McKenzie) Makarios" <tjm1983 at gmail.com> wrote:

> I've had a look at your work, and found it interesting.
> 
> One thing that I noticed was that you defined what it means to be a
> second_price_auction, and you proved various things about functions that
> satisfy this definition, but you never showed that the definition was
> satisfiable.
> 
> This isn't an inconsequential detail; at first, I thought you'd got the
> definition wrong, and that "second_price_auction n x p" implied n < 2.
> When I tried to prove it, I finally noticed that your allocation and
> payment functions depend on the set of bids.  But it is easy to write
> definitions that aren't satisfiable, or that imply trivialities.
> 
> So I decided to prove that your second_price_auction was satisfiable for
> n > 0.  See attached for the proof.
> 
> Also, you made a comment about removing an element from a set.  Given a
> set A, the set of all the elements of A except x can be written as
> "A - {x}"
> 
> I have a feeling that there was something else I was going to comment
> on, but I should go and have lunch, and write again if I remember it.
> 
> Tim
> <><
> <Vickrey_Extras.thy>






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