John, can you make SET_RULE part of the miz3 "by" justification? What I just
wrote about Collinear {A, B, C} doesn't yet make sense, because miz3 does not
know that
{A, B, C} = {A, C, B} = {B, A, C} = {B, C, A} = {C, A, B} = {C, B, A}.
At least, I had to work to prove a simpler result that's analogous to what
MESON does immediately for /\ and \/:
let DoubletonSymmetry_THM = thm `;
let x y be A;
thus {x, y} = {y, x}
proof
{x, y} = x INSERT {y} /\ {y, x} = y INSERT {x} [defDoubleton];
! P. P IN {x, y} <=> P = x \/ P = y [defxy] by defDoubleton, IN_INSERT,
IN_SING;
! P. P IN {y, x} <=> P = x \/ P = y by defDoubleton, IN_INSERT,
IN_SING;
qed by -, defxy, EXTENSION`;;
But SET_RULE can do this!!! And it can do what I wanted above:
SET_RULE `{A, B, C} = {C, A, B} /\ {A, B, C} = {B, A, C}`;;
val it : thm = |- {A, B, C} = {C, A, B} /\ {A, B, C} = {B, A, C}
So thanks for telling me about a cool prover SET_RULE of yours. If I could do
this in miz3, I think my code would be prettier. And maybe I don't need you to
do anything, as this already works in miz3:
let DoubletonSymmetry_THM = thm `;
let x y be A;
thus {x, y} = {y, x}
by SET_RULE`;;
let TripletonSymmetry_THM = thm `;
let x y z be A;
thus {x, y, z} = {y, x, z} /\ {x, y, z} = {y, z, x}
by SET_RULE`;;
I have problems with your actual SET_RULE suggestion, or maybe I don't
understand it:
If [the IN_ELIM_THM theorem seems complicated or unintuitive to
explain to readers not versed in HOL], one could argue that
provided you can prove semantic equivalence to something more
intuitive, there's no reason to use a separate definition. For
example, instead of your
let union = new_definition
`! s t:A->bool. s union t = \x. x IN s \/ x IN t`;;
how about re-using the existing notion but simply setting up a
different characterization
let union = SET_RULE `!s t:A->bool. s UNION t = \x. x IN s \/ x IN t`;;
Hmm... My long-range objective is to find work in the proof assistant world
with my math skills, as among mathematician, I think I'm exceptionally
interested in mathematical rigor. But of course that will require me to really
learn HOL Light (and maybe other proof assistants) very well, including
IN_ELIM_THM. But right now I'm trying to improve my position by getting a
Geometry/HOL paper published in a math journal, and that I think requires me to
explain HOL & miz3 is the simplest possible terms, kinda like Denzel Washington
in the movie Deja Vu telling the hotshot time-travel physicists, ``I know you
have PhDs, so I'm going to try to make this really simple...''
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:
let Ray_DEF = new_definition
`! A B. ray A B = {X | ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)}`;;
let IN_Ray = thm `;
! A B X. X IN ray A B <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)
by Ray_DEF, IN_ELIM_THM, REWRITE_TAC`;;
If we say my hotshots are supposed to learn HOL Light, then this code is
perfectly fine, and I'm proud of myself for figuring it out. This (which I'm
also proud of figuring out) however is I think a lot simpler:
let Rayz_DEF = new_definition
`! A B X. rayz A B X <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)`;;
let IN_Rayz = thm `;
! A B X. X IN rayz A B <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)
by Rayz_DEF, IN, BETA_THM`;;
--
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
