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

[Christoph LANGE]

Dear Isabelle community,

We are pleased to announce our first step towards building an auction
theory toolbox: a complete formalisation of William Vickrey's 1961
theorem on second price auctions (see
http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/Vickrey.thy
for the code). This has been done as part of our ForMaRE project (Formal
Mathematical Reasoning in Economics); see
http://cs.bham.ac.uk/research/projects/formare/.

This mail outlines our result and our next steps. We'd also like to ask
you for some Isabelle-specific advice on our next steps, and to share
and discuss the experiences we've had.

AUCTION THEORY

In second price (or Vickrey) auctions, bidders submit sealed bids; the
highest bidder wins, and pays the highest bid of the _remaining_ bids;
the losers pay nothing. (See
http://en.wikipedia.org/wiki/Vickrey_auction for more information,
including a discussion of variants used by eBay, Google and Yahoo!.)
Vickrey proved that 'truth-telling' (i.e. submitting a bid equal to
one's actual valuation of the good) was a weakly dominant strategy. This
means that no bidder could do strictly better by bidding above or below
its valuation _whatever_ the other bidders did. Thus, the auction is
also efficient, awarding the item to the bidder with the highest valuation.

Vickrey was awarded Economics' Nobel prize in 1996 for his work. High
level versions of his theorem, and 12 others, were collected in Eric
Maskin's 2004 review of Paul Milgrom's influential book on auction
theory ("The unity of auction theory: Milgrom’s master class", Journal
of Economic Literature, 42(4), pp. 1102–1115). Maskin himself won the
Nobel in 2007.

OUR RESULT AND PLANS

We began our formalisation by rewriting Maskin's proof in a more
machine-friendly format
(http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/vickrey-paper.pdf).
As the proof is case based, this allowed a simple translation to Isabelle.

We plan to formalise the other theorems in Maskin's paper, adding them
to an auction theory toolbox, with the eventual goal of proving new
theorems about old and new types of auctions.

This will require both re-arrangements of our current formalisation into
multiple theories, and generalisations. For example, we now model
bidders as an integer range 1,…,n, and their bids as an n-vector of real
numbers (actually, as a function from 1,…,n to reals). However,
Vickrey's theorem does not assume any _order_ among the participants. It
is thus sufficient to treat them as a set, but it must be possible to
remove elements from such a set (which we currently do by skipping
components of a vector).

QUESTIONS FOR ISABELLE COMMUNITY

We would like to contribute our formalisation to the AFP, but are unsure
about the procedure: once accepted and published, can we submit updates?
We could imagine submitting this formalisation soon (as it is
self-contained and covers a relevant field), but still we are planning
to evolve and improve it.

As this was our first major Isabelle formalisation, we may have got a
lot of things wrong. We would be grateful if any of you were able to
look into the source and tell us of any "anti-patterns" we shouldn't
use. I will also follow up on this mail with a number of mails asking
specific questions on how certain things in Isabelle work, and with some
jEdit bug reports.

COMMENTS ON ISABELLE EXPERIENCE

Overall, we have been quite satisfied with how Isabelle works so far,
but we are also trying to take the perspective of our end users
(economists with little computer science background), who may find it
harder to use. Here are some preliminary notes (some of which may be
based on wrong assumptions):

* jEdit gives good feedback about syntax errors and certain semantic errors.
* When developing the structure of a proof, "show ?thesis sorry"
placeholders proved useful.
* sledgehammer is very useful for finding justifications for proof steps.
* Local renamings with "let" proved useful in complex proofs.
* It would be nice to be able to introduce proper types (not just
type_synonyms) for things such as non-negative real vectors.
* In statements such as "!x. p x --> q x" it is tedious (and always the
same) to break their structure down to a level where the actually
interesting work starts.

Cheers, and thanks in advance for your feedback,

Christoph & Colin & Manfred

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

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
2–5 April 2013, Exeter, UK. Deadlines 10 Dec (stage 1), 14 Jan (st. 2)
http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/

[Lawrence Paulson]

I greatly welcome this news. Both the general application area and the particular proof development seem very important.

On 31 Oct 2012, at 18:28, Christoph LANGE <c.l...@cs.bham.ac.uk> wrote:

> * In statements such as "!x. p x --> q x" it is tedious (and always the same) to break their structure down to a level where the actually interesting work starts.

It is almost never necessary or helpful to state a theorem in that format. I suggest

lemma "p x ==> q x"

for a straightforward proof, or

lemma assumes "p x" shows "q x"

for a more complicated structured proof.

Larry Paulson

[Christoph LANGE]

2012-10-31 20:09 Lawrence Paulson:

> On 31 Oct 2012, at 18:28, Christoph LANGE <c.l...@cs.bham.ac.uk> wrote:
>> * In statements such as "!x. p x --> q x" it is tedious (and always the same) to break their structure down to a level where the actually interesting work starts.
>
> It is almost never necessary or helpful to state a theorem in that format.

Thanks for your advice! However simply changing my statements to …

> I suggest
>
> lemma "p x ==> q x"
>
> for a straightforward proof, or
>
> lemma assumes "p x" shows "q x"
>
> for a more complicated structured proof.

… such a structure doesn't always work; I think the proofs will also
need some adaptation.

The following lemma (reduced to the structural outline) has a
(anti-)pattern that is typical for my formalisation:

lemma skip_index_keeps_non_negativity :
fixes n::nat and v::real_vector
assumes non_empty: "n > 0"
and non_negative: "non_negative_real_vector n v"
shows "\<forall>i::nat . in_range n i \<longrightarrow>
non_negative_real_vector (n-(1::nat)) (skip_index v i)"
proof
fix i::nat
show "in_range n i \<longrightarrow> non_negative_real_vector
(n-(1::nat)) (skip_index v i)"
proof
assume "in_range n i"
...
show "non_negative_real_vector (n-(1::nat)) (skip_index v i)" sorry
qed
qed

How would I have to adapt the proof when rephrasing the statement as
shows "in_range n i \<Longrightarrow> ..." ?

(I'll be happy to accept "RTFM" as an answer, if you could give me a
pointer.)

Cheers, and thanks,

Christoph

[Tim (McKenzie) Makarios]

> We would like to contribute our formalisation to the AFP, but are unsure about the procedure: once accepted and published, can we submit updates?

Yes; see http://afp.sourceforge.net/updating.shtml

> * It would be nice to be able to introduce proper types (not just type_synonyms) for things such as non-negative real vectors.

Have you seen section 8.5.2 of tutorial.pdf in Isabelle's doc folder?
Perhaps there's also other documentation in another file; if so, I hope
someone else knows where and points you to it.

I'm quite interested in what you're doing; after working with Isabelle
for my Master's project, I'm now musing about auction theory:
http://wp.me/p2IaW7-W (I'm not trained in economics, so please be
gentle, but please do comment on my musings if you think I'm in error,
or if you have anything else to say about them.) Consequently, I
decided to have a look at your Vickrey theory. In preparation for this,
I tried running Isabelle's document preparation system on Vickrey.thy
(see chapter 4 of isar-ref.pdf, and possibly other parts of Isabelle's
documentation). Unfortunately, it didn't work at first, for a couple of
reasons.

