Michael and Petros, thanks to your help, I wrote a tactics script for
REACHABLE_INVARIANT from p 67 of the HOL tutorial using the explicitly
sequential definition reachable of 65. Here's a simpler version of it, using
STRIP_TAC, EXISTS_TAC, and extra type annotations as you taught me to:
let addN = new_definition
`!p p' n.
addN p p' n <=> ?s.
s 0 = p /\ s n = p' /\
(!m. m < n ==> s (SUC m) = SUC (s m))`;;
let addN_CLAUSES = prove
(`! p p'. (addN p p' 0 <=> p = p') /\
!n. addN p p' (SUC n) <=> ?q. addN p q n /\ (SUC q) = p'`,
REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[addN; LT]
THENL [MESON_TAC[]; DISCH_TAC; STRIP_TAC; STRIP_TAC] THENL
[EXISTS_TAC `\m:num. p':num` THEN SIMP_TAC[];
EXISTS_TAC `(s:num->num) n`;
EXISTS_TAC `\m:num. if m < SUC n then s m else p':num`] THEN
REPEAT STRIP_TAC THEN ASM_MESON_TAC[LT_0; LT_REFL; LT; LT_SUC]);;
I like my tactics script (maybe someone can suggest a better), but I wish I had
been able to define variables and give them labels, as I did in the miz3 proof
below with "consider". EXISTS_TAC worked fine, but if you need to use a
defined variable more than once, it would look awkward to EXISTS_TAC it every
time you used it. One could argue that this is ugly and hard to read
`(\m. if m < SUC n then s m else p') (SUC m) =
SUC ((\m. if m < SUC n then s m else p') m)`
and that it would be nicer to call this function "t" and write instead
t (SUC m) = SUC (t m),
as I essentially do in my miz3 proof. I'm sure this can be done in HOL
tactics, I just haven't figured it out yet.
I did answer two beginner questions I posted earlier: how can you see the
entire goalstack, and how you debug a tactics script? More precisely, how can
you produce a tactics script when THEN works differently than it does in a
interactive proof and you have to use THENLs? The answer is that you can
gradually turn an interactive proof g & e proof into a tactics script, because
a tactics script is "really" just an interactive proof with one e-command.
I'll use my tactics script above as an example. It's basically this
"interactive" proof:
g `! p p'. (addN p p' 0 <=> p = p') /\
!n. addN p p' (SUC n) <=> ?q. addN p q n /\ (SUC q) = p'`;;
e(REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[addN; LT]
THENL [MESON_TAC[]; DISCH_TAC; STRIP_TAC; STRIP_TAC] THENL
[EXISTS_TAC `\m:num. p':num` THEN SIMP_TAC[];
EXISTS_TAC `(s:num->num) n`;
EXISTS_TAC `\m:num. if m < SUC n then s m else p':num`] THEN
REPEAT STRIP_TAC THEN ASM_MESON_TAC[LT_0; LT_REFL; LT; LT_SUC]);;
let addN_CLAUSES = top_thm();;
I took a interactive proof with lots of e-commands and gradually built an
interactive proof with only one e-command. You can see how I built it by
evaluating a top chunk, e.g.
g `! p p'. (addN p p' 0 <=> p = p') /\
!n. addN p p' (SUC n) <=> ?q. addN p q n /\ (SUC q) = p'`;;
e(REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[addN; LT]
THENL [MESON_TAC[]; DISCH_TAC; STRIP_TAC; STRIP_TAC]);;
val it : goalstack = 3 subgoals (3 total)
0 [`s 0 = p`]
1 [`s n = q`]
2 [`!m. m < n ==> s (SUC m) = SUC (s m)`]
3 [`SUC q = p'`]
`?s. s 0 = p /\
s (SUC n) = p' /\
(!m. m = n \/ m < n ==> s (SUC m) = SUC (s m))`
0 [`s 0 = p`]
1 [`s (SUC n) = p'`]
2 [`!m. m = n \/ m < n ==> s (SUC m) = SUC (s m)`]
`?q. (?s. s 0 = p /\ s n = q /\ (!m. m < n ==> s (SUC m) = SUC (s m))) /\
SUC q = p'`
0 [`p = p'`]
`?s. s 0 = p'`
So there exactly 3 goals, and each of them requires plugging in a variable, so
that requires 3 EXISTS_TAC. We can easily write all 3 EXISTS_TACs at once and
put them into the tactics script with THENL:
THENL
[EXISTS_TAC `\m:num. p':num` THEN SIMP_TAC[];
EXISTS_TAC `(s:num->num) n`;
EXISTS_TAC `\m:num. if m < SUC n then s m else p':num`]
Paste that into the big e-command and evaluate it, and you'll we see there are
2 goals, as the SIMP_TAC[] finished the first goal. As both goals need
STRIP_TAC-ing, I just use
THEN REPEAT STRIP_TAC
and now I have 6 goals, all of which are solved by ASM_MESON_TAC[] and some of
the arith.ml LT theorems. So I can finish the proof interactively (and it is
sure cool to know the whole goalstack!):
e(ASM_MESON_TAC[]);;
e(ASM_MESON_TAC[]);;
e(ASM_MESON_TAC[LT_0]);;
e(ASM_MESON_TAC[LT_REFL]);;
e(ASM_MESON_TAC[LT_REFL; LT]);;
e(ASM_MESON_TAC[LT_SUC; LT]);;
val it : goalstack = No subgoals
Yay! And then I can tactify this with last step with
THENL
[ASM_MESON_TAC[]; ASM_MESON_TAC[]; ASM_MESON_TAC[LT_0]; ASM_MESON_TAC[LT_REFL];
ASM_MESON_TAC[LT_REFL; LT]; ASM_MESON_TAC[LT_SUC; LT]]
but as John explains, why not just use all the LT theorems for all 6 cases, and
then we have my
THEN ASM_MESON_TAC[LT_0; LT_REFL; LT; LT_SUC]. Now John explains a lot about
interactive proof vs tactics scripts, but somehow I missed the point that with
a "one e-command" version of tactics script you can see whole goalstack, and if
you would just solve all the goals simultaneously, instead of working one goal
at a time, then you'd build your tactics script as you go. Of course I
probably wouldn't do that, but here's my 4-pass compiler to turn a interactive
proof vs tactics scripts:
First make the interactive proof with the g-command on top and each e-command
on it's own line and no blank lines. Then after you're done, evaluate all the
commands again from the top, and insert blank lines and TABs to indicate when
you switch over to a new goal. Now take a 3rd pass and incrementally build an
interactive proof with just one huge e-command underneath the g-command. Just
steal the top-most lines and put them in a THENL which goes at the end of the
huge e-command. You have to run it every time to make sure you didn't goof up
which goals you were working one. And then of course we must replace the
`;;<RET>e( with let THM_NAM = prove and a ,.
Is this all completely obvious? I didn't know it. Maybe someone has a better
way to do it. Anyway, it was a lot of fun writing this script!
--
Best,
Bill
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
timeout := 50;;
let addN_THM = thm `;
!p p'. (addN p p' 0 <=> p = p') /\
!n. addN p p' (SUC n) <=> ?q. addN p q n /\ SUC q = p'
proof
let p p' be num;
p = p' ==> addN p p' 0
proof
assume p = p' [pp'];
consider s such that s = \m:num. p;
qed by -, pp', addN, LT;
addN p p' 0 <=> p = p' [Clause0] by addN, -;
!n. addN p p' (SUC n) ==> ? q. addN p q n /\ SUC q = p' [Imp1]
proof
let n be num;
assume addN p p' (SUC n);
consider s such that
s 0 = p /\ s (SUC n) = p' /\ ! m. m < SUC n ==> SUC (s m) = s (SUC m)
[SUCnDef] by -, addN;
consider q such that q = s n [qDef];
SUC q = p' [qp'] by -, SUCnDef, LT;
s 0 = p /\ s n = q /\ !m. m < n ==> SUC (s m) = s (SUC m) by
qDef, LT, SUCnDef;
qed by -, qp', addN;
!n. (?q. addN p q n /\ SUC q = p') ==> addN p p' (SUC n)
proof
let n be num;
assume ? q. addN p q n /\ SUC q = p';
consider q such that
addN p q n /\ SUC q = p' [Assump] by -;
consider s such that
s 0 = p /\ s n = q /\ !m. m < n ==> SUC (s m) = s (SUC m) [nDef] by
-, addN;
consider t such that
t = \m. if m < SUC n then s m else p' [tDef];
t 0 = p /\ t (SUC n) = p' [tBotTop] by -, nDef, LT_0, LT_REFL;
! m. m < (SUC n) ==> SUC (t m) = t (SUC m)
proof
let m be num;
assume m < SUC n [mAss];
m = n \/ m < n by -, LT;
cases by -;
suppose m < n;
SUC (s m) = s (SUC m) /\ t m = s m /\ t (SUC m) = s (SUC m)
by -, LT, LT_SUC, tDef, nDef;
qed by -, nDef;
suppose m = n;
qed by -, LT, tDef, nDef, Assump, tBotTop;
end;
qed by tDef, tBotTop, -, addN;
! n. addN p p' (SUC n) <=> ? q. addN p q n /\ SUC q = p' by Imp1, -;
qed by Clause0, -;
`;;
------------------------------------------------------------------------------
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
