Re: [Hol-info] Learning HOL Light

[Petros P. <P.P...@sm...>]

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: P.P...@sm...

---
  The University of Edinburgh is a charitable body, registered in
  Scotland, with registration number SC005336.