Re: [isabelle] Length of Proofs

Almost always, it is possible to considerably shorten proofs by use (and proper setup) of automated techniques (maybe even more so when using Isabelle/ML). The other extreme is to explicitly write every single step in Isar (as I know from myself and many students I taught, mostly beginners use this kind of proofs... of course it also depends on your intended audience).

In my opinion both extremes are bad. It is an art (as is often pointed out in Isar related manuals) to write Isar proofs that are readable yet not too verbose. But if you master this art, the gain is that others can actually read your proofs and follow the steps without even starting Isabelle (which is definitely not the case with the technique shown by Jeremy; so I would rather use that technique that are considered "trivial" by humans... but then again humans are often wrong in their initial judgment of what is trivial ;)).

I guess what I want to say is that no, proofs do not have to be exceedingly long in many cases, but sometimes long versions (or rather versions of appropriate length) are much better to read and maintain.



On 11/01/2012 03:59 PM, Jeremy Dawson wrote:

I don't know if this is a factor in this particular set of proofs, but
often a particular sequence of proof steps is reused repeatedly.
In such a case it is advantageous not to have to write them all down
repeatedly, but to reuse them.
The Standard ML interface to Isabelle is ideally suited to this
purpose.  Unfortunately its use has become actively discouraged in
recent years.

To illustrate, here are some bits of a proof script of mine which makes
good use of the Standard ML interface.

fun mctrtac sg st = FIRST [ atac sg, (match_tac [mstrctr.ctr] sg),
  ((resolve_tac [mstrctr.Comma, mstrctr.Star] THEN_ALL_NEW mctrtac) sg),
  (rtac mstrctr.same sg) ] st ;

fun dvi_ctr_tacs dths = [
  (rtac ex_conjI), (rtac mseqctr.I), mctrtac, mctrtac,
  (eresolve_tac [der_asm, dd1th] THEN_ALL_NEW
    resolve_tac dths THEN_ALL_NEW ssai_tac) ] ;

fun init_dvi_ctr_tacs dths = [
  (* ensure only desired occurrence of rule is expanded *)
  Clarsimp_tac, dtac trans, (clarsimp_tac (cesimps rule_defs)),
  rtac refl, Clarsimp_tac,
    (* split up say F delible from (X,Y),Z |- W into cases:
      F (with stars) is X,Y or Z, or F is delible from X,Y,Z or W *)
    (REPEAT_SOME (eresolve_tac [mseqctr.elim,
        mstrctr_CommaR, mstrctr_StarR, mstrctr_IR]
      THEN_ALL_NEW Clarsimp_tac)),
    (* when deletion to substituted variable in rule *)
    TRYALL (EVERY' (dvi_ctr_tacs dths)) ])) ] ;

fun xstacs th = [
  (rtac ex_conjI 1), (etac dd1th 2),
  ((rtac th THEN_ALL_NEW ssai_tac) 2),
  (rtac mseqctr.I 1), mctrtac 1, mctrtac 1 ] ;

val th = rdp (tn [dca1, dppsA, dica1, dassoc]) ;

in the above, each additional theorem in the list of arguments to tn
involves several proof steps

val ctr_assoc_tacs = [
  (EVERY' (init_dvi_ctr_tacs [dassoc]) 1),
  (EVERY (xstacs ([dassoc, dassoc] MRS duA2))),
  (EVERY (xstacs th)) ] ;

(and twelve more rather like ctr_assoc_tacs, just a bit different)

val ctr_tacs = [ EVERY init_ctr_tacs,
  EVERY ctr_assoc_tacs,
  EVERY ctr_ica1_tacs, EVERY ctr_ica2_tacs,
  EVERY ctr_ics1_tacs, EVERY ctr_ics2_tacs,
  (EVERY' (init_dvi_ctr_tacs [dastars]) 1),
  (EVERY' (init_dvi_ctr_tacs [dassA]) 1),
  EVERY ctr_ca1_tacs, EVERY ctr_ca2_tacs,
  EVERY ctr_cs1_tacs, EVERY ctr_cs2_tacs,
  EVERY ctr_rstars_tacs, EVERY ctr_rssA_tacs ] ;

If I had written this out in the modern style (using Isar) the above
would expand to thousands, probably tens of thousands, of lines of code.


Jeremy Dawson

Jens Doll wrote:
Hello all,

when viewing the file Vickrey.thy from Tim I almost fell from my
chair. It has 22 pages of code and that seems to be a normal length
for Isabelle.

Does anyone know how to shorten these artefacts or could someone
explain to me why proofs have to be that long?


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