First, Vickrey.thy didn't end with "end", which was easy to fix.

Second, your "text {* ... *}" portions don't always contain valid LaTeX.
I made minimal changes to get your document to compile, but I haven't
had time to read it yet. I've attached my edited version of your
Vickrey.thy, so you can see what changes I've made. I've made almost no
effort to make it look as you intended --- only to make it compile.

Tim
<><

[Christian Sternagel]

Dear Christoph,

Consider the proofs:

lemma 1:
"ALL i. i < length xs --> xs ! i = hd (drop i xs)"
proof
fix i
show "i < length xs --> xs ! i = hd (drop i xs)"
proof
assume "i < length xs"
then show "xs ! i = hd (drop i xs)"
by (induct i arbitrary: xs) (case_tac xs, simp_all)+
qed
qed
thm 1
thm 1 [rule_format]


lemma 2:
"!!i. i < length xs ==> xs ! i = hd (drop i xs)"
proof -
fix i
assume "i < length xs"
then show "xs ! i = hd (drop i xs)"
by (induct i arbitrary: xs) (case_tac xs, simp_all)+
qed
thm 2

lemma 3:
assumes "i < length xs"
shows "xs ! i = hd (drop i xs)"
using assms
by (induct i arbitrary: xs) (case_tac xs, simp_all)+
thm 3

I hope the example proofs still cover the structure that was important
to you (I changed them only to have some lemma I could actually prove).
Note the following points:

1) In lemma 3 we do not explicitly all-quantify i, thus it is handled as
"arbitrary but fixed" throughout the proof (and implicitly
all-quantified after the proof is finished; in fact "thm 2" and "thm 3"
give exactly the same result). This can always be done when we do not
need to vary/instantiate i inside the proof itself.

2) The attribute [rule_format] turns (some) HOL connectives into Pure
connectives (which are used to present natural deduction style rules in
Isabelle, hence the name).

3) For Isar proofs (i.e., structured proofs, as opposed to
proof-scripts) the style of lemma 3 is the most idiomatic, if such a
style is not possible (since we need to generalize a variable like i),
then the style of lemma 2 is the next most idiomatic. As Larry already
pointed out, the style of lemma 1 is the least idiomatic nowadays.

hope that helps,

chris

[Lawrence Paulson]

You should look at the documentation on the induct/induction proof methods. They achieve the effect of performing induction on a formula such as

"\<forall>i::nat . P i \<longrightarrow> Q i"

while completely hiding the tedious manipulations of these logical connectives that would normally be required.

Larry Paulson

[Christoph LANGE]

Hi Makarius,

2012-11-01 02:07 Tim (McKenzie) Makarios:

> First, Vickrey.thy didn't end with "end", which was easy to fix.

I had no idea, as jEdit didn't warn me. Is this a bug or a feature?

Cheers,

[Christoph LANGE]

Hi Tim,

thanks for your reply! Colin has already covered your feedback on
auction theory; he is our expert for economics. Let me reply on the
Isabelle-specific things, with some more questions to everyone, covering:

* defining restrictions of existing types
* tutorial.pdf vs. isar-ref.pdf

2012-11-01 02:07 Tim (McKenzie) Makarios:

>> We would like to contribute our formalisation to the AFP, but are unsure about the procedure: once accepted and published, can we submit updates?
>
> Yes; see http://afp.sourceforge.net/updating.shtml

Thanks, and sorry; I should have noticed that on the AFP homepage. I
think that after another revision (according to the other feedback
collected here, plus some other things we wanted to do anyway), we will
submit.

>> * It would be nice to be able to introduce proper types (not just type_synonyms) for things such as non-negative real vectors.
>
> Have you seen section 8.5.2 of tutorial.pdf in Isabelle's doc folder?

I have, but wasn't sure whether/how it applies to what we are doing.
IIUC this is about defining completely new types from scratch, whereas
we are rather interested in restricting existing types.

Plus, a question to everyone reading this: I haven't worked with the
Tutorial too much, but mainly consulted the Isar Reference. The
Tutorial does proofs in the "apply(rule)" style, which we don't consider
helpful for our target audience; we prefer textbook style. Of course,
I'm sure, for "apply(rule)" proof there is a straightforward translation
to Isar, but for me, being a relative beginner, this is not yet _so_
straightforward.

> I'm quite interested in what you're doing; after working with Isabelle

> for my Master's project, I'm now musing about auction theory: …

Interesting! (I just can't add anything to Colin's comment.)

> In preparation for this,
> I tried running Isabelle's document preparation system on Vickrey.thy
> (see chapter 4 of isar-ref.pdf, and possibly other parts of Isabelle's
> documentation).

