Re: [Hol-info] newbie questions

Petros Papapanagiotou Mon, 23 Apr 2012 05:38:18 -0700

Hello Felix,

I'll try to answer as many of these as I can.
I'll skip the ones I am unsure about.

On 23/4/2012 6:06, Felix Breuer wrote:

1) How to undo definitions? It sometimes does happen that I make a "wrong" definition and would like to correct it on the REPL afterwards. How can I do that (without restarting OCaml)?

2) Where are definitions stored, anyway? There seems to be some global state involved. Is there a way to make definitions locally? Or to pass definitions around explicitly?

As far as I know, the answer is negative. There is no notion of a locale, or context, or module in HOL Light. All theorems are stored at the same "level" (the OCaml toplevel really).
Once you store a definition you are not allowed to undo or correct it, as this (for instance) may break some of the theorems you may have already proven with the old definition.

4) Is there some kind of REAL_FIELD_TAC? I found REAL_FIELD to be much more useful than REAL_ARITH and it would be great to have that as a tactic as well.

You can make REAL_FIELD into a tactic using CONV_TAC REAL_FIELD.
eg:
e (CONV_TAC REAL_FIELD);;

5) How can I make HOL Light compute something? On the one hand, I would like HOL to evaluate numerical expressions inside terms. I guess this is the purpose of REAL_RAT_REDUCE_CONV, but I could not figure out how to use that. On the other hand, if I define a function in HOL, it would be great to evaluate this function for some given arguments. How can I do that?

In what context do you want to compute things?
- If you simply have a term that you want to evaluate, you can use the conversion directly on it. It will return a theorem showing that your term is equal to a reduced version.
You can use "rhs o concl" to retrieve the result from such a theorem.
- If you want to compute things in the goal of your proof, you can use CONV_TAC with the same conversion.
- If you want to compute things in the assumptions of your proof, you can use (among other things) (RULE_ASSUM_TAC (CONV_RULE REAL_RAT_REDUCE_CONV)).

You basically use conversions to do such computations. If you have a custom function, you need to build a custom conversion to be able to compute it.
For simple definitions, you can use REWRITE_CONV[definition].
Depending on how complicated your definition is, this may become fairly hard.

7) When using the compact way of writing proofs, e.g.

let rewrite_x_lemma = prove

(`~(x:num=0) ==> ?n:num. x = n + 1`,

DISCH_TAC THEN (EXISTS_TAC `x - 1`) THEN ASM_SIMP_TAC[ARITH_RULE `~(x=0) ==> x >= 1`;ARITH_RULE `x >= 1 ==> x - 1 + 1 = x`]);;

is there a way to generate a "long form" of this with all intermediate subgoals? Or would I have to rewrite the whole thing manually using g() and e()?

I think there have been some efforts towards building a tool to do what you described, but as far as I know nothing complete has been built yet.
I believe your best option at the moment is to manually break down the proof into "e" commands.

let recip = define `recip f (0:num) = ((&1:real)/(f 0) :real) /\ recip f (n+1) = -- (&1/(f 0)) * sum (1..(n+1)) (\k. (f k) * recip f ((n + 1) - k))`;;

It is preferable if you can use new_recursive_definition with num_RECURSION.
(In this case it fails, so there must be something I'm missing in the definition.)

(* we do induction *)

You can do induction by:
e (MATCH_MP_TAC num_INDUCTION);;
before the second GEN_TAC below.
This would change the proof altogether (possibly solving some of your problems) so I'm mentioning it here in case you were looking for it.

(* base case *)

e(GEN_TAC);;

e(DISCH_TAC);;

e(REWRITE_TAC[gf_reciprocal;gf_times;gf_one;gf_mono]);;

e(REWRITE_TAC[FUN_EQ_THM]);;

e(GEN_TAC);;

e(COND_CASES_TAC);;

e(ASM_SIMP_TAC[NUMSEG_SING;SUM_SING;ARITH_RULE `0-0=0`]);;

e(REWRITE_TAC[recip]);;

e(SIMP_TAC[REAL_ARITH `x * &1 / x = x / x`]);;

e(ASM_SIMP_TAC[REAL_DIV_REFL]);;

This completes the proof of the base case. So far, so good. However, I was not happy with my use of ARITH_RULE and REAL_ARITH as this seemed a bit pedestrian. If ARITH_RULE can figure out 0-0=0 by itself, then there is certainly a tactic I can use so that I don't have to specify that 0-0=0 should be used? However, ARITH_TAC, does not work here. There is another instance of this problem below.

You can use:
e (CONV_TAC NUM_REDUCE_CONV);;
to get rid of the 0-0 term.

I think your use of REAL_ARITH is fairly standard if you want to do something quickly, but you can't find the corresponding theorem or automated method (or they simply don't exist).

