Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 30 Aug 1993 17:51:50 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA08366; Mon, 30 Aug 93 09:44:03 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA08362; Mon, 30 Aug 93 09:44:02 -0700 Received: from albatross.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 30 Aug 1993 17:43:59 +0100 To: info-hol@dworshak.cs.uidaho.edu Cc: jrh@cs.cornell.edu Subject: Re: HOL improvement: to better document your proof In-Reply-To: Your message of "Mon, 30 Aug 93 11:05:44 BST." <199308300905.AA20962@infix.cs.ruu.nl> Date: Mon, 30 Aug 93 17:43:54 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:158940:930830164401"@cl.cam.ac.uk> Konrad Slind writes: | I think an analysis of textbook-style proofs will show that the | weighting between forward and backward steps in a proof is different | than in a typical HOL proof. I think it's true that proofs in textbooks are generally forward at low levels of granularity, although sometimes backward at a higher level, e.g. "Clearly it is sufficient to prove ..." "This follows easily from the following lemma ..." The question is: why are proofs in mathematics books generally written forward -- is it just tradition or is there a good reason for it? If you look at some "epsilontics" proofs in analysis, lots of instantiations for lemmas are plucked from the air and then by some magic, the quantity we're interested in comes out less that epsilon. This sort of thing seems easier to understand backwards. Alternatively, you might say that the most comprehensible proof uses Isabelle-style "logic variables" which are instantiated retrospectively. John.