PVSのこと(1)

 数学的帰納法の例です.

lem002 :  

  |-------
{1}   FORALL (n: nat, x: real): x ^ n = 0 => x = 0

Rerunning step: (induct "n")
Inducting on n on formula 1,
this yields  2 subgoals: 
lem002.1 :  

  |-------
{1}   FORALL (x: real): x ^ 0 = 0 => x = 0

Rerunning step: (skeep)
Skolemizing and keeping names of the universal formula in (+ -),
this simplifies to: 
lem002.1 :  

{-1}  x ^ 0 = 0
  |-------
{1}   x = 0

Rerunning step: (grind)
expt rewrites expt(x, 0)
  to 1
^ rewrites x ^ 0
  to 1
Trying repeated skolemization, instantiation, and if-lifting,

This completes the proof of lem002.1.

lem002.2 :  

  |-------
{1}   FORALL j:
        (FORALL (x: real): x ^ j = 0 => x = 0) IMPLIES
         (FORALL (x: real): x ^ (j + 1) = 0 => x = 0)

Rerunning step: (skeep*)
Iterating skeep in '*,
this simplifies to: 
lem002.2 :  

{-1}  FORALL (x: real): x ^ j = 0 => x = 0
{-2}  x ^ (j + 1) = 0
  |-------
{1}   x = 0

Rerunning step: (inst -1 "x")
Instantiating the top quantifier in -1 with the terms: 
 x,
this simplifies to: 
lem002.2 :  

{-1}  x ^ j = 0 => x = 0
[-2]  x ^ (j + 1) = 0
  |-------
[1]   x = 0

Rerunning step: (case "x ^ j * x = 0")
Case splitting on 
   x ^ j * x = 0, 
this yields  2 subgoals: 
lem002.2.1 :  

{-1}  x ^ j * x = 0
[-2]  x ^ j = 0 => x = 0
[-3]  x ^ (j + 1) = 0
  |-------
[1]   x = 0

Rerunning step: (use "zero_times3")
Using lemma zero_times3,
this simplifies to: 
lem002.2.1 :  

{-1}  x ^ j * x = 0 IFF x ^ j = 0 OR x = 0
[-2]  x ^ j * x = 0
[-3]  x ^ j = 0 => x = 0
[-4]  x ^ (j + 1) = 0
  |-------
[1]   x = 0

Rerunning step: (ground)
Applying propositional simplification and decision procedures,

This completes the proof of lem002.2.1.

lem002.2.2 :  

[-1]  x ^ j = 0 => x = 0
[-2]  x ^ (j + 1) = 0
  |-------
{1}   x ^ j * x = 0
[2]   x = 0

Rerunning step: (grind)
^ rewrites x ^ j
  to expt(x, j)
expt rewrites expt(x, 1 + j)
  to x * expt(x, j)
^ rewrites x ^ (1 + j)
  to x * expt(x, j)
Trying repeated skolemization, instantiation, and if-lifting,

This completes the proof of lem002.2.2.


This completes the proof of lem002.2.

Q.E.D.




Run time  = 0.22 secs.
Real time = 0.80 secs.

 次のレンマを参照すれば...

expt_nonzero: LEMMA n0x^i /= 0

当然

%|- lem02 : PROOF
%|- (then (skeep) (spread (use "expt_nonzero") ((grind) (grind))))
%|- QED

でOKです.しかし,そのもとのレンマは

  expt_nonzero_aux: LEMMA expt(n0x, n) /= 0;
Proof script:

(""
 (induct "n")
 (("1" (grind))
  ("2"
   (skosimp*)
   (expand "expt" -2)
   (inst?)
   (rewrite "zero_times3")
   (assert))))

なので結局は同じことです.