On Sat, Aug 18, 2012 at 5:55 AM, Bill Richter <rich...@math.northwestern.edu>
wrote:
> Right now I'm worrying about a different problem, that I've never
> understood sets.ml, especially its use of IN_ELIM_THM to prove the
> IN_<operation> theorems. After Michael taught me that a {...} is equal, in
> a complicated way, to a lambda, I thought, why not just define INTER,
> DELETE, UNION etc as lambdas? Then the IN_<operation> theorems are easy
> to prove, and I wrote up miz3 proofs myself that I could easily understand.
>
As I think was mentioned before, you don't have to (re)define the set
operations as abstractions (or "lambdas" as you call them), you can simply
prove that the existing definitions are equal to the desired abstractions
and then pretend those theorems are the definitions thereafter. (This has
the advantage of not introducing new constants, so you can use all the
existing theorems about the existing set operations without reproving them.)
> It would be easy to rewrite my 4000 lines of miz3 Hilbert code using
> lambda defs of INTER etc, and maybe that makes my code look simpler or more
> self-contained. I'm still not convinced it's a good idea. I think I'm
> missing a lot. What is the point of the {...} definition of INTER, other
> than to see the nice {...} notation? I love the {...} notation myself, but
> it's really equal to a lambda. So I wonder if the visual plus of some
> {...} in my code and in sets.ml offsets the fact that BETA_THM is so much
> simpler than IN_ELIM_THM. I can't judge. It was definitely a thrill for
> me to write readable understandable miz3 proofs of all the sets.mlresults
> that I use.
>
Here's my attempt at rationalising this:
- The point of using the set-abstraction/enumeration notation is that it
makes it convenient to write set comprehensions (aka "set builder"
notation) like { x + 6 | x < n }, which combine a filtering predicate with
an element-building expression.
- Using the same notation (and hence the same GSPEC constant or whatever
it parses down to) for all set operations, including simple ones like { x |
x IN s1 /\ x IN s2 }, gives a uniformity to the treatment of sets.
- A uniform treatment of sets makes it easier (for you and for tactics)
to see where the sets are (as opposed to other terms), and creates a
(semi-transparent) abstraction barrier between sets and ordinary
function-representing lambda abstractions (which is useful, for example, if
one day you want to change the representation of sets). 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. It's like
giving variables meaningful names when the compiler doesn't care:
distinguish the terms you want to treat as sets even though the logic
doesn't care.
------------------------------------------------------------------------------
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
