Quelle  extra_examples.pvs

%% Examples of strategies in Extrategies 6.0
%% Cesar Munoz 
%% http://shemesh.larc.nasa.gov/people/cam/Extrategies
%% NASA LaRC
%%
%% The following formulas do not have intended semantics. 

extra_examples : THEORY
BEGIN

  x,y,z,w     : VAR real
  nzx,nzy,nzz : VAR nzreal
  px,py       : VAR posreal
  A           : VAR nzreal
  B,C,Delta   : VAR real
  sq(x:real)  : nnreal

  fcb: FORMULA % field, cancel-by
    x*nzz/(4*nzx) + x*nzz/(2*nzy) = x*nzz*nzx*nzy/8

%|- fcb : PROOF 
%|- (then (skeep) (field) (cancel-by 1 "nzz") (postpone))
%|- QED


  cf : LEMMA % cancel-formula
    4*(px*py) + (px*2)*px <= px*((x+1)*6) =>
    x = y

%|- cf : PROOF
%|- (then (skeep) (cancel-formula -1) (postpone))
%|- QED

  distrib : FORMULA % real-props, grind-reals
   4*(y+1)*1+0 = z AND
   2*(x+1)*1+0 = z AND
   x*(x+1) = y IMPLIES
   x*(x+2) = y*(y+2)

%|- distrib : PROOF
%|- (then (skeep) (real-props -1) (real-props -2 :distrib? nil)
%|-  (grind-reals :dontdistrib (-3 1)) (grind-reals) (postpone))
%|- QED

  replaces1 : FORMULA % replaces
    Delta = B*B - 4*A*C AND
    x = (sq(Delta) - B) / (2 * A)
    IMPLIES A * x*x + B * x + C = Delta OR Delta = 0

%|- replaces1 : PROOF
%|- (then (skeep) (replaces (-1 -2) :in 1 :hide? nil) (replaces) (postpone))
%|- QED

  replaces2 : FORMULA % replaces
    C = 3 AND
    Delta = B*B - 4*A*C AND
    x = (sq(Delta) - B) / (2 * A) AND
    A = 4 
    IMPLIES A * x*x + B * x + C = Delta OR Delta = 0

%|- replaces2 : PROOF
%|- (then (skeep) (replaces :from -2 :to -3) (replaces -2 :dir rl :in 1)
%|-  (replaces -1) (postpone))
%|- QED

  addformulas : LEMMA % add-formulas
    FORALL (x,y:ARRAY[nat->real]):
    x(0) <  y(0) AND
    x(1) <= y(1) AND
    x(2) >  y(2) AND
    x(3) >= y(3) AND
    x(4) =  y(4) IMPLIES
    x(5) <  y(5) OR
    x(6) <= y(6) OR
    x(7) >  y(7) OR
    x(8) >= y(8) OR
    x(9) =  y(9)

%|- addformulas : PROOF
%|- (then (skeep) (add-formulas -1 :hide? nil)
%|-  (add-formulas -2 -3 :hide? nil) (add-formulas -3 -5 :hide? nil)
%|-  (add-formulas -4 -7 :hide? nil) (add-formulas -5 -9 :hide? nil)
%|-  (add-formulas -6 1 :hide? nil) (add-formulas -7 2 :hide? nil)
%|-  (add-formulas -8 3 :hide? nil) (add-formulas -9 4 :hide? nil)
%|-  (hide (-1 -2 -3 -4 -5 -6 -7 -8 -9)) (add-formulas -5 5)
%|-  (add-formulas 2 -1) (add-formulas 3 -2) (add-formulas 4 -1)
%|-  (add-formulas 5 -1) (add-formulas 1 2) (add-formulas 2 3)
%|-  (add-formulas 1 2 :label "AddFormula") (postpone))
%|- QED

  subformulas : LEMMA % sub-formulas
    FORALL (x,y:ARRAY[nat->real]):
    x(0) <  y(0) AND
    x(1) <= y(1) AND
    x(2) >  y(2) AND
    x(3) >= y(3) AND
    x(4) =  y(4) IMPLIES
    x(5) <  y(5) OR
    x(6) <= y(6) OR
    x(7) >  y(7) OR
    x(8) >= y(8) 

%|- subformulas : PROOF
%|- (then (skeep) (sub-formulas -1 -2 :hide? nil)
%|-  (sub-formulas -2 -4 :hide? nil) (sub-formulas -3 -6 :hide? nil)
%|-  (sub-formulas -5 -8 :hide? nil) (sub-formulas -7 1 :hide? nil)
%|-  (sub-formulas -8 2 :hide? nil) (sub-formulas -9 3 :hide? nil)
%|-  (sub-formulas -10 4 :hide? nil) (hide (-1 -2 -3 -4 -5 -6 -7 -8))
%|-  (sub-formulas 1 -1) (sub-formulas 2 -2) (sub-formulas 3 -3)
%|-  (sub-formulas 4 -1) (sub-formulas 1 2) (sub-formulas 2 3)
%|-  (sub-formulas 1 2) (sub-formulas 1 -1 :label "SubFormula") (postpone))
%|- QED

  redlet1 : LEMMA % redlet
    -(LET a = (LET b = py in b+px) in a*py) =     
    -(LET a = (LET b = px in b*px) in a+px) IMPLIES
    LET a=px+py IN
    LET b=a*a IN
    a+b = px

