On Fri, 23 Nov 2012, Alexey Solovyev wrote:
>> * 'have' as subgoal: I reckon it is simular to subgoal_tac in Isabelle
>> or its counterpart in HOL. In Isar, I made this quite different:
>> having a first-class notion of proof context, 'have' is just a fresh
>> local goal within it, and its result a theorem with certain
>> assumptions, which is then re-used in the enclosing proof. This gives
>> you more structure and scalability than just goal-modifications in the
>> old style.
>>
> 'have' is implemented via SUBGOAL_THEN in HOL Light. Your implementation of
> 'have' in Isar sounds interesting, but could you give examples when "local
> theorems" are better than just subgoals?
After so many years of first-class notion of proof context and local facts
within it, I find it hard to explain its many benefits. So here are just
some aspects to get an idea.
(1) Occam's razor. Traditional tactical provers encode local results by
pushing more and more premises into subgoals. This is somehow
indirect: SUBGOAL_TAC and relatives do some logical bookeeping to do
nothing more than saying you want to use later again what you had
before already. To carry around local facts, I don't need logic. I
just carry them around (in ML).
A more basic instance of this principle are multiple facts, e.g.
groups of related things like LE_1 in arith.ml of HOL-Light from
today (rev 152).
let LE_1 = prove
(`(!n. ~(n = 0) ==> 0 < n) /\
(!n. ~(n = 0) ==> 1 <= n) /\
(!n. 0 < n ==> ~(n = 0)) /\
(!n. 0 < n ==> 1 <= n) /\
(!n. 1 <= n ==> 0 < n) /\
(!n. 1 <= n ==> ~(n = 0))`,
Here Isar makes an ML list of several thm values, not a thm with
several propisitions encoded via auxiliary connectives. Getting rid
of redundant conjunctions (and auxilary quantifiers) should be
rather obvious. If you add management of implicit hyphotheses from
the context (like Coq sections, Isabelle locales, or rather Isar
proof contexts) you are coming towards genuine local facts. Just
facts within a context, without funny logical decorations.
In your SSReflect/HOL Light manual you were speaking about the proof
context in a way that might get close to that already.
An important aspect of the "small-scale reflection" of Gonthier's
original version seems to be similar avoidance of logical
inconveniences. Although he is still somehow tied to his type
theory.
(2) Structure. The most basic indication of a structured proof step is
an indication of its relevant facts: the collection of facts that
might contribute to it at most. It is given explicitly. (Tools
may also have a secondary context of implicit facts declared as
hints in the library).
If you add more and more results from SUBGOAL_TAC to you goal state,
you get more and more potentially used premises. This looses
information to the user. Which 1 or 2 or 3 of 20 of them contribute
to the proof?
(3) Scalability. Like (2) but affecting automated proof tools.
Overcrowded goal states slow down proof search, or make it loop.
Isar has greatly benefitted from explicit fact indication before
entering the next goal statement. So relatively heavy automated
tools have become more useful after the main reform in 1999.
For example, you write:
from fact1 fact42 fact99 have XXX by auto
instead of implicit use from the old times:
from prems -- "99 things produced before" have XXX by auto
Another aspect of scalability: having many independent 'have' goal
states in your proof allows the prover to schedule things fexibly
and in parallel. It is good to be relived from the one
central goal state where everything had to be fiddled through
sequentially.
Makarius
------------------------------------------------------------------------------
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
