Hello Bill, On 13/12/2012 10:32, Bill Richter wrote: > Let's try to port this proof to HOL Light up to qDef: > > g `addN p p' 4 ==> ?q. addN p q 3 /\ p' = SUC q`;; > e(SIMP_TAC[addN]);; > e(DISCH_THEN(X_CHOOSE_TAC `s: num->num`));; > e(SUBGOAL_THEN `s 0 = p` ASSUME_TAC);; > e(ASM_MESON_TAC[]);; > > It's OK to the last line, but MESON times out with Exception: Failure > "solve_goal: Too deep". I get the same problem using John's Mizar-like > `consider':
That is because the `s` and `p` in your subgoal do not match the `s` and `p` in your assumptions. If you replace: e(SUBGOAL_THEN `s 0 = p` ASSUME_TAC);; with: e(SUBGOAL_THEN `(s:num->num) 0 = p` ASSUME_TAC);; it will work. However, using SUBGOAL_THEN to obtain the conjuncts of your assumption is not very "elegant". You can do something like: e (FIRST_ASSUM (CONJUNCTS_THEN ASSUME_TAC));; or if you do not need the original assumption: e (POP_ASSUM (CONJUNCTS_THEN ASSUME_TAC));; or if you want to break all conjuncts in one go: e (REPEAT (POP_ASSUM (CONJUNCTS_THEN ASSUME_TAC)));; or the equivalent: e (POP_ASSUM (REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC));; I should note that for this proof you don't actually need to break down the assumption at all. MESON_TAC is powerful enough to handle it as-is (in fact using ASM_MESON_TAC puts the conjuncts back together in the background). Here is my take on the proof you are attempting: g `!p p'. addN p p' 4 ==> (?q. addN p q 3 /\ p' = SUC q)`;; e (REPEAT GEN_TAC);; e (SIMP_TAC[addN]);; e (DISCH_THEN (X_CHOOSE_THEN `s: num->num` (REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC)));; (* Or simply: *) (* e (DISCH_THEN (X_CHOOSE_TAC `s: num->num`));; *) e (EXISTS_TAC `(s:num->num) 3`);; e (ASM_MESON_TAC[LT;ARITH_RULE `SUC 3 = 4`]);; Regards, Petros -- Petros Papapanagiotou CISA, School of Informatics The University of Edinburgh Email: [email protected] --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ 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