%|- redlet1 : PROOF
%|- (then (skeep) (redlet -1) (redlet -1 "a" :nth 2) (redlet -1)
%|-  (redlet 1 :nth 2) (redlet -1 "b") (redlet 1) (postpone))
%|- QED

  triple(x,y,z) : [real,real,real] = (x,y,z)

  redlet2 : LEMMA % redlet, redlet*
    (LET d=3*x+2 IN LET (a,b,c)=(d,x*x,LET e=x+1 IN e*e) IN a=b+c+d) OR
    (LET d=3*x+2 IN LET (a,b,c)=triple(d,x*x,LET e=x+1 in e*e) IN a=b+c+d)

%|- redlet2 : PROOF
%|- (then (skeep) (redlet 1 "b") (redlet 2 :nth 2) (redlet 1)
%|-  (redlet* 2 :n 2) (redlet 1 "a") (redlet 1 "c") (postpone))
%|- QED

  skolet1 : LEMMA % skoletin
    -(LET a = (LET b = py in b+px) IN a*py) =     
    -(LET a = (LET b = px in b*px) IN a+px) IMPLIES
    LET a=px+py IN
    LET b=px*py IN
    a+b = a*b

%|- skolet1 : PROOF
%|- (then (skeep) (skoletin 1) (skoletin 1 :var "Myb" :hide? t)
%|-  (reveal "Myb:") (skoletin -3 "a" :nth 2 :postfix "_2") (skoletin -1)
%|-  (skoletin -3 :postfix "_2") (skoletin -3 :var "AA") (postpone))
%|- QED

  skolet2 : LEMMA % skoletin
    (LET d=3*x+2 IN LET (a,b,c)=(d,x*x,LET e=x+1 IN e*e) IN a=b+c+d) OR
    (LET d=3*x+2 IN LET (a,b,c)=triple(d,x*x,LET e=x+1 in e*e) IN a=b+c+d)

%|- skolet2 : PROOF
%|- (then (skeep) (skoletin 1) (skoletin 2 :var "dd")
%|-  (skoletin 2 "e" :hide? t) (skoletin* 2) (skoletin 2) (postpone))
%|- QED

  redsko : LEMMA % redlet*, skoletin*
    -(LET a = (LET b = py in b+px) IN a*py) =     
    -(LET (c,a) = (1,LET b = px in b*px) IN a+px) IMPLIES
    LET a=px+py IN
    LET b=a*a IN
    a+b = px

%|- redsko : PROOF
%|- (then (skeep) (redlet* 1 :n 2) (skoletin* -1 :postfix "_2" :hide? t)
%|-  (reveal ("a_2:" "b_2:")) (postpone))
%|- QED

  skodef : FORMULA % skodef, skodef*
    (FORALL(a,b,c,d:real):
      b=x AND
      a=2+b AND
      d=x*x AND
      c=a+b IMPLIES
      a*b*c >= y) IMPLIES 
    (EXISTS (a,b,c:real): a = 2+x+y AND b=a AND x = 2*a AND c=2*x)

%|- skodef : PROOF
%|- (then (skeep) (skodef -1 "d") (skodef -2 :var "bb")
%|-  (skodef* -3 :hide? t) (reveal ("a:" "c:"))
%|-  (skodef* 1 :postfix "_2" :n 2) (skodef 1 :postfix "_3") (postpone))
%|- QED

  splash1 : FORMULA % splash, skoletin
    x /= 0 AND LET a = 1/x IN a*x = 2

%|- splash1 : PROOF
%|- (then (skeep)
%|-  (spread (splash 1) ((then (skoletin) (postpone)) (postpone))))
%|- QED

  splash2 : FORMULA % splash, skoletin
    (x /= 0 IMPLIES LET a = 1/x IN a*x = 2)
    IMPLIES
    x*x = 1

%|- splash2 : PROOF
%|- (then (skeep)
%|-  (spread (splash -) ((then (skoletin -) (postpone)) (postpone))))
%|- QED

  bothsidesneg : FORMULA % both-sides-f, neg-formula
  -x*-x + z < -w*-w + y AND
    x+y = z+w IMPLIES
    (-x-w*w < -w + x OR 2*z+w = x*x-w)

%|- bothsidesneg : PROOF
%|- (then (skeep) (both-sides-f -2 "sq") (neg-formula -1) (neg-formula 1)
%|-  (neg-formula 2) (postpone))
%|- QED

END extra_examples