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))))
なので結局は同じことです.