%% Examples of strategies in Extrategies 6.0 %% Cesar Munoz %% http://shemesh.larc.nasa.gov/fm/pvs/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