PVSのこと（３）

　PVS は LK を素直にインプリメントしており，否定は直ちにシーケントの対辺に移されます．これは数についての等式において移項により辺々を和の形に直すことに相当します．また，SUBGOALの導入・証明は，本来の case として (P ∨ ¬P),S ==> T が P,S ==> T および (¬P),S ==> T に split され，更に後者が S ==> P,T となる，非常に透明度の高い仕様になっています．

lem085:lemma forall (a,b,c:real): a+b+c/=0 => a^3+b^3+c^3=3*a*b*c => (a-b)^2+(b-c)^2+(c-a)^2=0

%|- lem085 : PROOF
%|- (then (skeep) (name "s" "a+b+c") (name "t" "(a-b)^2+(b-c)^2+(c-a)^2")
%|-  (spread (case "s*t=2*( a ^ 3 + b ^ 3 + c ^ 3 - 3 * a * b * c)")
%|-   ((then (replace -4 * LR) (simplify -1) (use "zero_times3") (grind))
%|-    (grind))))
%|- QED

lem085 :  

  |-------
{1}   FORALL (a, b, c: real):
        a + b + c /= 0 =>
         a ^ 3 + b ^ 3 + c ^ 3 = 3 * a * b * c =>
          (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = 0

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

{-1}  a ^ 3 + b ^ 3 + c ^ 3 = 3 * a * b * c
  |-------
{1}   a + b + c = 0
{2}   (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = 0

Rerunning step: (name "s" "a+b+c")
Letting s name a + b + c,
this simplifies to: 
lem085 :  

{-1}  a + b + c = s
[-2]  a ^ 3 + b ^ 3 + c ^ 3 = 3 * a * b * c
  |-------
[1]   a + b + c = 0
[2]   (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = 0

Rerunning step: (name "t" "(a-b)^2+(b-c)^2+(c-a)^2")
Letting t name (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2,
this simplifies to: 
lem085 :  

{-1}  (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = t
[-2]  a + b + c = s
[-3]  a ^ 3 + b ^ 3 + c ^ 3 = 3 * a * b * c
  |-------
[1]   a + b + c = 0
[2]   (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = 0

Rerunning step: (case "s*t=2*( a ^ 3 + b ^ 3 + c ^ 3 - 3 * a * b * c)")
Case splitting on 
   s * t = 2 * (a ^ 3 + b ^ 3 + c ^ 3 - 3 * a * b * c), 
this yields  2 subgoals: 
lem085.1 :  

{-1}  s * t = 2 * (a ^ 3 + b ^ 3 + c ^ 3 - 3 * a * b * c)
[-2]  (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = t
[-3]  a + b + c = s
[-4]  a ^ 3 + b ^ 3 + c ^ 3 = 3 * a * b * c
  |-------
[1]   a + b + c = 0
[2]   (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = 0

Rerunning step: (replace -4 * LR)
Replacing using formula -4,
this simplifies to: 
lem085.1 :  

{-1}  s * t = 2 * (3 * a * b * c - 3 * a * b * c)
[-2]  (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = t
[-3]  a + b + c = s
[-4]  a ^ 3 + b ^ 3 + c ^ 3 = 3 * a * b * c
  |-------
[1]   a + b + c = 0
[2]   (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = 0

Rerunning step: (simplify -1)
Simplifying with decision procedures,
this simplifies to: 
lem085.1 :  

{-1}  s * t = 0
[-2]  (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = t
[-3]  a + b + c = s
[-4]  a ^ 3 + b ^ 3 + c ^ 3 = 3 * a * b * c
  |-------
[1]   a + b + c = 0
[2]   (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = 0

Rerunning step: (use "zero_times3")
Using lemma zero_times3,
this simplifies to: 
lem085.1 :  

{-1}  s * t = 0 IFF s = 0 OR t = 0
[-2]  s * t = 0
[-3]  (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = t
[-4]  a + b + c = s
[-5]  a ^ 3 + b ^ 3 + c ^ 3 = 3 * a * b * c
  |-------
[1]   a + b + c = 0
[2]   (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = 0

Rerunning step: (grind)
expt rewrites expt((a - b), 0)
  to 1
expt rewrites expt((a - b), 1)
  to a - b
expt rewrites expt((a - b), 2)
  to a * a - a * b + (b * b - a * b)
^ rewrites (a - b) ^ 2
  to a * a - a * b + (b * b - a * b)
expt rewrites expt((b - c), 0)
  to 1
expt rewrites expt((b - c), 1)
  to b - c
expt rewrites expt((b - c), 2)
  to b * b - b * c + (c * c - b * c)
^ rewrites (b - c) ^ 2
  to b * b - b * c + (c * c - b * c)
expt rewrites expt((c - a), 0)
  to 1
expt rewrites expt((c - a), 1)
  to c - a
expt rewrites expt((c - a), 2)
  to a * a - a * c + (c * c - a * c)
^ rewrites (c - a) ^ 2
  to a * a - a * c + (c * c - a * c)
expt rewrites expt((a - b), 0)
  to 1
expt rewrites expt((a - b), 1)
  to a - b
expt rewrites expt((a - b), 2)
  to a * a - a * b + (b * b - a * b)
^ rewrites (a - b) ^ 2
  to a * a - a * b + (b * b - a * b)
expt rewrites expt((b - c), 0)
  to 1
expt rewrites expt((b - c), 1)
  to b - c
expt rewrites expt((b - c), 2)
  to b * b - b * c + (c * c - b * c)
^ rewrites (b - c) ^ 2
  to b * b - b * c + (c * c - b * c)
expt rewrites expt((c - a), 0)
  to 1
expt rewrites expt((c - a), 1)
  to c - a
expt rewrites expt((c - a), 2)
  to a * a - a * c + (c * c - a * c)
^ rewrites (c - a) ^ 2
  to a * a - a * c + (c * c - a * c)
expt rewrites expt(a, 0)
  to 1
expt rewrites expt(a, 1)
  to a
expt rewrites expt(a, 2)
  to a * a
expt rewrites expt(a, 3)
  to a * (a * a)
^ rewrites a ^ 3
  to a * (a * a)
expt rewrites expt(b, 0)
  to 1
expt rewrites expt(b, 1)
  to b
expt rewrites expt(b, 2)
  to b * b
expt rewrites expt(b, 3)
  to b * (b * b)
^ rewrites b ^ 3
  to b * (b * b)
expt rewrites expt(c, 0)
  to 1
expt rewrites expt(c, 1)
  to c
expt rewrites expt(c, 2)
  to c * c
expt rewrites expt(c, 3)
  to c * (c * c)
^ rewrites c ^ 3
  to c * (c * c)
Trying repeated skolemization, instantiation, and if-lifting,

This completes the proof of lem085.1.

lem085.2 :  

[-1]  (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = t
[-2]  a + b + c = s
[-3]  a ^ 3 + b ^ 3 + c ^ 3 = 3 * a * b * c
  |-------
{1}   s * t = 2 * (a ^ 3 + b ^ 3 + c ^ 3 - 3 * a * b * c)
[2]   a + b + c = 0
[3]   (a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 = 0

Rerunning step: (grind)
expt rewrites expt(a, 0)
  to 1
expt rewrites expt(a, 1)
  to a
expt rewrites expt(a, 2)
  to a * a
expt rewrites expt(a, 3)
  to a * (a * a)
^ rewrites a ^ 3
  to a * (a * a)
expt rewrites expt(b, 0)
  to 1
expt rewrites expt(b, 1)
  to b
expt rewrites expt(b, 2)
  to b * b
expt rewrites expt(b, 3)
  to b * (b * b)
^ rewrites b ^ 3
  to b * (b * b)
expt rewrites expt(c, 0)
  to 1
expt rewrites expt(c, 1)
  to c
expt rewrites expt(c, 2)
  to c * c
expt rewrites expt(c, 3)
  to c * (c * c)
^ rewrites c ^ 3
  to c * (c * c)
expt rewrites expt((a - b), 0)
  to 1
expt rewrites expt((a - b), 1)
  to a - b
expt rewrites expt((a - b), 2)
  to a * a - a * b + (b * b - a * b)
^ rewrites (a - b) ^ 2
  to a * a - a * b + (b * b - a * b)
expt rewrites expt((b - c), 0)
  to 1
expt rewrites expt((b - c), 1)
  to b - c
expt rewrites expt((b - c), 2)
  to b * b - b * c + (c * c - b * c)
^ rewrites (b - c) ^ 2
  to b * b - b * c + (c * c - b * c)
expt rewrites expt((c - a), 0)
  to 1
expt rewrites expt((c - a), 1)
  to c - a
expt rewrites expt((c - a), 2)
  to a * a - a * c + (c * c - a * c)
^ rewrites (c - a) ^ 2
  to a * a - a * c + (c * c - a * c)
Trying repeated skolemization, instantiation, and if-lifting,

This completes the proof of lem085.2.

Q.E.D.

Run time  = 1.59 secs.
Real time = 2.59 secs.

lem086:lemma forall (a,b,c:real): a^2+b^2+c^2=0 => a=0 & b=0 & c=0 

%|- lem086 : PROOF
%|- (skeep)
%|- (lemma "sq_pos") (lemma "sq_eq_0")
%|- (repeat(then* (inst-cp * "a") (inst-cp * "b") (inst * "c")))
%|- (grind)
%|- QED

lem090:lemma forall (a,b,c:real): a+b+c/=0 => a^3+b^3+c^3=3*a*b*c => a=b & b=c & c=a

%|- lem090 : PROOF
%|- (then (skeep) (use* "lem085") (use* "lem086") (grind))
%|- QED