So far we haven't bothered to generate a document from our
formalisation, but I agree that we should soon do. I see that chapter
4.2 of the Tutorial also documents this. So I should learn how to do it.

> Second, your "text {* ... *}" portions don't always contain valid LaTeX.
> I made minimal changes to get your document to compile, but I haven't
> had time to read it yet. I've attached my edited version of your
> Vickrey.thy, so you can see what changes I've made.

Thanks for these!

> I've made almost no
> effort to make it look as you intended

Well, as I said, I have not yet _intended_ anything ;-)

[Tobias Nipkow]

Am 01/11/2012 13:38, schrieb Christoph LANGE:
> Plus, a question to everyone reading this: I haven't worked with the Tutorial
> too much, but mainly consulted the Isar Reference. The Tutorial does proofs in
> the "apply(rule)" style, which we don't consider helpful for our target
> audience; we prefer textbook style. Of course, I'm sure, for "apply(rule)"
> proof there is a straightforward translation to Isar, but for me, being a
> relative beginner, this is not yet _so_ straightforward.

If you look at the documentation page
http://isabelle.in.tum.de/documentation.html you will find that the first
document is the relatively new Programming and Proving in Isabelle/HOL, which
does cover structured proofs (which is why I wrote it). The Tutorial is now only
second choice because of the foucus on "apply".

Tobias

[Tobias Nipkow]

Am 31/10/2012 19:28, schrieb Christoph LANGE:
> * It would be nice to be able to introduce proper types (not just type_synonyms)
> for things such as non-negative real vectors.

If you want to restrict to a subset of a type wityhout creating a completely new
type, you must do that on the formula level with explicit assumptions in your
propositions.

Tobias

[Tobias Nipkow]

Great stuff, look forward to more of this.

A small random point: the definition

definition in_range ::
"nat \<Rightarrow> nat \<Rightarrow> bool" where
"in_range n i \<equiv> 1 \<le> i \<and> i \<le> n"

excludes 0. Unless you have some very good reason for starting at 1, I would
start at 0, which typically makes things smoother. For a start, you can just
write "i<n" instead of "in_range n i".

Tobias

Am 31/10/2012 19:28, schrieb Christoph LANGE:

[Tim (McKenzie) Makarios]

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
<><

[Lawrence Paulson]

"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

> <Vickrey_Extras.thy>

[Makarius]

On Thu, 1 Nov 2012, Christoph LANGE wrote:

> So far we haven't bothered to generate a document from our
> formalisation, but I agree that we should soon do. I see that chapter
> 4.2 of the Tutorial also documents this. So I should learn how to do
> it.

In addition, see

* http://isabelle.in.tum.de/dist/Isabelle2012/doc/system.pdf
Chapter 3: Presenting theories

* http://isabelle.in.tum.de/dist/Isabelle2012/doc/isar-ref.pdf
Chapter 4: Document preparation


Makarius

[Makarius]

On Wed, 31 Oct 2012, Christoph LANGE wrote:

> QUESTIONS FOR ISABELLE COMMUNITY
>
> We would like to contribute our formalisation to the AFP, but are unsure
> about the procedure: once accepted and published, can we submit updates?
> We could imagine submitting this formalisation soon (as it is
> self-contained and covers a relevant field), but still we are planning
> to evolve and improve it.

I am not an editor of AFP, but it is generally a good idea to refine and
consilidate some development several times, before entering the submission
process.

If you need a hosting platform for the development process, I can
recommend https://bitbucket.org/ (with Mercurial).

> As this was our first major Isabelle formalisation, we may have got a
> lot of things wrong. We would be grateful if any of you were able to
> look into the source and tell us of any "anti-patterns" we shouldn't
> use. I will also follow up on this mail with a number of mails asking
> specific questions on how certain things in Isabelle work, and with some
> jEdit bug reports.

Looking only briefly over your Vickrey.thy, it already looks quite good as
a start. There are many fine points to be considered; we should go
through it gradually and without attacking everything at the same time.


Since Christoph is also a CICM person, I would like to point out the MKM
2008 paper by myself and Stefan Berghofer on "Logic-free reasoning in
Isabelle/Isar". It shows how to deflate your theories by a significant
factor, by removing unnecessary fluff. (Informal people sometimes think
they are doing formal logic when writing a lot of logical connectives
around there meterial, but this is not the real point of it.)

When doing functional programming properly, you also don't write funny
tuple arguments all the time, just to please ousiders, you use currying.


Can you write your sources with 80 char per line, or 100 maximum? These
exceedingly long lines are hard to read. The physicial parameters of
cinema displays have changed a lot recently, but not the parameters of the
human brain.

jEdit is not very good at soft line-breaks, and it is better to layout
your formal sources explicitly yourself. (The jEdit indentation
facilities still need to be activated for Isar sources, like I did many
years ago for Proof General / Emacs.)


Makarius

[Christoph LANGE]

Hi Makarius, hi all,

@All: Let me slowly resume the discussion of your feedback about our
formalisation. The earlier feedback sent by others (thanks once more!)
is not forgotten, I will get back to this next week, but the points in
this mail are good for me to start with, as they don't require me to
learn a lot of new things.

2012-11-16 22:49 Makarius:

> Since Christoph is also a CICM person, I would like to point out the MKM
> 2008 paper by myself and Stefan Berghofer on "Logic-free reasoning in
> Isabelle/Isar". It shows how to deflate your theories by a significant
> factor, by removing unnecessary fluff.

Thanks for the pointer!

> (Informal people sometimes think
> they are doing formal logic when writing a lot of logical connectives
> around there meterial, but this is not the real point of it.)

