Continuing to study whether HOL Light tactics proofs can be ported to miz3, and
if miz3 can explain tactics proofs, I turn to John's inductive proof (p 52 ff)
of the sum of the first n natural numbers. John writes on p 53 "The resulting
goal may look like a mess", but I think the problem is just that
NSUM_CLAUSES_NUMSEG is oddly stated. So I wrote a miz3 proof (below) of a
variant
NSUM_CLAUS_NUMSEG : thm =
|- ∀f. (∀ m. nsum (m..0) f = (if m = 0 then f 0 else 0)) ∧
(∀ m n.
nsum (m..SUC n) f =
(if m <= SUC n then nsum (m..n) f + f (SUC n) else 0))
We can substitute NSUM_CLAUS_NUMSEG into John's p 53 proof:
let th = prove
(`!n. nsum(1..n) (\i. i) = (n * (n + 1)) DIV 2`,
MATCH_MP_TAC num_INDUCTION THEN
SIMP_TAC[NSUM_CLAUS_NUMSEG] THEN ARITH_TAC);;
and I don't think we get a mess:
g `!n. nsum(1..n) (\i. i) = (n * (n + 1)) DIV 2`;;
e(MATCH_MP_TAC num_INDUCTION THEN SIMP_TAC[NSUM_CLAUS_NUMSEG]);;
`(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2 /\
(!n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2
==> (if 1 <= SUC n then (n * (n + 1)) DIV 2 + SUC n else 0) =
(SUC n * (SUC n + 1)) DIV 2)`
Now of course 1 <= SUC n, so it doesn't matter what the else clause is, and we
get the consequent
(n * (n + 1)) DIV 2 + SUC n = (SUC n * (SUC n + 1)) DIV 2
which is what we want. In John's goal, my else clause of 0 is replaced by the
correct by odd-looking (n * (n + 1)) DIV 2).
I'm guessing the reason NSUM_CLAUSES_NUMSEG gets its odd look is that it's
derived from the impressive-looking
ITERATE_CLAUSES_NUMSEG;;
val it : thm =
|- ∀ op. monoidal op
⇒ (∀ m. iterate op (m..0) f = (if m = 0 then f 0 else neutral op)) ∧
(∀ m n.
iterate op (m..SUC n) f =
(if m <= SUC n
then op (iterate op (m..n) f) (f (SUC n))
else iterate op (m..n) f))
And here there may be a reason for the else clause to be iterate op (m..n) f)
instead of neutral op.
--
Best,
Bill
horizon := 0;;
timeout := 50;;
parse_as_infix("NOTIN",(11, "right"));;
let NOTIN = new_definition
`! a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;;
let NSUM_CLAUS_NUMSEG = thm `;
let f be num->num;
thus (! m. nsum (m..0) f = if m = 0 then f 0 else 0) /\
! m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n) else 0
proof
! m. nsum (m..0) f = (if m = 0 then f 0 else 0) [mf0]
proof
let m be num;
cases;
suppose m = 0;
qed by -, NSUM_SING_NUMSEG;
suppose ~(m = 0) [m0];
0 < m by -, LT_NZ;
qed by m0, -, NSUM_TRIV_NUMSEG;
end;
! m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n)
else 0
proof
let m n be num;
FINITE (m..n) [mnFinite] by FINITE_NUMSEG;
~(SUC n <= n) by LT, LET_ANTISYM;
SUC n NOTIN (m..n) [TooBig] by -, IN_NUMSEG, NOTIN;
cases;
suppose m <= SUC n [case1];
m..SUC n = SUC n INSERT (m..n) by -, NUMSEG_REC;
nsum (m..SUC n) f = nsum (m..n) f + f (SUC n) by mnFinite, TooBig,
-, NSUM_CLAUSES, ADD_SYM, NOTIN;
qed by -, case1;
suppose ~(m <= SUC n) [case2];
SUC n < m by -, LET_CASES;
nsum (m..SUC n) f = 0 by -, NSUM_TRIV_NUMSEG;
qed by -, case2;
end;
qed by mf0, -;
`;;
------------------------------------------------------------------------------
Keep yourself connected to Go Parallel:
TUNE You got it built. Now make it sing. Tune shows you how.
http://goparallel.sourceforge.net
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
