I have a dumb question about interactive HOL Light proofs vs tactics scripts.
I got the impression from p 48 of the tutorial that you can package an
interactive (g & e) proof as a tactic script with THEN. But that didn't work
for me. Part of my question is how to debug a tactics script. Also, I don't
understand the goalstack and how to read it. After my first interactive
e(COND_CASES_TAC);;
HOL Light reports
# val it : goalstack = 2 subgoals (3 total)
I think that means there's a third goal that HOL Light didn't report, and I
think I know what that 3rd goal is, but I'd like to get HOL Light to print it,
i.e. print the entire goalstack (doesn't that mean the stack of goals?).
I got my version of NSUM_CLAUSES_NUMSEG to look better, i.e. not just a miz3
proof shoe-horned into tactics form, again using my version of NUMSEG_CLAUSES:
let NUMSEG_CLAUS = prove
(`(!m. m..0 = if m = 0 then {0} else {}) /\
(!m n. m..SUC n = if m <= SUC n then (SUC n) INSERT (m..n) else {})`,
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
GEN_REWRITE_TAC I [EXTENSION] THEN
REWRITE_TAC[IN_NUMSEG; NOT_IN_EMPTY; IN_INSERT] THEN
POP_ASSUM MP_TAC THEN ARITH_TAC);;
g `(!m. nsum (m..0) f = if m = 0 then f 0 else 0) /\
!m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n) else
0`;;
e(REWRITE_TAC[NUMSEG_CLAUS]);;
e(REPEAT STRIP_TAC);;
e(COND_CASES_TAC);;
e(ASM_SIMP_TAC[NSUM_SING]);;
e(ASM_SIMP_TAC[NSUM_CLAUSES]);;
e(COND_CASES_TAC);;
e(ASM_SIMP_TAC[FINITE_NUMSEG; NSUM_CLAUSES]);;
e(ASM_SIMP_TAC[ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG; ADD_SYM]);;
e(ASM_SIMP_TAC[NSUM_CLAUSES]);;
let NSUM_CLAUS2_NUMSEG = top_thm();;
(* That's a fine interactive proof, and I expected to turn it into a tactic
script by just replacing the e's with THEN. But it didn't work, and the
problem is the 2nd COND_CASES_TAC: *)
let NSUM_CLAUS2_NUMSEG = prove
(`(!m. nsum (m..0) f = if m = 0 then f 0 else 0) /\
!m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n) else
0`,
REWRITE_TAC[NUMSEG_CLAUS] THEN REPEAT STRIP_TAC THEN
COND_CASES_TAC THEN
ASM_SIMP_TAC[NSUM_SING] THEN
ASM_SIMP_TAC[NSUM_CLAUSES] THEN COND_CASES_TAC THEN
ASM_SIMP_TAC[FINITE_NUMSEG; NSUM_CLAUSES] THEN
ASM_SIMP_TAC[ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG; ADD_SYM] THEN
ASM_SIMP_TAC[NSUM_CLAUSES]);;
(* That script earns an error of
Exception: Failure "find_term".
So I just took it out the 2nd COND_CASES_TAC, and it works fine: *)
let NSUM_CLAUS2_NUMSEG = prove
(`(!m. nsum (m..0) f = if m = 0 then f 0 else 0) /\
!m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n) else
0`,
REWRITE_TAC[NUMSEG_CLAUS] THEN REPEAT STRIP_TAC THEN
COND_CASES_TAC THEN
ASM_SIMP_TAC[NSUM_SING] THEN ASM_SIMP_TAC[NSUM_CLAUSES] THEN
ASM_SIMP_TAC[FINITE_NUMSEG; NSUM_CLAUSES] THEN
ASM_SIMP_TAC[ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG; ADD_SYM] THEN
ASM_SIMP_TAC[NSUM_CLAUSES]);;
(* But if I remove the 2nd the 2nd COND_CASES_TAC from my interactive proof, I
make no progress on the harder goal: *)
g `(!m. nsum (m..0) f = if m = 0 then f 0 else 0) /\
!m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n) else
0`;;
e(REWRITE_TAC[NUMSEG_CLAUS]);;
e(REPEAT STRIP_TAC);;
e(COND_CASES_TAC);;
e(ASM_SIMP_TAC[NSUM_SING]);;
e(ASM_SIMP_TAC[NSUM_CLAUSES]);;
e(ASM_SIMP_TAC[FINITE_NUMSEG; NSUM_CLAUSES]);;
e(ASM_SIMP_TAC[ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG; ADD_SYM]);;
e(ASM_SIMP_TAC[NSUM_CLAUSES]);;
(* --
Best,
Bill *)
------------------------------------------------------------------------------
Keep yourself connected to Go Parallel:
BUILD Helping you discover the best ways to construct your parallel projects.
http://goparallel.sourceforge.net
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
