Thanks for responding, Ramana! I see only one advantage to redefining set
operations (e.g. INTER) as abstractions: it makes my code easier to read for me
and my target audience of mathematicians, as I can substitute the very easy
BETA_THM for the subtle and complicated IN_ELIM_THM that Michael and John just
explained. You gave me some arguments against switching from set abstractions
to sets, and that's good. However,
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. I think you're saying the set-abstraction/enumeration
notation creates some sort of difference between subsets and boolean
functions, and I'm happy to hear that. There's certainly something to be said
for abstraction barrier so we can change low-level representations, but I
don't see the relevance of that here. So that's great, and thanks for
explaining. But I'm confused about the difference between set-abstractions and
set-enumeration, both of which get printed as {...}. Both INSERT and {} are
defined as abstractions in HOL Light, and I assume the same is true for HOL4,
and yet they they get printed with {...}:
# `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)`
This is the same reason to use the constant IN in your definitions
and statements, even though many proofs go through easiest by
rewriting it away first.
I think my motivation is different. I have 1167 occurrences of the predicate
IN in my miz3 Hilbert axiomatic geometry code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
(now at 4180 lines, Euclid's book I formalized up to Proposition 26 (AAS)),
and 369 occurrences of NOTIN. I use IN and NOTIN to make it clear that I'm
talking about sets, as in e.g.
DropPerpendicularToLine_THM
|- ∀ P l. Line l ∧ P ∉ l
⇒ ∃ A D. A ∈ l ∧ D ∈ l ∧ Right (∡ P D A)
There's no way I'd be happy writing instead the equivalent
Line l ∧ ¬(l P)
⇒ ∃ A D. l A ∧ l D ∧ Right (∡ P D A)
My mathematical audience wouldn't understand me, and I wouldn't understand my
own code well enough to write it. But I only have 3 occurrences of set
abstractions {...} in my code, although I ought to add to that the set
abstractions {...} I use for INTER etc in sets.ml (5 by my count). Now I'm
certainly not willing to give up my set-enumerations, e.g.
Segment_DEF |- ∀ A B. seg A B = {A, B} ∪ open (A,B)
or the operation INTER (which Emacs pre-processor turns ∪ into. I was very
happy, a few months ago, when I realized that HOL had this set theory capacity!
But my readers won't spend much time, if any, looking at the set abstraction
definition
let UNION = new_definition
`s UNION t = {x:A | x IN s \/ x IN t}`;;
in sets.ml, and my definition (which works just as well)
let union = new_definition
`! s t:A->bool. s union t = \ x. x IN s \/ x IN t`;;
isn't that much less readable, I'm thinking, if you only look at it once.
--
Best,
Bill
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