Well, I actually didn't try to be as "formal" as possible, but I did not
yet know how to do it right. In several lemmas I started with a simpler
statement, e.g. just the right side of an implication, and put the left
side into "assumes" declarations, but then I wasn't able to reuse these
assumptions in the proof as expected. In the cumbersome way I ended up
doing it I got the work done at least – but of course I'll be excited to
learn about the nicer way of doing it, and how to avoid such pitfalls as
I mentioned.

> Can you write your sources with 80 char per line, or 100 maximum? These
> exceedingly long lines are hard to read. The physicial parameters of
> cinema displays have changed a lot recently, but not the parameters of
> the human brain.

OK, I will try; it should be possible to introduce line breaks where it
semantically makes sense.

But actually I'd like to blame half of the problem on this:

> jEdit is not very good at soft line-breaks,

Not having much previous jEdit experience I simply had hoped that a
modern editor would be good at that (even recent versions of dinosaurs
such as Emacs are), and somehow denied that it didn't work so well after
all.

End of rant; I don't want to start an editor war here.

> and it is better to layout
> your formal sources explicitly yourself. (The jEdit indentation
> facilities still need to be activated for Isar sources, like I did many
> years ago for Proof General / Emacs.)

Let me report a problem related to that: I tried at least to enable
auto-indentation, so that any new line would be indented as much as the
previous line. But with that I found that Isabelle didn't pick up the
changes I made. (This is roughly what I remember from trying it a few
weeks ago; if you'd like me to do some experiments and give a more
detailed report, I'm happy to do so.)

Cheers,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham

http://cs.bham.ac.uk/~langec/, Skype duke4701

[Makarius]

On Fri, 16 Nov 2012, Christoph LANGE wrote:

>> jEdit is not very good at soft line-breaks,
>
> Not having much previous jEdit experience I simply had hoped that a
> modern editor would be good at that (even recent versions of dinosaurs
> such as Emacs are), and somehow denied that it didn't work so well after
> all.

Depends what you mean by "modern" and "editor".

jEdit is a very capable "programmer's editor" is it advertizes itself, but
not a word processor. Program text is hardly ever soft-wrapped, so
relatively little has been invested in this area. It you take Isar
sources, things like {* ... *} are a separate token anyway, like " ... ".
Would you expect from a source-code editor to wrap lines within string
literals?

Nonetheless, I can myself imagine Isabelle/jEdit doing something for
text {* ... *} blocks within Isar source, but that has to be specific to
the language, meaning I have to sit down and provide that functionality.
(As I did already for many other things.)


Makarius

[Christoph LANGE]

Dear Larry, dear all,

I'm now back at our auction formalisation and catching up with emails.

I have taken into account the advice I got from you and the others;
basically I managed to change my statements from

shows "!i . p x --> q x"

to

fixes ... and i

assumes "p x"
shows "q x"

This and similar changes helped to shorten the overall formalisation
from 1145 to 1045 lines (see
http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/Vickrey.thy).
I'm sure I can do even better.

I have not yet made any further simplifications, such as doing a lot of
things at once in a style like

.. by (induct i arbitrary: xs) (case_tac xs, simp_all)+

that Chris used in his example of a lemma about lists. At the moment I
don't even know how to get started using such proof methods.

2012-11-01 12:03 Lawrence Paulson:

> You should look at the documentation on the induct/induction proof methods.

Where can I find that documentation? The Tutorial mainly uses
apply(induct_tac), which is probably something else. Is there a single,
up to date reference manual that documents all proof methods?

BTW, changing induction proofs to "assumes ... shows ..." did not always
make them shorter. Is there a way of not having to explicitly restate
the assumption for (Suc n) in the induction step?

E.g. I have one lemma of the following structure, which proves some
property of a function "fun maximum":

lemma maximum_sufficient :
fixes n::nat and ...
assumes assm1: "p n"
and assm2: "q n"
and assm3: "r n"
shows "s n"
using assms (* <-- now this became necessary,
otherwise even "case 0" would fail, but why? *)
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
(* and now I have to explicitly restate all assumptions: *)
assume assm1: "p (Suc n)"
assume assm2: "q (Suc n)"
assume assm3: "r (Suc n)"
...
show "s (Suc n)" ...
qed

Cheers, and thanks for any help,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham

http://cs.bham.ac.uk/~langec/, Skype duke4701

[Tobias Nipkow]

Am 22/11/2012 15:13, schrieb Christoph LANGE:
> Dear Larry, dear all,
>
> I'm now back at our auction formalisation and catching up with emails.
>
> I have taken into account the advice I got from you and the others; basically I
> managed to change my statements from
>
> shows "!i . p x --> q x"
>
> to
>
> fixes ... and i
> assumes "p x"
> shows "q x"

Unless you want to give the type of i, you don't need to fix it.

> This and similar changes helped to shorten the overall formalisation from 1145
> to 1045 lines (see
> http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/Vickrey.thy).
> I'm sure I can do even better.
>
> I have not yet made any further simplifications, such as doing a lot of things
> at once in a style like
>

> ... by (induct i arbitrary: xs) (case_tac xs, simp_all)+

>
> that Chris used in his example of a lemma about lists. At the moment I don't
> even know how to get started using such proof methods.
>
> 2012-11-01 12:03 Lawrence Paulson:
>> You should look at the documentation on the induct/induction proof methods.
>
> Where can I find that documentation? The Tutorial mainly uses
> apply(induct_tac), which is probably something else.

This is what I suggested to you 3 weeks back:

"If you look at the documentation page
http://isabelle.in.tum.de/documentation.html you will find that the first
document is the relatively new Programming and Proving in Isabelle/HOL, which
does cover structured proofs (which is why I wrote it). The Tutorial is now only
second choice because of the foucus on "apply"."

That is also where you find the induction method.

> Is there a single, up to
> date reference manual that documents all proof methods?

Yes, the reference manual (more or less).

> BTW, changing induction proofs to "assumes ... shows ..." did not always make
> them shorter. Is there a way of not having to explicitly restate the assumption
> for (Suc n) in the induction step?

Indeed, for inductions, the most convenient way is stating them as implications
(with ==>). The manuals above will also tell you about the naming conventions of
assumptions in each case.

Tobias

[Lars Noschinski]

On 22.11.2012 15:13, Christoph LANGE wrote:
> assumes assm1: "p n"
> and assm2: "q n"
> and assm3: "r n"
> shows "s n"
> using assms (* <-- now this became necessary,
> otherwise even "case 0" would fail, but why? *)
> proof (induct n)

[...]

> case (Suc n)
> (* and now I have to explicitly restate all assumptions: *)
> assume assm1: "p (Suc n)"
> assume assm2: "q (Suc n)"
> assume assm3: "r (Suc n)"
> ...

You don't need to restate your assumptions here: They are all stored in
"Suc" (or Suc.prems, which omits the hypotheses added by induction).

-- Lars

[Christoph LANGE]

2012-11-22 14:31 Tobias Nipkow:

>> fixes ... and i
>> assumes "p x"
>> shows "q x"
>
> Unless you want to give the type of i, you don't need to fix it.

Thanks! Now I'm not quite sure what's better style. On paper you do
not always give types, if it's clear from the context. But when it is
not clear, it helps to mention types explicitly.

> "If you look at the documentation page
> http://isabelle.in.tum.de/documentation.html you will find that the first
> document is the relatively new Programming and Proving in Isabelle/HOL, which
> does cover structured proofs (which is why I wrote it). The Tutorial is now only
> second choice because of the foucus on "apply"."

Sorry, I just had not yet got back to that old recommendation you made.
Indeed I had had a look into "Programming and Proving" meanwhile and
found it very instructive. Thanks!

> That is also where you find the induction method.

That's right, but "Programming and Proving" is not a full reference of
all proof methods and their options; that's what I was referring to.

>> Is there a single, up to
>> date reference manual that documents all proof methods?
>
> Yes, the reference manual (more or less).

OK, thanks, I see.

BTW, about "Programming and Proving": I had noticed this manual when I
got started with Isabelle, but then didn't take a closer look, as I was
misled by the "Programming". I thought it was some specific guide on
verifying functional programs.

> Indeed, for inductions, the most convenient way is stating them as implications
> (with ==>). The manuals above will also tell you about the naming conventions of
> assumptions in each case.

OK, I'll add this to my to-do list.

Cheers,

[Makarius]

On Thu, 22 Nov 2012, Christoph LANGE wrote:

> I'm now back at our auction formalisation and catching up with emails.
>

> http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/Vickrey.thy

A few more hints on the version that happens to be behind this inversion
link right now:

* 'definition' with Pure equality (==) is quite old-fashioned. Normally
you just use HOL = or its abbreviation for bool <-> here, as you would
for 'primrec', 'fun', 'function'

(In contrast HOL --> and ! are old-fashioned/cumbersome, where Pure
==> and !! would do the job better.)

* I recommend to put the whole 'head' of some definition on one line,
this works best with jEdit folding:

definition a :: A
where "a = t"

fun b :: B
where "b x = t"

Where the 'where' goes depends on the length of A and t; it is not
informative for the head, so I prefer to have it second by default.

* 'done' should be indented like the 'apply' script. Don't ask why,
Isar indentation is an arcane discipline, and still awaits tool
support in Isabelle/jEdit.

BTW, the shortest structured proof that is not a script looks like
this:

lemma A unfolding a_def b_def c_def auto

instead of your apply unfold, apply auto, done

* About your funny comments (* by contradiction *): according to the
Isar philosophy, you always strive to make things clear by formal
means, and avoid comments. Thus can be done by putting a suitable
"proof (rule ...)" standard step here.

According to my experience, informal or semi-formal people often have
problems to understand what not-introduction, not-elimination, and
classical reasoning means. The following examples explore this in the
formal playground:

notepad
begin

have "¬ A"
proof (rule notI)
assume A
then show False sorry
qed

next

have "¬ A" sorry
have A sorry
from `¬ A` and `A` have C by (rule notE)

from `¬ A` and `A` have C by contradiction
from `A` and `¬ A` have C by contradiction

next

have C
proof (rule ccontr)
assume "¬ C"
then show False sorry
qed

next

have C
proof (rule classical)
assume "¬ ?thesis"
then show ?thesis sorry
qed

next

have C
proof (rule classical)
assume "¬ ?thesis"
then have False sorry
then show ?thesis by (rule FalseE)
qed

end


Here the rule steps with notI, notE, FalseE have been made explicit for
illustration: these default rules are normally omitted, i.e. you would
just write 'proof' without anything or '..' in instead of 'by (rule ...)'.

The Isar method "contradiction" allows to present to two preconditions in
either order -- this often happens in practice. For notE the negated
formula has to come first, to eliminate it properly.

There is nothing special behind any of these intro/elim steps so far: just
plain intuitionistic natural deduction. Nonetheless, people sometimes
think that notI is "proof by contradiction", because they have to show
False in the end.

This might also stem from the ccontr rule above, which is often seen in
text books (without this Isabelle-specific name). I usually prefer the
one called "classical", because it lacks the builtin False step and
illustrates the brutality of classical reasoning in a pure way: you may
assume that the thesis does not hold, then you have to show that it holds.
The latter proof often works "by contradiction" in the above formal sense,
to explain once more while you might get confused informally.

Formally, everything should be clear at this pure Isar level, because
there is no magic built-in apart from higher-order unification and
proof-by-assumption to solve trivial "end-games" in natural deduction.


Makarius

[Christoph LANGE]

2012-11-22 16:04 Lars Noschinski:

Thanks, that's very helpful!

For readability I'd sometimes like to make it explicit to what
assumption I'm referring when there is more than one.

When explicitly restating them with 'assume "... (Suc n) ..."' that's no
problem. With "Suc" I found, e.g., Suc.prems(1) to work. A symbolic
name, e.g. Suc.prems(foo), if the original statement says 'assumes foo:
"..."', would be even nicer – but that's not possible, I suppose.

Cheers,

[Lars Noschinski]

On 22.11.2012 17:56, Makarius wrote:
> * 'definition' with Pure equality (==) is quite old-fashioned. Normally
> you just use HOL = or its abbreviation for bool <-> here, as you would
> for 'primrec', 'fun', 'function'
>
> (In contrast HOL --> and ! are old-fashioned/cumbersome, where Pure
> ==> and !! would do the job better.)

Is there actually a drawback when using == instead of = or is it a mere
matter of style? I like using Pure equality because it saves me a level
of parentheses when I have a binder on the right hand side.

> BTW, the shortest structured proof that is not a script looks like
> this:
>
> lemma A unfolding a_def b_def c_def auto

To avoid confusion: There is a "by" missing:

lemma A unfolding a_def b_def c_def by auto

> The Isar method "contradiction" allows to present to two preconditions
> in either order -- this often happens in practice. For notE the negated
> formula has to come first, to eliminate it properly.

Never saw this method before. I'll have a look.

-- Lars

[Florian Haftmann]

>> (In contrast HOL --> and ! are old-fashioned/cumbersome, where Pure
>> ==> and !! would do the job better.)
>
> Is there actually a drawback when using == instead of = or is it a mere
> matter of style? I like using Pure equality because it saves me a level
> of parentheses when I have a binder on the right hand side.

It is simpler:

a) Uniformity

