HOL Light vs PVS (2)
http://d.hatena.ne.jp/ehito/20130816/1376622603 の続編です．
前回は n≦n*n を sub goal としましたが，今回は結論に含め，帰納法の仮定を強くしました．
g `!n. &0 <= &n * (&n - &1) * (&n - &2) /\ &0 <= &n * (&n - &1) /\ &1 + &n + &n * (&n - &1) / &2 + &n * (&n - &1) * (&n - &2) / &6 <= &2 pow n` ;;
e INDUCT_TAC ;;
e ARITH_TAC ;;
e( REWRITE_TAC [pow;REAL] );;
e ASM_ARITH_TAC ;;
# g `!n. &0 <= &n * (&n - &1) * (&n - &2) /\ &0 <= &n * (&n - &1) /\ &1 + &n + &n
* (&n - &1) / &2 + &n * (&n - &1) * (&n - &2) / &6 <= &2 pow n` ;;
val it : goalstack = 1 subgoal (1 total)
`!n. &0 <= &n * (&n - &1) * (&n - &2) /\
&0 <= &n * (&n - &1) /\
&1 + &n + &n * (&n - &1) / &2 + &n * (&n - &1) * (&n - &2) / &6 <=
&2 pow n`
# e INDUCT_TAC ;;
val it : goalstack = 2 subgoals (2 total)
0 [`&0 <= &n * (&n - &1) * (&n - &2) /\
&0 <= &n * (&n - &1) /\
&1 + &n + &n * (&n - &1) / &2 + &n * (&n - &1) * (&n - &2) / &6 <=
&2 pow n`]
`&0 <= &(SUC n) * (&(SUC n) - &1) * (&(SUC n) - &2) /\
&0 <= &(SUC n) * (&(SUC n) - &1) /\
&1 +
&(SUC n) +
&(SUC n) * (&(SUC n) - &1) / &2 +
&(SUC n) * (&(SUC n) - &1) * (&(SUC n) - &2) / &6 <=
&2 pow SUC n`
`&0 <= &0 * (&0 - &1) * (&0 - &2) /\
&0 <= &0 * (&0 - &1) /\
&1 + &0 + &0 * (&0 - &1) / &2 + &0 * (&0 - &1) * (&0 - &2) / &6 <= &2 pow 0`
# e ARITH_TAC ;;
val it : goalstack = 1 subgoal (1 total)
0 [`&0 <= &n * (&n - &1) * (&n - &2) /\
&0 <= &n * (&n - &1) /\
&1 + &n + &n * (&n - &1) / &2 + &n * (&n - &1) * (&n - &2) / &6 <=
&2 pow n`]
`&0 <= &(SUC n) * (&(SUC n) - &1) * (&(SUC n) - &2) /\
&0 <= &(SUC n) * (&(SUC n) - &1) /\
&1 +
&(SUC n) +
&(SUC n) * (&(SUC n) - &1) / &2 +
&(SUC n) * (&(SUC n) - &1) * (&(SUC n) - &2) / &6 <=
&2 pow SUC n`
# e( REWRITE_TAC [pow;REAL] );;
val it : goalstack = 1 subgoal (1 total)
0 [`&0 <= &n * (&n - &1) * (&n - &2) /\
&0 <= &n * (&n - &1) /\
&1 + &n + &n * (&n - &1) / &2 + &n * (&n - &1) * (&n - &2) / &6 <=
&2 pow n`]
`&0 <= (&n + &1) * ((&n + &1) - &1) * ((&n + &1) - &2) /\
&0 <= (&n + &1) * ((&n + &1) - &1) /\
&1 +
(&n + &1) +
(&n + &1) * ((&n + &1) - &1) / &2 +
(&n + &1) * ((&n + &1) - &1) * ((&n + &1) - &2) / &6 <=
&2 * &2 pow n`
# e ASM_ARITH_TAC ;;
val it : goalstack = No subgoals
tst00:lemma forall(n:nat): 0 <= n * (n - 1) * (n - 2) and 0 <= n * (n - 1) and
1 + n + n * (n - 1) / 2 + n * (n - 1) * (n - 2) / 6 <= 2 ^ n
%|- tst00 : PROOF
%|- (spread (induct "n" 1)
%|- ((grind) (grind) (grind) (then (skeep*) (grind))))
%|- QED
tst00 :
|-------
{1} FORALL (n: nat):
0 <= n * (n - 1) * (n - 2) AND
0 <= n * (n - 1) AND
1 + n + n * (n - 1) / 2 + n * (n - 1) * (n - 2) / 6 <= 2 ^ n
Inducting on n on formula 1,
we get 4 subgoals:
tst00.1 :
|-------
{1} 0 <= 0 * (0 - 1) * (0 - 2)
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of tst00.1.
tst00.2 :
|-------
{1} 0 <= 0 * (0 - 1)
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of tst00.2.
tst00.3 :
|-------
{1} 1 + 0 + 0 * (0 - 1) / 2 + 0 * (0 - 1) * (0 - 2) / 6 <= 2 ^ 0
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of tst00.3.
tst00.4 :
|-------
{1} FORALL j:
0 <= j * (j - 1) * (j - 2) AND
0 <= j * (j - 1) AND
1 + j + j * (j - 1) / 2 + j * (j - 1) * (j - 2) / 6 <= 2 ^ j
IMPLIES
0 <= (j + 1) * (j + 1 - 1) * (j + 1 - 2) AND
0 <= (j + 1) * (j + 1 - 1) AND
1 + (j + 1) + (j + 1) * (j + 1 - 1) / 2 +
(j + 1) * (j + 1 - 1) * (j + 1 - 2) / 6
<= 2 ^ (j + 1)
Iterating skeep in '*,
tst00.4 :
{-1} 0 <= j * (j - 1) * (j - 2)
{-2} 0 <= j * (j - 1)
{-3} 1 + j + j * (j - 1) / 2 + j * (j - 1) * (j - 2) / 6 <= 2 ^ j
|-------
{1} 0 <= (j + 1) * (j + 1 - 1) * (j + 1 - 2) AND
0 <= (j + 1) * (j + 1 - 1) AND
1 + (j + 1) + (j + 1) * (j + 1 - 1) / 2 +
(j + 1) * (j + 1 - 1) * (j + 1 - 2) / 6
<= 2 ^ (j + 1)
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of tst00.4.
Q.E.D.
