読者です 読者をやめる 読者になる 読者になる

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.