definition foo :: …
where "foo … = …"

vs.

primrec foo :: …
where "foo … = …"
| …
| "foo … = …"

vs.

fun(ction) foo :: …
where "foo … = …"
| …
| "foo … = …"

b) Less symbols

Why care about »foo« anyway?

Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

[Christoph LANGE]

2012-11-22 15:59 Christoph LANGE:
> 2012-11-02 22:08 Tobias Nipkow:
>> It may still be a bit simpler to write
>> "1<=i & i <=n" instead of "in_range n i" - no need to expand in_range. In
>> general it is a good idea not to invent new constants for existing
>> concepts:
>> "in_range n i" is actually the same as "i : {1..n}".
> I have now followed your advice; thanks! Another advantage that is
> important to us is that it makes the code more readable.
>
> Overall it helped simplifying my formalisation; however there were some
> surprises.

Here is another surprise I forgot to mention. If you or anyone else
feel like it, please have a look into the attached file, from which I
removed everything else. (Note that the server where I put our whole
formalisation will be offline until tomorrow morning.)

In the last case of the case distinction, I would like to infer the fact
I call pred_is_component. I need this to continue with the proof.

Now I have been unable to infer pred_is_component directly. But I made
it work with a detour via in_range. (So, don't worry, my proof works –
it's just not _nice_.)

And when I define in_range as "i : {1..n}" instead "1 <= i /\ i <= n",
even that doesn't work.

Cheers,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham

http://cs.bham.ac.uk/~langec/, Skype duke4701

[Lars Noschinski]

On 22.11.2012 18:41, Florian Haftmann wrote:
>>> (In contrast HOL --> and ! are old-fashioned/cumbersome, where Pure
>>> ==> and !! would do the job better.)
>>
>> Is there actually a drawback when using == instead of = or is it a mere
>> matter of style? I like using Pure equality because it saves me a level
>> of parentheses when I have a binder on the right hand side.
>
> It is simpler:
>
> a) Uniformity

