Email Gateway (Aug 19 2022 at 12:37): Email Gateway (Aug 19 2022 at 12:37):From: John Wickerson <johnwickerson@cantab.net>
This is a really basic question, and I'll probably kick myself once somebody tells me the answer.
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.
Thanks!
john
Email Gateway (Aug 19 2022 at 12:47):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m afraid that this concept of "well-defined” does not exist in higher-order logic. You may find that some properties of foo only hold for non-empty lists, that’s all.
Larry Paulson
Email Gateway (Aug 19 2022 at 12:48):From: Christoph LANGE <math.semantic.web@gmail.com>
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:
it is left-total on valid inputs, i.e. for any such input there
exists an outcome
these outcomes are unique. (1) and (2) means that the auction
relation is a function.
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
Last updated: Apr 19 2024 at 04:17 UTC