I have a question about REWRITE_TAC. I was invited to speak at the conference
https://ihp2014.pps.univ-paris-diderot.fr/doku.php?id=workshop_1
where John, Freek, Tobias Nipkow and Tom Hales are 4 of the 14 plenary
speakers, and I hope folks here will help answer various HOL Light questions I
still have. It would also be nice if folks could tell me how other HOLs differ
on my questions, such as this one. Here's a fine proof OPEN_BALL from
Multivariate/topology.ml:
needs "Multivariate/topology.ml";;
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]);;
Here's a somewhat shorter proof I'll write interactively:
g `!x e. open (ball (x,e))`;;
e(REWRITE_TAC [open_def; ball; IN_ELIM_THM]);;
e(REWRITE_TAC [DIST_SYM]);;
e(MESON_TAC [REAL_SUB_LT; REAL_LT_SUB_LADD; REAL_ADD_SYM;
REAL_LET_TRANS; DIST_TRIANGLE]);;
I'm quite mystified that the REWRITE_TAC[DIST_SYM] only rewrote the middle dist
term (I substituted math characters for readability), changing
`∀x e x'.
dist (x,x') < e
⇒ (∃e'. &0 < e' ∧ (∀x''. dist (x'',x') < e' ⇒ dist (x,x'') < e))`
to
`∀x e x'.
dist (x,x') < e
⇒ (∃e'. &0 < e' ∧ (∀x''. dist (x',x'') < e' ⇒ dist (x,x'') < e))`
Why did REWRITE_TAC only symmetrize the middle dist term? Here's a version I
understand, where I targeted exactly which dist I wanted to symmetrize:
let rewriteRARARARRARRALL = GEN_REWRITE_TAC (RAND_CONV o ABS_CONV o
RAND_CONV o ABS_CONV o RAND_CONV o ABS_CONV o RAND_CONV o
RAND_CONV o ABS_CONV o RAND_CONV o RAND_CONV o ABS_CONV o
LAND_CONV o LAND_CONV);;
g `!x e. open(ball(x,e))`;;
e(REWRITE_TAC[open_def; ball; IN_ELIM_THM]);;
e(rewriteRARARARRARRALL [DIST_SYM]);;
e(MESON_TAC [REAL_SUB_LT; REAL_LT_SUB_LADD; REAL_ADD_SYM;
REAL_LET_TRANS; DIST_TRIANGLE]);;
The output is the same, and I suppose this shows the merit of the original
proof of OPEN_BALL, where all three dist terms get symmetrized by
ONCE_REWRITE_TAC[DIST_SYM]. Let me include that output for completeness:
g `!x e. open (ball (x,e))`;;
e(REWRITE_TAC [open_def; ball; IN_ELIM_THM]);;
e(ONCE_REWRITE_TAC [DIST_SYM]);;
e(MESON_TAC [REAL_SUB_LT; REAL_LT_SUB_LADD; REAL_ADD_SYM;
REAL_LET_TRANS; DIST_TRIANGLE_ALT]);;
`∀x e x'.
dist (x,x') < e
⇒ (∃e'. &0 < e' ∧ (∀x''. dist (x'',x') < e' ⇒ dist (x,x'') < e))`
# val it : goalstack = 1 subgoal (1 total)
`∀x e x'.
dist (x',x) < e
⇒ (∃e'. &0 < e' ∧ (∀x''. dist (x',x'') < e' ⇒ dist (x'',x) < e))`
--
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
