Here's a question about free variables and REWRITE_TAC (and other
thmlist->tactics). Almost every usage of USE_THEN in the HOL Light sources is
of the form
USE_THEN label MATCH_MP_TAC
Here's an example of a labeled assumption used in thmlist of MESON_TAC:
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
INTRO_TAC "!p q; lose; need" THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
ASM_REWRITE_TAC [ARITH_RULE
`q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
(2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
USE_THEN "need" (fun thm ->
MESON_TAC[LE_MULT2; MULT_EQ_0; ARITH_RULE `2 * x <= x <=> x = 0`; thm]));;
0..0..1..3..9..22..48..204..698..2758..solved at 8153
val NSQRT_2 : thm = |- !p q. p * p = 2 * q * q ==> q = 0
The code is slightly modified from page 75 of the HOL Light tutorial, with
REPEAT STRIP_TAC replaced by an INTRO_TAC and ASM_MESON_TAC replaced by a
USE_THEN-powered MESON_TAC. But this blows up if I give a label for the
ARITH_RULE result and then USE that as well:
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
INTRO_TAC "!p q; lose; need" THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
ASM_REWRITE_TAC[ARITH_RULE
`q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
(2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
SUBGOAL_TAC "EZarith" `2 * x <= x <=> x = 0` [ARITH_TAC] THEN
USE_THEN "need" (fun thm1 ->
USE_THEN "EZarith" (fun thm2 ->
MESON_TAC [LE_MULT2; MULT_EQ_0; thm1; thm2])));;
MESON_TAC hangs, and I let it go up to 9,277,022. There's an easy fix, though:
quantify the free variable x in "EZarith". Now it works:
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
INTRO_TAC "!p q; lose; need" THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
ASM_REWRITE_TAC[ARITH_RULE
`q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
(2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
SUBGOAL_TAC "EZarith" `!x. 2 * x <= x <=> x = 0` [ARITH_TAC] THEN
USE_THEN "need" (fun thm1 ->
USE_THEN "EZarith" (fun thm2 ->
MESON_TAC [LE_MULT2; MULT_EQ_0; thm1; thm2])));;
That works fine, and it was worth doing, to show that two different labeled
assumptions can both be USE-ed in the same thmlist->tactic.
Why was the free variable x OK when the result was proved by ARITH_RULE in the
MESON_TAC thm list, but not OK when the result was proved externally and then
referred to by label?
I claim this problem is not caused by USE_THEN, as it comes up in the original
version of NSQRT_2:
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
ASM_REWRITE_TAC[ARITH_RULE
`q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
(2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
SUBGOAL_TAC "EZarith" `!x. 2 * x <= x <=> x = 0` [ARITH_TAC] THEN
ASM_MESON_TAC[LE_MULT2; MULT_EQ_0]);;
That works fine, but it hangs if take out the universal quantifier in "EZarith":
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
ASM_REWRITE_TAC[ARITH_RULE
`q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
(2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
SUBGOAL_TAC "EZarith" `2 * x <= x <=> x = 0` [ARITH_TAC] THEN
ASM_MESON_TAC[LE_MULT2; MULT_EQ_0]);;
The reason I brought up USE_THEN is that what I really is labeled assumptions
used as arguments of MESON to create an argument of REWRITE_TAC (or some other
thm_list->tactic). So let's define
let USE_TltacThmlistThmTerm tltac thmlist label term = USE_THEN label
(fun thm -> tltac (thmlist @ [MESON [thm] term]));;
I know this code works in contrived examples like this, where I use MESON in
the thm list to prove the result using itself:
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
INTRO_TAC "!p q; lose; need" THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
ASM_REWRITE_TAC[ARITH_RULE
`q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
(2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
SUBGOAL_TAC "EZarith" `!x. 2 * x <= x <=> x = 0` [ARITH_TAC] THEN
USE_THEN "need" (fun thm1 ->
USE_THEN "EZarith" (fun thm2 ->
USE_TltacThmlistThmTerm MESON_TAC [LE_MULT2; MULT_EQ_0; thm1]
"EZarith" `2 * x <= x <=> x = 0`)));;
And notice that I was able to take off the universal quantifier at the bottom,
but not in the subgoal "EZarith". To compound the mystery, let's run this
interactively:
g `!p q. p * p = 2 * q * q ==> q = 0`;;
e(MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
INTRO_TAC "!p q; lose; need" THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
ASM_REWRITE_TAC[ARITH_RULE
`q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
(2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
SUBGOAL_TAC "EZarith" `!x. 2 * x <= x <=> x = 0` [ARITH_TAC]);;
e(USE_THEN "need" (fun thm1 ->
USE_THEN "EZarith" (fun thm2 ->
USE_TltacThmlistThmTerm MESON_TAC [LE_MULT2; MULT_EQ_0; thm1]
"EZarith" `2 * x <= x <=> x = 0`)));;
0 [`(2 * m) * 2 * m = 2 * q * q`] (need)
1 [`!x. 2 * x <= x <=> x = 0`] (EZarith)
`2 * m <= q ==> q = 0`
0..0..1..solved at 4
0..0..1..solved at 4
0..0..1..3..9..22..48..204..698..2758..solved at 8153
val it : goalstack = No subgoals
Notice that the theorem labeled "need" has two free variables. Why is a free
variable with EZarith a problem?
--
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
