Hello Ramana, On 13/12/2012 12:53, Bill Richter wrote: > Petros, I really like your fix of my code,
Glad I could help. > and it's even nicer than Ramana's, although I need to understand why his > CHOOSE_TAC(ASSUME t) works. Your fix > SUBGOAL_THEN `?m. p = 2 * m` CHOOSE_TAC > is especially appealing to me, because you're usage just substitutes > CHOOSE_TAC for ASSUME_TAC, as e.g. in > SUBGOAL_THEN `EVEN p` ASSUME_TAC > I don't understand that usage yet, but I'm used it by now. I am not sure which part confuses you in order to help out. You can read "SUBGOAL_THEN t X" as "create a new subgoal t, then do X with it". If X is ASSUME_TAC then it is added as an assumption as-is. You can read "CHOOSE_TAC" as "take an existentially quantified theorem and add its body as an assumption". Actually things like "CHOOSE_TAC(ASSUME t)" and "MP_TAC(ASSUME t)" only work in this example because "t" is already an assumption. > I think you're saying that I can't avoid using two lines per statement: first > state the statement as a subgoal, and then prove it on the next line. So > that's fine. You can sometimes. If your subgoal is general, you can prove it (either as an external lemma or inline using "prove") and use it in one line. eg: You can convert this: e(SUBGOAL_THEN `q * q = 0` ASSUME_TAC);; [...] e(ASM_MESON_TAC[MULT_EQ_0]);; (* used to prove q = 0 *) to this: e(MATCH_MP_TAC (prove(`q * q = 0 ==> q = 0`,REWRITE_TAC[MULT_EQ_0]));; [...] It depends on your style and what you find better/cleaner. I think a lot of these things actually boil down to personal style. > But I find these 3 lines embarrassing: > > e(SUBGOAL_THEN `p = 2 * m /\ p * p = 2 * q * q ==> q * q = 2 * m * m` > ASSUME_TAC);; > e(CONV_TAC NUM_RING);; > e(ASM_MESON_TAC[]);; > > At this point my assumption-list and goal is > > 0 [`!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0)`] > 1 [`p * p = 2 * q * q`] > 2 [`p = 2 * m`] > 3 [`q < p`] > 4 [`q * q = 2 * m * m ==> m = 0`] > > `q * q = 2 * m * m` > > It's obvious that assumptions 1 & 2 imply the goal, and NUM_RING can prove > it. So intead of these 3 lines, I wanted to write > e(ASM_MESON_TAC[NUM_RING]);; > But I can't do that, because NUM_RING isn't a theorem. I had a similar > embarrassing problem with ARITH_TAC, but John's trick got rid of it. I am not exactly sure what your best option is here. I would go for: e (UNDISCH_TAC `p * p = 2 * q * q`);; e (UNDISCH_TAC `p = 2 * m`);; e (CONV_TAC NUM_RING);; but I don't think this is much less "embarrassing" than yours. I am as curious as you if someone could come up with a more elegant way of dealing with this. Having a more computer science/engineering point of view, little problems like this often lead me to write my own tactics to do things "my way" (and sometimes later discover there was a HOL way all along). On a different note, e(SUBGOAL_THEN `q * q = 2 * m * m ==> m = 0` ASSUME_TAC);; is not really necessary. 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
