Re: [Hol-info] Learning HOL Light

[Bill R. <ri...@ma...>]

I have a question about X_CHOOSE_TAC and another vote for miz3.

In miz3 you can easily define variables with `consider'.  The HOL Light tutorial only explains two ways to define variables, both in proofs (p 73--81) of the irrationality of sqrt{2}.  John's p 78 Mizar-like `consider' is close to miz3's, but I do not understand the code and I've found no HOL Light source code that seems to be using the idea.  I believe the only other variable definition in the tutorial is on p 74:
e(DISCH_THEN(X_CHOOSE_THEN 'm:num' SUBST_ALL_TAC));;
In the HOL Light source code I see variants of this, but always with DISCH.  I use DISCH_THEN(CHOOSE_TAC) below.  How can I use X_CHOOSE_TAC without DISCH?

John has a nice Mizar-like proof of the irrationality of sqrt{2} using his consider on p 81. I turned it into a normal tactics proof, but my code below looks clumsy.  It looks odd the way I add assumptions by SUBGOAL_THEN and then in one line prove the sub-goal.  I bet this can be done in one line.  I think my use of X_CHOOSE_TAC and DISCH is odd.  It's fine to only define variables through a "existentially quantified conclusion" like ?x.alpha, because when we define x, it no doubt satisfies some property alpha, thus ?x.alpha must be true.  So I made my ?x.alpha a sub-goal, proved it, and then used 
MP_TAC(ASSUME `?x.alpha`) 
to make ?x.alpha the antecedent of the goal, and then used 
DISCH_THEN(CHOOSE_TAC)
to define the variable x and make alpha an assumption.  Then we go back to the original goal.  Can someone tell me a better way?

-- 
Best,
Bill 

g `!p q. p * p = 2 * q * q ==> q = 0`;;
e(MATCH_MP_TAC num_WF);;
e(REPEAT STRIP_TAC);;
e(SUBGOAL_THEN `EVEN p` ASSUME_TAC);;
e(ASM_MESON_TAC[EVEN_EXISTS; EVEN_MULT]);;
e(SUBGOAL_THEN `?m. p = 2 * m` ASSUME_TAC);;
e(ASM_MESON_TAC[EVEN_EXISTS]);;
e(MP_TAC(ASSUME `?m. p = 2 * m`));;
e(DISCH_THEN(CHOOSE_TAC));;
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(ASM_MESON_TAC[MULT_EQ_0]);;
e(SUBGOAL_THEN `p * p <= q * q` ASSUME_TAC);;
e(ASM_MESON_TAC[LE_MULT2]);;
e(SUBGOAL_THEN `p * p = 2 * q * q /\ p * p <= q * q ==> q * q = 0` ASSUME_TAC);;
e(ARITH_TAC);;
e(SUBGOAL_THEN `q * q = 0` ASSUME_TAC);;
e(ASM_MESON_TAC[MULT_EQ_0]);;
e(ASM_MESON_TAC[MULT_EQ_0]);;