*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 28 Apr 2010 19:28:30 +0100*Cc*: isabelle-users at cl.cam.ac.uk, grechukbogdan <grechukbogdan at yandex.ru>*In-reply-to*: <k2mcc2478ab1004280945gb510d767maf21c86aad9e0ab5@mail.gmail.com>*References*: <6031272389962@web71.yandex.ru> <k2mcc2478ab1004280945gb510d767maf21c86aad9e0ab5@mail.gmail.com>

Thanks for tackling those questions. You make some good points about stability of proofs, but somehow you've omitted the most important one: structured proofs are inherently much more robust, because if something does fail then you know exactly which part of the proof is affected; you never get leftover subgoals being given to tactics that were intended to perform a separate part of the proof. Another small point: if you use sledgehammer to generate metis calls, these will be stable, because they explicitly list all the theorems involved. The only modification to Isabelle that could affect a metis call would be a change to metis itself. Larry Paulson On 28 Apr 2010, at 17:45, Brian Huffman wrote: > Yes, it is troubling that Isabelle does not really provide any kind of > backward compatibility for proof scripts. As someone who has spent a > lot of time fixing broken proof scripts, this is an important concern > for me. > > At the very least, it should be safe for you to assume that tactics > like auto are "monotonic" with respect to versions, i.e. any subgoal > that can be solved in one step by "auto" in Isabelle2008 should also > be solved in one step by "auto" in Isabelle2009. Of course, it is also > likely (and generally desirable!) that 2009's "auto" will solve some > subgoals that 2008's "auto" could not. > > Robust proof scripts need to keep this "monotonicity" property in > mind. Here's an example of a proof script that is NOT robust: > > apply (rule foo) > apply auto > apply (rule bar) > apply auto > apply (rule ...) > apply auto > ... > > Proof scripts like this are a nightmare to fix when they go wrong. The > problem is that there are applications of "auto" that don't solve > subgoals completely, but leave a bunch of leftover subgoals behind. > The rest of the proof script relies on the leftover junk being in a > very particular shape. If in a later version of Isabelle, auto leaves > a slightly smaller pile of leftovers, then the proof will break. > > So here is my advice for writing robust proof scripts: > > * One-step proofs like "by auto" should always be OK (You should be > able to rely on the developers to ensure "monotonicity" of future > versions.) > > * Tactics that leave other subgoals behind are OK if and only if they > have predictable behavior (this includes tactics like "rule", > "clarify", "intro", and "safe"; but NOT "auto".)

**Follow-Ups**:**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Alexander Krauss

**References**:**[isabelle] Proof by analogy and proof stability in Isabelle***From:*grechukbogdan

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Previous by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Cl-isabelle-users April 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list