Re: [isabelle] problem with opening proof



On Mon, 25 May 2009, Dr. Brendan Patrick Mahony wrote:

On 23/05/2009, at 7:13 PM, Makarius wrote:

You should be able to ignore the "intro" and "elim" methods most of the time -- they stem from a very early stage of Isar when structured proofs were not fully understood yet.

Is there any source I can access that describes this full understanding of structured proofs?

Let's say, the understanding has greatly improved since then, but is not really a "full" one.

An up-to-date exposition of general Isar concepts and machinery is now in section 2 of the isar-ref manual. This spot has been empty for ten years and has been filled only a few months ago.

Nonetheless, there are many things that are not written anywhere, notably about the deeper reasons for various design details. I am already glad enough to have occasional readers of the more basic stuff, and did not see a market yet for the really arcane lore.


Generally, I see the structured proof game as coaxing the proof engine into returning the particular proof state that I feel best explains the truth of my proposition to the human reader.

This basic principle has been there in Isar from the very beginning, but its focus has shifted more and more away from goals, towards more direct composition of facts (with nice derived concepts like 'also' and 'obtain', free-form blocks { ... } etc.).


To this end, I find intro and elim necessary quite often, when the default reasoning set returns a proof state that is incomprehensible to a human reader.

The "intro" and "elim" methods are probably best understood as logical counterparts to "unfold". This category of methods can be used at the start of an Isar proof, but the demand for this has greatly diminished over the years.

For example, in 1999 (when doing the HahnBanach case-study) we found ourselves using "elim" a lot to simulate what 'obtain' would become a bit later. Moreover, free-form blocks with moreover/ultimately + auto/blast are often more convenient for arbitrary composition of intermediate stepping stones than fiddling on goals with "intro" etc.

Nonetheless, intro/elim/unfold are in no way blacklisted as initial proof step (in contrast to bad things like "proof auto" which is really just a leftover from a very ancient attempt of mine at structure reasoning in
1997).


Obviously, it is suboptimal to have long convoluted chains of methods that result in the "obvious" goal state, since this will tend to make the reader uneasy about the "formal nonsense" that is meant to be reassuring them about the quality of the proof being offered.

Maybe this paper http://www4.in.tum.de/~wenzelm/papers/isar-reasoning.pdf helps to reduce formal nonsense a bit. (After the presentation at the conference some Coq expert told me that they have essentially always done the same, although with quite different means and ends.)


I still must say, that I can't follow the reasoning behind the way
default/rule is implemented. My confusion is well described by the
following examples, the first of which is a valid proof

lemma
  assumes
    a1: "A" and
    a2: "B"
  shows
    "A & B"
  using a1 a2 ..

lemma
  assumes
    a1: "A" and
    a2: "B"
  shows
    "A & B"
  using a2 a1 ..

and the second of which is not.

This can be seriously annoying when trying to chain facts

assume b1: "B"
have b2: "A"
  -- proof
with b1 show "A & B" ..

Here the "rule" method (of the '..' step) asks you to present facts in proper order, i.e. "from this and by".

In 1998, I did have a version of "rule" that was much more liberal, but never worked out so well. The critical question is how much variance (degrees of freedom) is acceptable in Isar proof checking, before either the system or the reader can no longer work things out with reasonable efforts.

If "rule" would admit arbitrary permutations of facts, for example, there would be a much larger search space for seamingly trivial steps. Even worse, it would stop working in most "open" situations via plain "proof ... qed', because the first choice needs to be the right one. It is better to leave free rearrangement of facts and goals to automated tools, and use something like "from a b c show D by blast" instead.

In contrast, there is no problem to allow the user write the required sub-proofs (fix/assume/show) in any order, because explicit text is given, and both the system and the user usually manage to fit things together quickly. (Actually, there used to be a performance bottle-neck here until recently; it has been sorted out for Isabelle2009.)


	Makarius





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