let split_sum_lemma = MP (SPECL [`(\k. f k * recip f (x - k))`; `0`; `x:num`] SUM_CLAUSES_LEFT) (ARITH_RULE `0 <= x`);;

You could do:
let split_sum_lemma = MATCH_MP (SPEC `(\k. f k * recip f (x - k))` SUM_CLAUSES_LEFT) (SPEC_ALL LE_0);;

MATCH_MP is much more convenient in cases like this.

e(REWRITE_TAC[split_sum_lemma]);;

e(SIMP_TAC[ARITH_RULE `x - 0 = x`;ARITH_RULE `0 + 1 = 1`]);;

You can reduce this to:
e(REWRITE_TAC[split_sum_lemma;SUB_0;ADD_0;ADD_AC]);;

Question: Could I have done this in a different way, without specifying explicit substitutions into SUM_CLAUSES_LEFT?

See above! :)

Next, I wanted to substitute x = n + 1 so that I could apply the recursive definition of recip. This turned out to be a huge headache and I am sure that there is a much better way to do this.

As a first step, I proved that x indeed has the form x = n + 1:

let rewrite_x_lemma = prove

(`~(x:num=0) ==> ?n:num. x = n + 1`,

DISCH_TAC THEN (EXISTS_TAC `x - 1`) THEN ASM_SIMP_TAC[ARITH_RULE `~(x=0) ==> x >= 1`;ARITH_RULE `x >= 1 ==> x - 1 + 1 = x`]);;

Or simpler:
let rewrite_x_lemma = prove (`~(x:num=0) ==> ?n:num. x = n + 1`,
SIMP_TAC[num_CASES;GSYM ADD1; TAUT `!p q . ~p ==> q <=> p \/ q`]);;

e(ASSUME_TAC rewrite_x_lemma);;

e(UNDISCH_TAC `~(x = 0) ==> (?n. x = n + 1)`);;

e(UNDISCH_TAC `~(x = 0)`);;

e(MATCH_MP_TAC (TAUT `(b ==> c) ==> (a ==> ( a ==> b ) ==> c)`));;

e(DISCH_TAC);;

My problem here was that I could not figure out how to get the conclusion of my lemma as an assumption into my goal stack. So I placed the whole lemma into the assumptions, pulled the lemma and the fact that x /= 0 into the conclusion, applied a tautology there to simplify and then discharged the ?n. x = n + 1 again. How to do this better?

You are probably looking for this:
e (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP rewrite_x_lemma)));;

FIRST_X_ASSUM pops the first assumption on which the following tactic succeeds.
ASSUME_TAC adds a theorem as a new assumption.
MATCH_MP applies modus ponens by matching the lhs of rewrite_x_lemma to the assumption, thus returning the desired conclusion.

Generally the syntax:
e (FIRST_ASSUM (ASSUME_TAC o (some_rule)));;
is the most straightforward way to manipulate an assumption with some_rule.

I knew that x had the form I wanted, but how could I substitute n+1 for x? I did this:

e(ASSUME_TAC (MESON[] `(?n. x = n + 1) ==> x = (@n. x = n + 1) + 1`));;

e(UNDISCH_TAC `(?n. x = n + 1) ==> x = (@n. x = n + 1) + 1`);;

e(UNDISCH_TAC `(?n. x = n + 1)`);;

e(MATCH_MP_TAC (TAUT `(b ==> c) ==> (a ==> ( a ==> b ) ==> c)`));;

e(DISCH_TAC);;

Similarly to above, you could do this in one step:
e (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP (MESON[] `(?n. x = n + 1) ==> x = (@n. x = n + 1) + 1`))));;

Now I was here:
[...]
and wanted to do the substitution. However, e(ASM_REWRITE_TAC[]) did not do anything at this point. I had to resort to e(FIRST_X_ASSUM(SUBST1_TAC)) instead. Why?

I'm not sure I can give a complete answer to this.
I would suggest SUBST1_TAC for most such cases anyway as it gives precise control of the substitution.

All I wanted to do now was cancel the f(0)'s. I tried various things, without success:

I would personally go for:
e (FIRST_ASSUM (ASSUME_TAC o (MATCH_MP (REAL_FIELD `!x. ~(x = &0) ==> !a. x * --(&1 / x) * a = -- a`))));;
e (ASM_REWRITE_TAC[]);;

but I'm sure there are even better ways of doing this.

Hopefully I managed to give you some standard ways to do simple things in HOL Light.

Of course, there are usually many different ways to accomplish the same thing in HOL Light, and I'm sure quite a few people here could give more elegant solutions to your questions, but at least I hope mine helped a bit.

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.

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

------------------------------------------------------------------------------
For Developers, A Lot Can Happen In A Second.
Boundary is the first to Know...and Tell You.
Monitor Your Applications in Ultra-Fine Resolution. Try it FREE!
http://p.sf.net/sfu/Boundary-d2dvs2

_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] newbie questions

Reply via email to