Re: [isabelle] Proof by analogy and proof stability in Isabelle



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".)






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