Hello everyone!
I have long wanted to get my feet wet using HOL Light and today I finally
took the time to do so. I succeeded in doing a small exercise proof, which,
however, is not very idiomatic. So, I have a lot of questions and I would
also love some suggestions for improvement of my proof. If any of you have
the time to look over my questions or my exercise, that would be great!
*Questions*
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?
3) HOL Light has large libraries for num, int and real. Are there also
libraries for abstract groups, rings or fields?
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.
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?
6) I am very curious about Mizar Light and would like to convert my
exercise to Mizar Light. I found the Mizar Light sources as well Freek's
paper on Mizar Light. However, at first glance it seemed as if the syntax
for Mizar Light given in the paper is quite different from what I saw in
the source. So... what is the current status of the project?
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()?
*Exercise*
Below is the proof I did today, with comments. There are three spots where
I am sure I did something the wrong way. At these spots, there are more
extensive comments, with sample evaluations on the REPL.
Goal: I could not find any library on generating functions (i.e., formal
power series as used in combinatorics), so I decided to define them from
scratch and prove that every FPS with non-zero first term has a reciprocal
(i.e. a multiplicative inverse).
(* formal power series are modeled as functions from num to real, i.e. we
just record the coefficients. *)
let gf_plus = new_definition `gf_plus = \(f:num->real) (g:num->real)
(n:num). (f n) + (g n) :real`;;
let gf_times = new_definition `gf_times = \(f:num->real) (g:num->real)
(n:num). (sum (0 .. n) (\k. (f k)*(g (n-k)))) :real`;;
let gf_mono = new_definition `gf_mono = \(a:real) (k:num) (n:num). if n = k
then a else &0 :real`;;
let gf_one = new_definition `gf_one = gf_mono (&1:real) (0:num)`;;
let gf_reciprocal = new_definition `gf_reciprocal = \(f:num->real)
(g:num->real). gf_times f g = gf_one`;;
(* the reciprocal of an fps f can be given explicitly, via the following
inductive definition. *)
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))`;;
(* Thm: recip f is a reciprocal of f *)
g `!(f:num->real). ~(f (0:num) = (&0:real)) ==> gf_reciprocal f (recip f)`;;
(* we do induction *)
(* 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.
We continue with the induction step. At this point, the goal stack looks
like this:
# val it : goalstack = 1 subgoal (1 total)
0 [`~(f 0 = &0)`]
1 [`~(x = 0)`]
`sum (0..x) (\k. f k * recip f (x - k)) = &0`
I did:
let split_sum_lemma = MP (SPECL [`(\k. f k * recip f (x - k))`; `0`;
`x:num`] SUM_CLAUSES_LEFT) (ARITH_RULE `0 <= x`);;
e(REWRITE_TAC[split_sum_lemma]);;
e(SIMP_TAC[ARITH_RULE `x - 0 = x`;ARITH_RULE `0 + 1 = 1`]);;
to obtain:
# val it : goalstack = 1 subgoal (1 total)
0 [`~(f 0 = &0)`]
1 [`~(x = 0)`]
`f 0 * recip f x + sum (1..x) (\k. f k * recip f (x - k)) = &0`
Question: Could I have done this in a different way, without specifying
explicit substitutions into SUM_CLAUSES_LEFT?
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`]);;
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?
Now the situation was this:
val it : goalstack = 1 subgoal (1 total)
0 [`~(f 0 = &0)`]
1 [`?n. x = n + 1`]
`f 0 * recip f x + sum (1..x) (\k. f k * recip f (x - k)) = &0`
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);;
Now I was here:
# val it : goalstack = 1 subgoal (1 total)
0 [`~(f 0 = &0)`]
1 [`x = (@n. x = n + 1) + 1`]
`f 0 * recip f x + sum (1..x) (\k. f k * recip f (x - k)) = &0`
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?
Anyway, I could now do the substitutions I wanted:
e(FIRST_X_ASSUM(SUBST1_TAC));;
e(REWRITE_TAC[recip]);;
which got me here:
# val it : goalstack = 1 subgoal (1 total)
0 [`~(f 0 = &0)`]
`f 0 *
--(&1 / f 0) *
sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) + 1) -
k)) +
sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) + 1) -
k)) =
&0`
All I wanted to do now was cancel the f(0)'s. I tried various things,
without success:
# e(REAL_ARITH_TAC);;
Exception: Failure "linear_ineqs: no contradiction".
# e(MATCH_MP_TAC (REAL_FIELD `~(x = &0) /\ (--y + z = c) ==> (x * -- &1
/ x * y + z = c)`));;
2 basis elements and 0 critical pairs
4 basis elements and 1 critical pairs
4 basis elements and 0 critical pairs
Exception: Failure "MATCH_MP_TAC: No match".
# e(ASM_SIMP_TAC[REAL_FIELD `~(x = &0) /\ (--y + z = c) ==> (x * -- &1 / x
* y + z = c)`]);;
2 basis elements and 0 critical pairs
4 basis elements and 1 critical pairs
4 basis elements and 0 critical pairs
val it : goalstack = 1 subgoal (1 total)
0 [`~(f 0 = &0)`]
`f 0 *
--(&1 / f 0) *
sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) + 1) -
k)) +
sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) + 1) -
k)) =
&0`
# e(CONV_TAC REAL_RAT_REDUCE_CONV);;
val it : goalstack = 1 subgoal (1 total)
0 [`~(f 0 = &0)`]
`f 0 *
--(&1 / f 0) *
sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) + 1) -
k)) +
sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) + 1) -
k)) =
&0`
The only thing that helped was to manually substitute the correct
expressions into ~(x = &0) /\ (--y + z = c) ==> (x * -- &1 / x * y + z =
c) to be able to cancel the f(0)'s. The good news is that after that,
everything went through:
e(MATCH_MP_TAC (REAL_FIELD `~(f 0 = &0) /\ -- sum (1..(@n. x = n + 1) + 1)
(\k. f k * recip f (((@n. x = n + 1) + 1) - k)) + sum (1..(@n. x = n + 1) +
1) (\k. f k * recip f (((@n. x = n + 1) + 1) - k)) = &0 ==> f 0 * --(&1 / f
0) * sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) + 1)
- k)) + sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) +
1) - k)) = &0`));;
e(ASM_SIMP_TAC[]);;
e(SIMP_TAC[REAL_FIELD `--a + a = &0`]);;
let GF_RECIP_EXPLICIT_FORM = top_thm();;
Okay, this is it! Any help is appreciated! For convenience I past the
entire proof script again below in a more compact form. But this
far-too-long-email stops here. :)
Thanks,
Felix
(* formal power series are modeled as functions from num to real, i.e. we
just record the coefficients. *)
let gf_plus = new_definition `gf_plus = \(f:num->real) (g:num->real)
(n:num). (f n) + (g n) :real`;;
let gf_times = new_definition `gf_times = \(f:num->real) (g:num->real)
(n:num). (sum (0 .. n) (\k. (f k)*(g (n-k)))) :real`;;
let gf_mono = new_definition `gf_mono = \(a:real) (k:num) (n:num). if n = k
then a else &0 :real`;;
let gf_one = new_definition `gf_one = gf_mono (&1:real) (0:num)`;;
let gf_reciprocal = new_definition `gf_reciprocal = \(f:num->real)
(g:num->real). gf_times f g = gf_one`;;
(* the reciprocal of an fps f can be given explicitly, via the following
inductive definition. *)
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))`;;
(* Thm: recip f is a reciprocal of f *)
g `!(f:num->real). ~(f (0:num) = (&0:real)) ==> gf_reciprocal f (recip f)`;;
(* we do induction *)
(* 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]);;
(* induction step *)
let split_sum_lemma = MP (SPECL [`(\k. f k * recip f (x - k))`; `0`;
`x:num`] SUM_CLAUSES_LEFT) (ARITH_RULE `0 <= x`);;
e(REWRITE_TAC[split_sum_lemma]);;
e(SIMP_TAC[ARITH_RULE `x - 0 = x`;ARITH_RULE `0 + 1 = 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`]);;
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);;
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);;
(* for some reason, e(ASM_REWRITE_TAC[]) does not help at this point.
instead: *)
e(FIRST_X_ASSUM(SUBST1_TAC));;
e(REWRITE_TAC[recip]);;
e(MATCH_MP_TAC (REAL_FIELD `~(f 0 = &0) /\ -- sum (1..(@n. x = n + 1) + 1)
(\k. f k * recip f (((@n. x = n + 1) + 1) - k)) + sum (1..(@n. x = n + 1) +
1) (\k. f k * recip f (((@n. x = n + 1) + 1) - k)) = &0 ==> f 0 * --(&1 / f
0) * sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) + 1)
- k)) + sum (1..(@n. x = n + 1) + 1) (\k. f k * recip f (((@n. x = n + 1) +
1) - k)) = &0`));;
e(ASM_SIMP_TAC[]);;
e(SIMP_TAC[REAL_FIELD `--a + a = &0`]);;
let GF_RECIP_EXPLICIT_FORM = top_thm();;
(* as a corollary, we show that the reciprocal exists *)
g `!f. ~(f 0 = &0) ==> ?g. gf_reciprocal f g`;;
e(GEN_TAC);;
e(DISCH_TAC);;
e(EXISTS_TAC `recip f`);;
e(ASM_SIMP_TAC[GF_RECIP_EXPLICIT_FORM]);;
let GF_RECIP_EXISTS = top_thm();;
--
http://www.felixbreuer.net
------------------------------------------------------------------------------
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