> b) Less symbols

Ok, these are stylistic reasons and both only hold when always using =,
and not <-> (<-> can be used for all of definition, primrec, fun(ction),
but only for boolean valued functions. And I don't like it for
definitions anyway ;)).

> Why care about »foo« anyway?

This I don't understand. The situation I'm talking about is

definition foo :: …
where "foo … = (∀x. …)"

vs.

definition foo :: …
where "foo … ≡ ∀x. …"

(there are also other cases)

-- Lars

[Florian Haftmann]

>>> Is there actually a drawback when using == instead of = or is it a mere
>>> matter of style? I like using Pure equality because it saves me a level
>>> of parentheses when I have a binder on the right hand side.
>>
>> It is simpler:
>>
>> a) Uniformity
>> b) Less symbols
>
> Ok, these are stylistic reasons and both only hold when always using =,
> and not <-> (<-> can be used for all of definition, primrec, fun(ction),
> but only for boolean valued functions. And I don't like it for
> definitions anyway ;)).

The matter <-> vs. = is orthogonal to == vs. =

>> Why care about »foo« anyway?

This should have read »Why care about »==« anyway?«. The statement is
that end-users need not to even now about »==« in most situations (the
only exception known to me are rules like split_paired_All (all?) where
you rewrite framework-level connectives). So why burden them with it?

[Tobias Nipkow]

Am 22/11/2012 17:15, schrieb Christoph LANGE:
> BTW, about "Programming and Proving": I had noticed this manual when I got
> started with Isabelle, but then didn't take a closer look, as I was misled by
> the "Programming". I thought it was some specific guide on verifying functional
> programs.

In a way it is. It starts from a functional programming perspective. If you have
a suggestion for a better title, let me know.

Tobias

[Christoph LANGE]

2012-11-23 06:55 Tobias Nipkow:

OK, got the point. Now I really can't imagine a better title.

