Examples (7)
■ 今更ですが，0<=SUC n は
# LE_0;;
val it : thm = |- !n. 0 <= n
で賄えることに気付きました．
# g`!n. sum(0..n)(\k. &k)= &n*( &n+ &1)/ &2`;;
val it : goalstack = 1 subgoal (1 total)`!n. sum (0..n) (\k. &k) = &n * (&n + &1) / &2`
# e INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)0 [`sum (0..n) (\k. &k) = &n * (&n + &1) / &2`]
`sum (0..SUC n) (\k. &k) = &(SUC n) * (&(SUC n) + &1) / &2`
`sum (0..0) (\k. &k) = &0 * (&0 + &1) / &2`
# e (REWRITE_TAC[SUM_CLAUSES_NUMSEG] THEN REAL_ARITH_TAC);;
val it : goalstack = 1 subgoal (1 total)0 [`sum (0..n) (\k. &k) = &n * (&n + &1) / &2`]
`sum (0..SUC n) (\k. &k) = &(SUC n) * (&(SUC n) + &1) / &2`
# e (ASM_REWRITE_TAC[SUM_CLAUSES_NUMSEG;LE_0;ADD1;GSYM(REAL_ADD)] THEN REAL_ARIT
H_TAC);;
val it : goalstack = No subgoals
まとめると
# prove(`!n. sum(1..n)(\k. &k* &k )= &n*( &n+ &1)*(&2* &n+ &1)/ &6`,
INDUCT_TAC THEN ASM_REWRITE_TAC[SUM_CLAUSES_NUMSEG;LE_0;ADD1;GSYM(REAL_ADD);my] THEN
REAL_ARITH_TAC);;
val it : thm =
|- !n. sum (1..n) (\k. &k * &k) = &n * (&n + &1) * (&2 * &n + &1) / &6
■ ある証明アシスタントの入門講座に出ていた例題です．
# g`!n. EVEN (n*(n+1))`;;
val it : goalstack = 1 subgoal (1 total)`!n. EVEN (n * (n + 1))`
# e INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)0 [`EVEN (n * (n + 1))`]
`EVEN (SUC n * (SUC n + 1))`
`EVEN (0 * (0 + 1))`
# e ARITH_TAC;;
val it : goalstack = 1 subgoal (1 total)0 [`EVEN (n * (n + 1))`]
`EVEN (SUC n * (SUC n + 1))`
# e(ASM_REWRITE_TAC[ARITH_RULE`SUC n*(SUC n+1)=n*(n+1)+2*(n+1)`;EVEN_ADD;EVEN_DO
UBLE]);;
val it : goalstack = No subgoals
まとめると
# prove(`!n. EVEN (n*(n+1))`, INDUCT_TAC THENL [ARITH_TAC;ASM_REWRITE_TAC[ARITH_
RULE`SUC n*(SUC n+1)=n*(n+1)+2*(n+1)`;EVEN_ADD;EVEN_DOUBLE]]);;
val it : thm = |- !n. EVEN (n * (n + 1))
:numでのcutoffが絡むとSOSが便利です．
# g`!n. EVEN (n*(n-1))`;;
val it : goalstack = 1 subgoal (1 total)`!n. EVEN (n * (n - 1))`
# e INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)0 [`EVEN (n * (n - 1))`]
`EVEN (SUC n * (SUC n - 1))`
`EVEN (0 * (0 - 1))`
# e ARITH_TAC;;
val it : goalstack = 1 subgoal (1 total)0 [`EVEN (n * (n - 1))`]
`EVEN (SUC n * (SUC n - 1))`
# e(ASM_REWRITE_TAC[SOS_RULE`SUC n*(SUC n-1)=n*(n-1)+2*n`;EVEN_ADD;EVEN_DOUBLE]);;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Translating proof certificate to HOL
val it : goalstack = No subgoals
まとめると
prove(`!n. EVEN (n*(n-1))`, INDUCT_TAC THENL[ ARITH_TAC; ASM_REWRITE_TAC[SOS_RULE`SUC n*(SUC n-1)=n*(n-1)+2*n`;EVEN_ADD;EVEN_DOUBLE] ] );;
■ その２です．
# g`!(P:B->bool) (f:A->B). (!y:B. P y)==>(!x. P (f x))`;;
val it : goalstack = 1 subgoal (1 total)`!P f. (!y. P y) ==> (!x. P (f x))`
# e(REPEAT STRIP_TAC THEN
FIRST_ASSUM(fun t->SIMP_TAC[SPEC`(f:A->B) x`t]));;
val it : goalstack = No subgoals
