Thanks, Michael! I definitely did not know that, but I should have, as it
sounds like EXTENSION should prove it. Here's miz3 evidence for that, as this
proof works with MESON solved at number 69,282:
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
timeout := 30;;
let CurlyInterLambda_THM = thm `;
let P Q be A->bool;
thus P INTER Q = \x. x IN P /\ x IN Q
proof
! y. y IN P INTER Q <=> y IN P /\ y IN Q [interdef] by IN_INTER;
! y. y IN \x. x IN P /\ x IN Q <=> y IN P /\ y IN Q by IN, BETA_THM;
qed by -, interdef, IN, EXTENSION`;;
I don't think I should have needed IN in the qed line above, but it doesn't
work without it. For some reason, this didn't work, but I think it should have:
timeout := -1;;
let AbstractionInterLambda_THM = thm `;
let P Q be A->bool;
thus { x | x IN P /\ x IN Q} = \x. x IN P /\ x IN Q
proof
! y. y IN { x | x IN P /\ x IN Q} <=> y IN P /\ y IN Q [interdef] by
REWRITE_TAC, IN_ELIM_THM;
! y. y IN \x. x IN P /\ x IN Q <=> y IN P /\ y IN Q by IN, BETA_THM;
! y. y IN { x | x IN P /\ x IN Q} <=> y IN \x. x IN P /\ x IN Q by -,
interdef;
qed by -, IN, EXTENSION`;;
Everything worked until the qed line, where I got a #1 inference error after a
MESON number of 809,564, and 180,370 if I take out the IN which again seems
unnecessary. I was satisfied when miz3 bought my first line.
So I didn't solve your exercise, which maybe would have required me to
understand your GSPEC and SET_SPEC, but I see the result should be true.
Still, I don't admit I was wrong, as your phrase "fancy way of writing" isn't
precise. What I meant is that {x|..} is clearly not syntactic sugar for (λx.
..). I would be happy if it was, so that {x|..} = (λx. ..) would be true
without proof. It didn't occur to me that they were equal by a complicated
proof.
One exercise you might like to try is completely giving up on
set-notation. Write everything as predicates. If you need notions
like intersection, define predicate versions of these as well.
Don't use IN, just use application of a predicate to the argument.
I don't think I'll work your exercise, as I think it would be a huge amount of
work given my almost 4000 lines of code, and I don't see the point of it, as IN
has such a simple definition in sets.ml:
let IN = new_definition
`!P:A->bool. !x. x IN P <=> P x`;;
The exercise I'm considering is to continue using IN, but rewriting the parts
of sets.ml that I use to use (λx. ..) definitions instead of {x|..}, just as
you wrote:
inter P Q = λx. P x ∧ Q x
union P Q = λx. P x ∨ Q x
This would involve very little rewriting of my 4000 lines of miz3 code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
All it would cost me is my new {...} definitions e.g.
let Ray_DEF = new_definition
`∀ A B. ray A B = {X | ¬(A = B) ∧ Collinear A B X ∧ A ∉ open (X,B)}`;;
I'd just have to go back to my old definition
let Ray_DEF = new_definition
`∀ A B. ray A B X ⇔ ¬(A = B) ∧ Collinear A B X ∧ A ∉ open (X,B)`;;
The advantage of my exercise would be that I'd understand my code a little
better, as BETA_THM makes a lot more sense to me than IN_ELIM_THM! My HOL
ignorance is so vast that I don't even understand REWRITE_TAC yet :)
BTW, here's an example of what Freek wrote, how it's mystifying to need the
tactic REWRITE_TAC in miz3:
let IN_Ray = thm `;
∀ A B X. X ∈ ray A B ⇔ ¬(A = B) ∧ Collinear A B X ∧ A ∉ open (X,B)
by Ray_DEF, IN_ELIM_THM, REWRITE_TAC`;;
I get a #1 inference error if I take REWRITE_TAC out.
As you see, I actually write with your symbols ∪, ∈, ∩, ∀, ∃, and use an Emacs
preprocessor to turn these into the ordinary characters HOL Light uses. I'm
glad to hear that HOL4, as well as Isabelle, uses these math symbols. Which
one of you did it first, I wonder? It just hadn't occured to me to use your λ,
but I will starting now! How hard would it be for HOL Light to be able to do
this? Is that called supporting Unicode such tokens?
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
