Re: [isabelle] how to state that a function is well-defined?



Hi John,

2013-11-01 19:41 John Wickerson:
> How can I state a lemma that simply says my function is "well-defined"? I mean: suppose I define
>
> definition "foo x == x ! 0"
>
> I want to say that foo is "well-defined" on all inputs other than the empty list. I'm imagining something like
>
> lemma "x ≠ [] ⟹ ∃!y. foo x = y"
>
> but that's true for any foo.

I'm not sure what your concrete application is, but we have experienced
the same problem in the concrete setting of proving the well-definedness
of an auction.  To our most general understanding, an auction is a
relation of inputs (participants' bids on available goods) to outcomes
(an allocation of goods to participants, and a specification of who has
to pay how much to the auctioneer).  Of such a relation we seek to prove
three properties:

1. it is left-total on valid inputs, i.e. for any such input there
exists an outcome
2. these outcomes are unique.  (1) and (2) means that the auction
relation is a function.
3. the outcomes satisfy some additional properties.  Note that we call
these properties "well-definedness", whereas we use "soundness" to refer
to what you call "well-definedness".

OK, but one concrete auction for which we'd like to prove this is
already stated as a HOL function.  This means, taking into account what
Larry explained, that (1) and (2) are easy to prove, but that you don't
gain much from this close-to-vacuous observation in practice.  Thus …

2013-11-01 20:00 Lawrence Paulson:
> You may find that some properties of foo only hold for non-empty lists, that’s all.

… (3) is indeed the only interesting part of our proof.  For the source
see
https://github.com/formare/auctions/blob/master/isabelle/Auction/CombinatorialVickreyAuctionSoundness.thy,
and for an explanation (to an audience without a theorem proving
background) see section 5 of
https://codex.cs.bham.ac.uk/svn/mmk/formare/pubs/wine2013/130719n-VCG.pdf (use
username/password guest/guest).  Note that both are work in progress.

Cheers,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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