But I could imagine a better _guidance_, both on the documentation
website (http://isabelle.in.tum.de/documentation.html) and in the
"doc/Contents" file of the Isabelle installation (at least I have
/usr/share/doc/isabelle-2012/doc/Contents when installing from the
Gentoo Linux package).

On the website, Prog&Prove is listed first, but under a section header
"Miscellaneous tutorials". The section title could be changed to
"Getting started", and each document link could be followed by a few
words of explanation, e.g.:

Programming and Proving in Isabelle/HOL – Isabelle by example; read
this first

Similarly, the doc/Contents file should not merely restate the _titles_
of the documents, but provide the same extra information.

[Makarius]

On Fri, 23 Nov 2012, Christoph LANGE wrote:

> But I could imagine a better _guidance_, both on the documentation
> website (http://isabelle.in.tum.de/documentation.html) and in the
> "doc/Contents" file of the Isabelle installation

> On the website, Prog&Prove is listed first, but under a section header
> "Miscellaneous tutorials". The section title could be changed to
> "Getting started", and each document link could be followed by a few
> words of explanation, e.g.:
>
> Programming and Proving in Isabelle/HOL – Isabelle by example; read this first

This assumes a closed model of the documentation, and a uniform
understanding of it that does not really exist. Isabelle has many
different manuals from many different angles looking at the system, and a
long time-span covered in the writing of the texts. Larry even goes as far
saying, that nobody reads manuals anyway. Nonetheless I spend myself a lot
of time to keep the main reference manuals up-to-date, with more and more
examples. And others have updated various tutorials over time.

Concerning "guidance", that is also an open issue for the Prover IDE. When
I start Netbeans, it guides me quickly through the process of producing a
simple Java program. Little of that is there in Isabelle/jEdit so far.
At least in Isabelle2012, you should get a near 100% success rate in
starting it up on your platform, whatever it is (excluding *BSD).

> at least I have /usr/share/doc/isabelle-2012/doc/Contents when
> installing from the Gentoo Linux package

Better ignore these home-made derivatives of the official Isabelle
distribution, they will always be 1 or 2 steps behind the real thing.

Many years ago, I was fond of making OS packages myself as a hobby, long
before Debian and Gentoo existed. It is rather pointless for Isabelle
now, because the distribution is constructed in a way what would be called
"portable application" these days. So you don't care about "installing"
it, you just put it somewhere and run it. (This annoys packagers, because
they become obsolete, but users usually like it.)


Makarius

[Alfio Martini]

>
> Larry even goes as far saying, that nobody reads manuals anyway.
> Nonetheless I spend myself a lot of time to keep the main reference manuals
> up-to-date, with more and more examples. And others have updated various
> tutorials over time.

Without all the Isabelle documentation, I would have no chance with
this wonderful software system.

So, I am especially thankful that they are well-written and continuously
updated and
maintained!

Best!

On Fri, Nov 23, 2012 at 11:05 AM, Makarius <maka...@sketis.net> wrote:

> On Fri, 23 Nov 2012, Christoph LANGE wrote:
>
> But I could imagine a better _guidance_, both on the documentation

>> website (http://isabelle.in.tum.de/**documentation.html<http://isabelle.in.tum.de/documentation.html>)

>> and in the "doc/Contents" file of the Isabelle installation
>>
>
> On the website, Prog&Prove is listed first, but under a section header
>> "Miscellaneous tutorials". The section title could be changed to "Getting
>> started", and each document link could be followed by a few words of
>> explanation, e.g.:
>>
>> Programming and Proving in Isabelle/HOL – Isabelle by example; read
>> this first
>>
>
> This assumes a closed model of the documentation, and a uniform
> understanding of it that does not really exist. Isabelle has many
> different manuals from many different angles looking at the system, and a
> long time-span covered in the writing of the texts. Larry even goes as far
> saying, that nobody reads manuals anyway. Nonetheless I spend myself a lot
> of time to keep the main reference manuals up-to-date, with more and more
> examples. And others have updated various tutorials over time.
>
> Concerning "guidance", that is also an open issue for the Prover IDE. When
> I start Netbeans, it guides me quickly through the process of producing a
> simple Java program. Little of that is there in Isabelle/jEdit so far. At
> least in Isabelle2012, you should get a near 100% success rate in starting
> it up on your platform, whatever it is (excluding *BSD).
>
>

> at least I have /usr/share/doc/isabelle-2012/**doc/Contents when

>> installing from the Gentoo Linux package
>>
>
> Better ignore these home-made derivatives of the official Isabelle
> distribution, they will always be 1 or 2 steps behind the real thing.
>
> Many years ago, I was fond of making OS packages myself as a hobby, long
> before Debian and Gentoo existed. It is rather pointless for Isabelle now,
> because the distribution is constructed in a way what would be called
> "portable application" these days. So you don't care about "installing"
> it, you just put it somewhere and run it. (This annoys packagers, because
> they become obsolete, but users usually like it.)
>
>
> Makarius
>

--
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

[Makarius]

On Thu, 22 Nov 2012, Lars Noschinski wrote:

> On 22.11.2012 17:56, Makarius wrote:
>> * 'definition' with Pure equality (==) is quite old-fashioned. Normally
>> you just use HOL = or its abbreviation for bool <-> here, as you would
>> for 'primrec', 'fun', 'function'
>>
>> (In contrast HOL --> and ! are old-fashioned/cumbersome, where Pure
>> ==> and !! would do the job better.)
>
> Is there actually a drawback when using == instead of = or is it a mere
> matter of style? I like using Pure equality because it saves me a level of
> parentheses when I have a binder on the right hand side.

Using == for definitions is one of these things that can be explained only
historically. Many many years ago, you would have used consts/defs or
even consts/axioms or even consts/rules to spell out definitional axioms
using directly the == primitive of Pure. Larry explained it > 20 yeas ago
as "Pure == is used to represent definitions".

If you look at modern times, a "definitional package" is some mechanism
that accepts a specification (via terms or propositions) about what should
be provided by the system by means of some derived definitional concept.
So in 'primrec' and 'fun' you state equations, and the system will give
them you as theorems (and more things), in 'inductive' you write rules
about some relation, and you get them as theorems for introduction (and
more things for elimination and induction).

Long ago, the old 'defs' primitive has been superseded by such a
definitional package called 'definition', to do the same for basic
definitions without pattern matching or recursion. So 'definition' is
more like 'function' or 'theorem' than the primitive def that happens at
the bottom. That foundation of the definition does use Pure ==
internally, but the user never has to see it in practice. In Isabelle2012
these primitive defs behind 'definition' are particulary hard to retrieve,
and nobody has noticed so far :-)


Makarius

[Tobias Nipkow]

Am 23/11/2012 11:49, schrieb Christoph LANGE:
> 2012-11-23 06:55 Tobias Nipkow:
>> Am 22/11/2012 17:15, schrieb Christoph LANGE:
>>> BTW, about "Programming and Proving": I had noticed this manual when I got
>>> started with Isabelle, but then didn't take a closer look, as I was misled by
>>> the "Programming". I thought it was some specific guide on verifying functional
>>> programs.
>>
>> In a way it is. It starts from a functional programming perspective. If you have
>> a suggestion for a better title, let me know.
>
> OK, got the point. Now I really can't imagine a better title.
>
> But I could imagine a better _guidance_, both on the documentation website
> (http://isabelle.in.tum.de/documentation.html) and in the "doc/Contents" file of
> the Isabelle installation (at least I have
> /usr/share/doc/isabelle-2012/doc/Contents when installing from the Gentoo Linux
> package).
>
> On the website, Prog&Prove is listed first, but under a section header
> "Miscellaneous tutorials". The section title could be changed to "Getting
> started", and each document link could be followed by a few words of
> explanation, e.g.:
>
> Programming and Proving in Isabelle/HOL – Isabelle by example; read this first

I think most of the titles are self-explanatory, and indicate that they are
special manuals. Except for the first two. But all of them come with an abstract
or intro, and prog-prove explains quite clearly what it is about (and mentions
that the second one is old fashioned). You might want to also have this abstract
on the web page, but that would require yet more mechanisms.

However, there is a small linguistic point, which you may or may not have
intended to make: "Miscellaneous" material usually comes at the end. These are
"Tutorials", no qualification. The next subsection isn't called "Miscellaneous
Reference Manuals" either, and the whole section is called "Tutorials and
manuals". Makarius, could you drop the "Miscellaneous", please?

Tobias

[Makarius]

On Thu, 22 Nov 2012, Christoph LANGE wrote:

> For readability I'd sometimes like to make it explicit to what
> assumption I'm referring when there is more than one.
>
> When explicitly restating them with 'assume "... (Suc n) ..."' that's no
> problem. With "Suc" I found, e.g., Suc.prems(1) to work. A symbolic
> name, e.g. Suc.prems(foo), if the original statement says 'assumes foo:
> "..."', would be even nicer – but that's not possible, I suppose.

Restating case/assume is not a big deal, it is done occasionally and not
bad style, only a bit redundant and less formally checked than could be
done otherwise.

To make it more tight, you can do it via literal fact references or the
corresponing "fact" method like this:

notepad
begin

fix n :: nat

have "P n"

proof (induct n)
case 0

then show ?case sorry
next
case (Suc n)
then show ?case sorry
qed

have "P n"

proof (induct n)
case 0

show "P 0" sorry
next
case (Suc n)
from `P n` show "P (Suc n)" sorry
qed

have "P n"

proof (induct n)
case 0

show "P 0" sorry
next
case (Suc n)
have "P n" by fact
then show "P (Suc n)" sorry
qed

have "P n"

proof (induct n)
case 0

show "P 0" sorry
next
case (Suc n)
assume "P n"
then show "P (Suc n)" sorry
qed

have "P n"
proof (induct n)
show "P 0" sorry
next
fix n
assume "P n"
then show "P (Suc n)" sorry
qed

end


BTW, according to the way the logical framework works, you can have
redundant 'assume' statements in your proof body, but not redundant 'fix'.
The "fix n" is already part of the case (Suc n). Another fix n would
postulate a different hyptothetical entity in the context, that is not the
same, and its assumptions unrelated to what you have already after
invoking the case.

The funny thing is that textbook logicians often omit the formal "fix n"
altogether. I've seen this even in some implementations of logic, where
the global absence of a declaration over the whole text is taken as an
implicit fix of a local variable.


Makarius

[Makarius]

On Fri, 23 Nov 2012, Tobias Nipkow wrote:

> However, there is a small linguistic point, which you may or may not
> have intended to make: "Miscellaneous" material usually comes at the
> end. These are "Tutorials", no qualification. The next subsection isn't
> called "Miscellaneous Reference Manuals" either, and the whole section
> is called "Tutorials and manuals". Makarius, could you drop the
> "Miscellaneous", please?

There has been a lot of fluctuation and historical jokes in that file.
At some point the main reference manuals where pushed to the end along
with the "Old Manuals". Then there were "Miscellaneous Tutorials" and
"Main Reference Manuals", with "main" counted among the tutorials. Now it
is "Miscellaneous Tutorials" and "Reference Manuals", with "main" included
in reference manuals, which might explain why the title lost its "Main".

So the next logical step is indeed "Tutorials" and "Reference Manuals" for
the coming release, to disentangle that a bit more.


Makarius

[Makarius]

On Thu, 22 Nov 2012, Lars Noschinski wrote:

> On 22.11.2012 18:41, Florian Haftmann wrote:
>>>> (In contrast HOL --> and ! are old-fashioned/cumbersome, where Pure
>>>> ==> and !! would do the job better.)
>>>
>>> Is there actually a drawback when using == instead of = or is it a mere
>>> matter of style? I like using Pure equality because it saves me a level
>>> of parentheses when I have a binder on the right hand side.
>>
>> It is simpler:
>>
>> a) Uniformity
>> b) Less symbols
>
> Ok, these are stylistic reasons and both only hold when always using =,
> and not <-> (<-> can be used for all of definition, primrec, fun(ction),
> but only for boolean valued functions. And I don't like it for
> definitions anyway ;)).

Recall that 'definition', 'primrec', 'fun', 'function' are all the same
category of "derived definitional concept", although of different strength
and power invested in the mechanisms behind it.


Makarius