Hello Petros,
thank you very much for your detailed explanation. It helped a lot!
In case this is useful to others, I paste the streamlined version below. It
comes in two versions. First with Petros' corrections, and second using
INDUCT_TAC. As it turns out, with INDUCT_TAC I don't have to do the
substitution acrobatics in the middle, however, I do have to do an
additional case analysis in the end (which is is easy). On the whole
INDUCT_TAC helps :)
Best,
Felix
(********************* CORRECTED VERSION ********************)
(* 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]);;
e(CONV_TAC NUM_REDUCE_CONV);;
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 = MATCH_MP (SPEC `(\k. f k * recip f (x - k))`
SUM_CLAUSES_LEFT) (SPEC_ALL LE_0);;
e(REWRITE_TAC[split_sum_lemma]);;
e(REWRITE_TAC[SUB_0;ADD_0;ADD_AC]);;
let rewrite_x_lemma = prove
(`~(x:num=0) ==> ?n:num. x = n + 1`,SIMP_TAC[num_CASES;GSYM ADD1;TAUT
`~p ==> q <=> p \/ q`]);;
e(FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP rewrite_x_lemma)));;
e(FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP (MESON[] `(?n. x = n + 1) ==> x =
(@n. x = n + 1) + 1`))));;
e(FIRST_X_ASSUM(SUBST1_TAC));;
e(REWRITE_TAC[recip]);;
e(FIRST_ASSUM (ASSUME_TAC o (MATCH_MP (REAL_FIELD `!x. ~(x = &0) ==> !a. x
* -- (&1 / x) * a = -- a`))));;
e(ASM_REWRITE_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();;
(***************** INDUCT_TAC VERSION **********************)
(* 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(INDUCT_TAC);;
e(ASM_SIMP_TAC[NUMSEG_SING;SUM_SING]);;
e(CONV_TAC NUM_REDUCE_CONV);;
e(REWRITE_TAC[recip]);;
e(SIMP_TAC[REAL_ARITH `x * &1 / x = x / x`]);;
e(ASM_SIMP_TAC[REAL_DIV_REFL]);;
let split_sum_lemma = MATCH_MP (SPEC `(\k. f k * recip f (x - k))`
SUM_CLAUSES_LEFT) (SPEC_ALL LE_0);;
e(REWRITE_TAC[split_sum_lemma;SUB_0;ADD_0;ADD_AC]);;
e(REWRITE_TAC[ADD1]);;
e(REWRITE_TAC[recip]);;
e(FIRST_ASSUM (ASSUME_TAC o (MATCH_MP (REAL_FIELD `!x. ~(x = &0) ==> !a. x
* -- (&1 / x) * a = -- a`))));;
e(ASM_REWRITE_TAC[]);;
e(SIMP_TAC[REAL_FIELD `--a + a = &0`]);;
e(COND_CASES_TAC);;
e(UNDISCH_TAC `x + 1 = 0` THEN ASM_SIMP_TAC[ARITH_RULE `~(x + 1 = 0)`]);;
e(ASM_SIMP_TAC[]);;
2012/4/23 Petros Papapanagiotou <[email protected]>
> 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.
>
>
--
http://www.felixbreuer.net
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
