Impressum extra_examples.pvs Sprache: 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

quality94%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.