Petros, I really like your fix of my code, 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 have a new HOL Light proof runs faster because I added an extra step, and I
eliminated an embarrassment (see below) by using John's trick !x. 2 * x <= x
==> x = 0 from his earlier proof:
g `!p q. p * p = 2 * q * q ==> q = 0`;;
e(MATCH_MP_TAC num_WF);;
e(REPEAT STRIP_TAC);;
e(SUBGOAL_THEN `?m. p = 2 * m` CHOOSE_TAC);;
e(ASM_MESON_TAC[EVEN_EXISTS;EVEN_MULT]);;
e(DISJ_CASES_TAC(ARITH_RULE `q < p \/ p <= q`));;
e(SUBGOAL_THEN `q * q = 2 * m * m ==> m = 0` ASSUME_TAC);;
e(ASM_MESON_TAC[]);;
e(SUBGOAL_THEN `q * q = 2 * m * m` ASSUME_TAC);;
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[]);;
e(SUBGOAL_THEN `m = 0` ASSUME_TAC);;
e(ASM_MESON_TAC[]);;
e(SUBGOAL_THEN `q * q = 0` ASSUME_TAC);;
e(ASM_MESON_TAC[MULT_CLAUSES]);;
e(ASM_MESON_TAC[MULT_EQ_0]);;
e(SUBGOAL_THEN `p * p <= q * q` ASSUME_TAC);;
e(ASM_MESON_TAC[LE_MULT2]);;
e(SUBGOAL_THEN `!x. 2 * x <= x ==> x = 0` ASSUME_TAC);;
e(ARITH_TAC);;
e(ASM_MESON_TAC[LTE_CASES; LE_MULT2; MULT_EQ_0]);;
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. 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.
BTW I don't actually need ARITH_TAC for John's trick, as this miz3 proof shows:
let _THM = thm `;
thus !x. 2 * x <= x ==> x = 0
proof
let x be num;
assume 2 * x <= x;
2 <= 1 \/ x = 0 by -, MULT_CLAUSES, LE_MULT_RCANCEL;
qed by -, LT, TWO, LET_ANTISYM;
`;;
BTW I realized that
e(DISCH_THEN(CHOOSE_TAC));;
has the same effect as something that seems a lot simpler to me:
e(SIMP_TAC[LEFT_IMP_EXISTS_THM]);;
e(STRIP_TAC THEN DISCH_TAC);;
This is quite simple:
LEFT_IMP_EXISTS_THM;;
val it : thm = |- !P Q. (?x. P x) ==> Q <=> (!x. P x ==> Q)
And it makes me wonder if the way HOL tactics evolved had to do with what was
simple and appealing in the Lambda Calculus...
--
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
