Vince, this is very interesting:
I would say what is bad coding is not to rely on features you don't
understand but on features that are actually
undocumented/unintended. Here, the ordering chosen is indeed
ingenious to prevent some often-met looping situations. However,
as John pointed out it is also completely arbitrary (in your case
it just applies the rewrite you wanted because Ocaml orders symbols
as follows: x < x' < x'').
Ah, that's why it worked! I was really puzzled. But doesn't that mean you
won't ever use REWRITE_TAC or SIMP_TAC, as John's actual algorithm (or
Tobias's) might be published but isn't explained in the documentation? I mean,
I use REWRITE_TAC, MESON_TAC and SIMP_TAC all the time, rarely knowing in
advance which one will work. Two quick notes:
The ONCE_REWRITE_TAC approach was John's original code, and it did what John
intended. That's really cool, that you discovered that DIST_SYM can be moved
to the MESON_TAC theorem list (how did I miss that???), and that works for my
readable.ml code (and thanks again for helping me write it)
let OPEN_BALL = theorem `;
∀x e. open (ball (x,e))
proof
rewrite open_def ball IN_ELIM_THM;
fol DIST_SYM REAL_SUB_LT REAL_LT_SUB_LADD REAL_ADD_SYM REAL_LET_TRANS
DIST_TRIANGLE;
qed;
`;;
Note that my version runs about as long as yours
let OPEN_BALL = prove
(`!x e. open(ball(x,e))`,
REWRITE_TAC[open_def; ball; IN_ELIM_THM] THEN
MESON_TAC[DIST_SYM; REAL_SUB_LT; REAL_LT_SUB_LADD; REAL_ADD_SYM;
REAL_LET_TRANS; DIST_TRIANGLE_ALT]);;
and that John's original version is about 160 times faster :)
let OPEN_BALL = prove
(`!x e. open(ball(x,e))`,
REWRITE_TAC[open_def; ball; IN_ELIM_THM] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
MESON_TAC[REAL_SUB_LT; REAL_LT_SUB_LADD; REAL_ADD_SYM; REAL_LET_TRANS;
DIST_TRIANGLE_ALT]);;
--
Best,
Bill
------------------------------------------------------------------------------
Android apps run on BlackBerry 10
Introducing the new BlackBerry 10.2.1 Runtime for Android apps.
Now with support for Jelly Bean, Bluetooth, Mapview and more.
Get your Android app in front of a whole new audience. Start now.
http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
