Hello Freek and everyone,
I have now translated my little HOL Light exercise to miz3 and I am very
pleased with how it turned out! Below are some of my thoughts on miz3 as
well as the HOL Light and miz3 versions of the proof.
* The miz3 version is not only readable, but also not too far away from
what I might write in an informal proof. This is great!
* The declarative language allowed me to drop a number of the more
convoluted tactics that I needed to use in the procedural proof - and that
I was having a very hard time with. For example, instead of doing
REWRITE_TAC[MATCH_MP (SPEC `(\k. f k * recip f (x - k))` SUM_CLAUSES_LEFT)
(SPEC_ALL LE_0)], I could now just give the theorems SUM_CLAUSES_LEFT, LE_0
as justifications.
* In general, I notice that I rarely need to use tactics as justifications
and can focus on theorems instead. For examples I can often replace "by
REWRITE_TAC[SOME_THM]" with "SOME_THM". I wonder why this fails in some
cases though (see below).
* On the whole, working with the vi interface to miz3 was very pleasant.
However, there were some (minor) pitfalls that I want to mention:
- Working with definitions requires a trick: If you want to make a couple
of definitions, you need to make sure that there are no blank lines between
your definitions and the theorem you are working on and then press Ctrl-C
RET in vim. Now your definitons are known to miz3, but the vim buffer will
not get updated. (Instead an error message will appear in the REPL.) Next,
you need to insert a blank line between your defintions and the theorem.
After this Ctrl-C RET will update the vim buffer as intended - and you can
now use your definitions.
- Of course you cannot use backticks inside a block of miz3 syntax. So if
you want to do something like (SPEC `(\k. f k * recip f (x - k))`
SUM_CLAUSES_LEFT) within miz3 you need to write it as (SPEC (parse_term
"(\\k. f k * recip f (x - k))") SUM_CLAUSES_LEFT). I.e.: use the parse_term
function, use double-quotes and escape your backslashes.
- Some syntax errors are not reported in the vim buffer but only on the
REPL. These syntax errors are reported as "Error: File "/tmp/miz3_4802.ml",
line 17, characters 20-21: Parse error:..." which is not helpful, because
at the time the error is reported, the temporary file in question has
already been deleted. It would be great if the offending line could be
printed on the REPL as well.
* Finally, I have two concrete questions about the miz3 proof that is given
below:
- Is there a way to drop the explicit reference to REWRITE_TAC from the
last two lines of the proof? I can drop REWRITE_TAC almost everywhere (and
list only the theorems I would pass to REWRITE_TAC) but for some reason
this does not work in these last two lines.
- Is there an elegant way to roll [5] and [6] into one line? Better yet,
can I drop [5] and [6] altogether and just use REAL_FIELD and [1] in the
line where, now, [6] is referenced?
Cheers,
Felix
miz3 proof:
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`;;
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))`;;
let GF_RECIP_EXPLICIT_FORM = thm `;
!(f:num->real). ~(f (0:num) = (&0:real)) ==> gf_reciprocal f (recip f)
proof
let f be num->real;
assume ~(f 0 = &0) [1];
!n. sum (0..n) (\k. f k * recip f (n - k)) = (if n = 0 then &1 else &0)
[2]
proof
sum (0..0) (\k. f k * recip f (0 - k)) = f 0 * recip f (0 - 0) by
NUMSEG_SING,SUM_SING;
.= f 0 * recip f 0;
.= f 0 * &1 / f 0 by recip;
.= f 0 / f 0;
.= &1 by REAL_DIV_REFL,1;
.= (if 0 = 0 then &1 else &0) [3];
!n. sum (0..n) (\k. f k * recip f (n - k)) = (if n = 0 then &1 else
&0)
==> sum (0..SUC n) (\k. f k * recip f (SUC n - k)) = (if SUC n =
0 then &1 else &0) [4]
proof
let n be num;
assume sum (0..n) (\k. f k * recip f (n - k)) = (if n = 0 then &1
else &0);
!x. ~(x = &0) ==> !a. x * -- (&1 / x) * a = -- a [5] by REAL_FIELD;
!a. f 0 * -- (&1 / (f 0)) * a = -- a [6] by 1,5;
sum (0..SUC n) (\k. f k * recip f (SUC n - k)) = (\k. f k * recip f
(SUC n - k)) 0 + sum (0 + 1..SUC n) (\k. f k * recip f (SUC n - k)) by
SUM_CLAUSES_LEFT,LE_0;
.= (f 0 * recip f (SUC n)) + sum (1..SUC n) (\k. f k * recip f
(SUC n - k)) by ADD_0,SUB_0,ADD_AC;
.= (f 0 * recip f (n + 1)) + sum (1..(n + 1)) (\k. f k * recip f
((n + 1) - k));
.= (f 0 * -- (&1/(f 0)) * sum (1..(n + 1)) (\k. (f k) * recip f
((n + 1) - k))) + sum (1..(n + 1)) (\k. f k * recip f ((n + 1) - k)) by
recip;
.= -- sum (1..(n + 1)) (\k. (f k) * recip f ((n + 1) - k)) + sum
(1..(n + 1)) (\k. f k * recip f ((n + 1) - k)) by 6;
.= &0;
.= (if SUC n = 0 then &1 else &0);
qed;
qed by INDUCT_TAC from 3,4;
(\n. sum (0..n) (\k. f k * recip f (n - k))) = (\n. (if n = 0 then &1
else &0)) [7] by REWRITE_TAC[FUN_EQ_THM],2;
qed by REWRITE_TAC[gf_reciprocal;gf_times;gf_one;gf_mono],1 from 7,7;
`;;
HOL Light proof (for comparison):
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/30 Felix Breuer <[email protected]>
> Thanks! That solved it. (I really should have thought of the backquotes
> myself, though.)
>
> Felix
>
>
> 2012/4/30 Freek Wiedijk <[email protected]>
>
>> Hi Felix,
>>
>> >4) I start gvim and load a file with the following content:
>> >
>> >let ARITHMETIC_SUM = thm ';
>> > !n. nsum(1..n) (\i. i) = (n*(n+1)) DIV 2
>> > proof
>> > qed by #INDUCT_TAC;
>> >';;
>>
>> The quotes should be backquotes. With this I think miz3
>> will try to execute this as ocaml source (it does not match
>> the pattern of a miz3 lemma). You can check this theory by
>> pasting the same text in the ocaml session to see whether
>> you get the same ocmal error.
>>
>> Anyway, it should be backquotes. Proofs are `; ... `
>> instead of '; ... '
>>
>> Freek
>>
>
>
>
> --
> http://www.felixbreuer.net
>
--
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
