On 17/12/12 03:19, Petros Papapanagiotou wrote: > 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. You could also use the Pa module that Vincent Aravantinos recently posted (http://users.encs.concordia.ca/~vincent/Software_files/q.ml): e (Pa.SUBGOAL_THEN "s 0 = p" ASSUME_TAC) so that the new ‘s’ mentioned here picks up the right type from the goal. > 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));; Or even use STRIP_ASSUME_TAC. And though using DISCH_THEN (X_CHOOSE_TAC `s:num->num`) is probably good practice in general (fixing the names that will appear in the goal is better than relying on the names that the system chooses for you), you could just use STRIP_TAC and save yourself the hassle. Indeed, none of the manipulations after the call to SIMP_TAC are going to make any difference to ASM_MESON_TAC. You could just try (taking from Petros’ script) SIMP_TAC[addN] THEN ASM_MESON_TAC[LT;ARITH_RULE `SUC 3 = 4`] Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
