Thanks, Petros & Michael! I didn't completely understand what you wrote, but I
see how Michael simplified Petros's proof. This is really nice, and I can
probably just modify your code to finish the exercise in footnote 23, p 67 of
the HOL Light tutorial:
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))`;;
g `!p p'. addN p p' 4 ==> (?q. addN p q 3 /\ p' = SUC q)`;;
e (REPEAT GEN_TAC);;
e (SIMP_TAC[addN]);;
e(STRIP_TAC);;
e (EXISTS_TAC `(s:num->num) 3`);;
e (ASM_MESON_TAC[LT;ARITH_RULE `SUC 3 = 4`]);;
let addfour_THM = top_thm();;
I don't mind using EXISTS_TAC, and this code seems to answer my original
question: how can I define a function (s in this case)and call it whenever I
want. I don't understand why we needed the typing (s:num->num), or why we need
parenthesis. That is,
EXISTS_TAC `s:num->num 3` gets Exception: Failure "Unparsed input following
term".
But I really don't understand why Michael's STRIP_TAC works. P 48 of the
tutorial says
STRIP_TAC has the effect of DISCH_TAC, GEN_TAC or CONJ_TAC.
At the time we use it, we have only the goal
`(?s. s 0 = p /\ s 4 = p' /\ (!m. m < 4 ==> s (SUC m) = SUC (s m)))
==> (?q. (?s. s 0 = p /\ s 3 = q /\ (!m. m < 3 ==> s (SUC m) = SUC (s m))) /\
p' = SUC q)`
So I thought that STRIP_TAC here meant DISCH_TAC, which of course has the
effect:
0 [`?s. s 0 = p /\ s 4 = p' /\ (!m. m < 4 ==> s (SUC m) = SUC (s m))`]
which isn't helpful, as opposed to Michael's extremely helpful
0 [`s 0 = p`]
1 [`s 4 = p'`]
2 [`!m. m < 4 ==> s (SUC m) = SUC (s m)`]
where s is "defined" at it would be with miz3's consider. What am I missing?
BTW here's my miz3 proof:
horizon := 0;;
timeout := 1;;
let AddFour = thm `;
thus !p p'. addN p p' 4 ==> ?q. addN p q 3 /\ p' = SUC q
proof
let p p' be num;
assume addN p p' 4;
consider s such that
s 0 = p /\ s 4 = p' /\ (!m. m < 4 ==> s (SUC m) = SUC (s m)) [sDef] by
-, addN;
consider q such that
q = s 3 [qDef];
SUC 3 = 4;
s 0 = p /\ s 3 = q /\ (!m. m < 3 ==> s (SUC m) = SUC (s m)) /\ p' = SUC q
by -, qDef, LT, sDef;
qed by -, addN;
`;;
And here's a synthesis of my miz3 proof and your ideas above, which works with
a MESON "solved at" number of 433,447:
g `addN p p' 4 ==> ?q. addN p q 3 /\ p' = SUC q`;;
e(SIMP_TAC[addN]);;
e(STRIP_TAC);;
e(SUBGOAL_THEN `?q. q = s 3` CHOOSE_TAC);;
e(ASM_MESON_TAC[]);;
e(SUBGOAL_THEN `SUC 3 = 4 /\ 3 < 4` ASSUME_TAC);;
e (ASM_MESON_TAC[LT; ARITH_RULE `SUC 3 = 4 /\ 3 < 4`]);;
e (ASM_MESON_TAC[LT]);;
let addfour_THM = top_thm();;
So I "succeeded" in defining q and not using EXISTS_TAC, as we see from my
assumption,
3 [`q = s 3`]
but I ran up a half-million in MESON units for something your proof did in 652,
which is nothing. What is MESON doing? I'm so spoiled from miz3, where MESON
does everything a first order prover should do, except it's weak on equational
reasoning, and by setting the timeout to 50 I get just about everything I
actually want by waiting for it. I'm very curious about how Freek and John got
miz3 to work so well.
--
Best,
Bill
------------------------------------------------------------------------------
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
