Hi Bill,
| let DoubletonPlusSymmetry_THM = thm `;
| let a b be A;
| let X Y be A->bool;
| assume X = Y;
| thus {a, b} UNION X = {b, a} UNION Y
| by SET_RULE`;;
I think Ramana correctly diagnosed the problem, namely that the X = Y
assumption is not being implicitly used. If you change "horizon := 0"
to "horizon := 1" then it works. Though you probably wouldn't want to
do this globally, since you want to keep your proofs explicit and not
allow implicit assumptions.
One useful way of debugging such things is to turn on OCaml's tracing
to see exactly what is getting passed to the inference rule. So for
example, if you do the following before the above script you can see
what SET_RULE is trying to prove in each case
#trace SET_RULE;;
| I know you're real busy right now, and I can't argue this is high
| priority, but I think it would be nice for miz3 to have a good
| set-theory prover to go along with its good FOL prover MESON. I
| don't know exactly what this set-theory prover ought to prove, but
| I figure it should prove result analogous to what MESON already
| proves.
Yes, this would clearly be a useful thing to do. A crude approach
would be simply to use SET_TAC in place of MESON_TAC in the
justification code. All that SET_TAC really does is expand some
set-theoretic definitions systematically and then call MESON, as you
can see from the code:
let SET_TAC =
let PRESET_TAC =
POP_ASSUM_LIST(K ALL_TAC) THEN REPEAT COND_CASES_TAC THEN
REWRITE_TAC[EXTENSION; SUBSET; PSUBSET; DISJOINT; SING] THEN
REWRITE_TAC[NOT_IN_EMPTY; IN_UNIV; IN_UNION; IN_INTER; IN_DIFF; IN_INSERT;
IN_DELETE; IN_REST; IN_INTERS; IN_UNIONS; IN_IMAGE;
IN_ELIM_THM; IN] in
fun ths ->
(if ths = [] then ALL_TAC else MP_TAC(end_itlist CONJ ths)) THEN
PRESET_TAC THEN
MESON_TAC[];;
let SET_RULE tm = prove(tm,SET_TAC[]);;
However, I would like to do things a bit more carefully since this
preprocessing can occasionally hinder MESON as well as helping it.
Indeed, I have a few problems with SET_TAC that I would like to fix
(e.g. the first rewrite sometimes expands things too eagerly in the
case of sets of sets), and this would make a good excuse. I will think
about it a bit more.
I should also say that SET_RULE/SET_TAC, while tremendously useful for
generating trivial but tedious-to-prove little facts of set theory, may
not quite do all you wanted originally, making the built-in
justification insensitive to ordering in terms like `Collinear {A,B,C}`.
Although it can certainly prove `{A,B,C} = {B,A,C}` etc. as a
standalone goal, SET_RULE would not, for example, give you even such
simple generalizations as `P {A,B,C} ==> P {B,A,C}`. It would be an
interesting (and not necessarily easy) project to extend its abilities
like this. But it might be much easier to take a more focused approach
to dealing with this kind of permutation (e.g. something akin to
Brand's transformation, which is explained a bit in my book).
I'm a bit late to the party with recent discussions, but here are
a few other comments:
| The only reason I'm using union is to spare my readers the complicated
| and wonderful things that HOL folks have figured out, such as
| IN_ELIM_THM. But SET_RULE (from sets.ml) uses IN_ELIM_THM! The only
| problem I'm worrying about here is whether this short simple
| beautiful HOL Light isn't simple enough for my hotshot Math PhDs:
That is of course quite possible: those like myself have been using
HOL for so long that we've lost track of how baffling some of it is
to the uninitiated. Though you might still be able to make the case
that it would suffice to prove equivalence of the definition to a
more transparent one, rather than actually change the definition.
By analogy, whether you define "polytope" as "bounded polyhedron"
or "convex hull of a finite set" isn't that important provided you
can derive the other possible definition as a theorem.
| Anyway, it was clear to me that Hartshorne skipped a lot of steps in
| his proofs that folks can't fill in if they're not really serious
| about math, and I filled in many of these steps in my paper
| http://www.math.northwestern.edu/~richter/hilbert.pdf, which is now
| badly in need of revision because of all the steps HOL Light pointed
| out that I skipped and bungled!
It's very encouraging to hear that HOL Light helped you to debug your
own explicit proofs. In my experience, proofs at that level are very
hard to get right by hand, which may be why few others have tried to
make the proofs as explicit as you did. After all, you might expect
this to be well-trodden ground given the long history of axiomatic
geometry, yet it seems that pretty much everyone including Hartshorne
has been content with vaguer sketches, accurate or not, of what could
be done in principle.
| I can think of other miz3 problems that seem a lot more pressing that
| set notations, like being able to use #use "<miz3-file>.ml";; I'm
| guessing I'll have 5000 lines of code by the time I'm done, and what
| if some body's machine can't store that much in the X-selection or
| whatever to paste it from one window to another? And if we could #use
| miz3 code, couldn't it be included in distributions with straight HOL
| Light code?
Yes, that would obviously be a very useful thing. It should be easy
enough to code up. I am tempted to call it "mizuse" but that might be
misunderstood.
| Mathematicians distinguish between a subset of X and a boolean
| function on X, even though they're "the same thing", and I was worried
| that HOL wasn't making this distinction.
The systematic development of this basic set-theoretic machinery in
HOL was largely done by Tom Melham (using some older material by Ton
Kalker, Philip Leveilley and perhaps others). Tom wrote two closely
analogous libraries, one of which ("sets") defined a distinct type of
sets, and one of which ("pred_sets") just defined set operations on
predicates. When I developed HOL Light I decided just to adopt sets as
predicates, since it seemed that the convenience of being able to
switch between "set" and "predicate" point of view was worth the loss
of an abstraction barrier, and I didn't want to present the user with
a difficult choice or make HOL Light less "light".
I think HOL4 might have gone the same way, since I see "src/pred_set"
in its source base but not "src/set". Isabelle/HOL used to have a
similar separation between sets and predicates-as-sets, but it was
removed in 2008. There was a bit of discussion of the advantages and
disadvantages starting here:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-December/msg00039.html
The "sets.ml" file in HOL Light is clearly a derivative of Tom's
original pred_sets work, though better use is made of proof automation
like MESON (which wasn't present in HOL88), and the definitions of
recursion and cardinality use later work by Ching-Tsun Chou. Many of
the names of theorems are just copied from Tom's library, as you can
see from some of the names. Tom always wanted to maintain the
terminology that functions are commutative while relations are
symmetric, hence the use of INTER_COMM and not INTER_SYM, while I
tend to use _SYM everywhere else without distinction.
Moreoever, those working in program verification often chose to define
"lifted" versions of logical connectives, which in many cases are
coextensive with set operations on predicates, but use names
suggestive of the logical connectives to reflect the intended use. The
motivation is that annotations like preconditions and postconditions
are analyzed into predicates on some "state" type, and you don't want
to pass this around in an unreadable fashion. See for example HOL
Light's "Examples/prog.ml" file:
let OR = new_definition
`p OR q = \x:S. p x \/ q x`;;
| But I'm confused about the difference between set-abstractions and
| set-enumeration, both of which get printed as {...}.
You can always tell the abstractions apart because they have at least
one vertical bar as in {f x | P x} (sometimes two bars if you need to
disambiguate the intended bound variables).
| # `x INSERT {y}`;;
| val it : term = `{x, y}`
| # `x INSERT y INSERT {}`;;
| val it : term = `{x, y}`
| That surprises me. I don't see why abstractions should get printed as
| {...}, and I don't see how INSERT and {} respect your barrier between
| abstractions and sets. But {} is defined as (\ x:A. F), and this does
| not get printed as {...}:
| # `x INSERT y INSERT (\ x. F)`;;
| val it : term = `x INSERT y INSERT (\x. F)`
Generally the approach is to prettyprint certain "standard" forms in
a special way, where it seems likely to be intuitive to the user. In
your last example it doesn't fit the standard form `{a,b,c,...,x}` and
so it is just printed in a "raw" style. The same is true, for example,
of numerals, which have a composite representation internally:
# `NUMERAL (BIT1 _0)`;;
val it : term = `1`
# `NUMERAL (BIT1 x)`;;
val it : term = `NUMERAL (BIT1 x)`
John.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
