%% 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
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
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.
|
