%% metit_examples.pvs metit_examples : theory BEGIN IMPORTING trig@atan, lnexp@ln_exp, interval_arith@interval x,y : var real simple : LEMMA FORALL(x:real): x*(1-x) <= 1/4 %|- simple : PROOF (metit) QED simple_abs : LEMMA FORALL (x:real,y:posreal): abs(x*y) <= 1 IMPLIES x*y <= abs(x)*y % The proof command (metit) also works. This example illustrates that % metit can be called with multiple formulas. %|- simple_abs : PROOF %|- (then (skeep :preds? t) (metit (-3 -4 1))) %|- QED v : VAR posreal phi : VAR real sqrtx3 : LEMMA x ## [|1,2|] IMPLIES sqrt(x)+sqrt(3) < pi + 0.01 %|- sqrtx3 : PROOF (metit) QED g : MACRO posreal = 9.8 % [m/s^2] tr_35 : LEMMA abs(phi) <= 35 AND v ## [| 200, 250 |] IMPLIES abs(180*g*tan(phi*pi/180)/(pi*v*0.514)) ## [|0.000, 3.825|] %|- tr_35 : PROOF (metit) QED V: MACRO posreal=250*0.514 %[m/s] tr(phi:(Tan?)): MACRO real = g*tan(phi)/V tr_35_le : LEMMA 3*pi/180 <= tr(35*pi/180) %|- tr_35_le : PROOF (metit) QED sqrt23 : LEMMA sqrt(2)+sqrt(3)-pi ## [|0.002, 0.007|] %|- sqrt23 : PROOF (metit) QED sin6sqrt2 : LEMMA sin(6*pi/180)+sqrt(2) ## [|1.517, 1.520|] %|- sin6sqrt2 : PROOF (metit) QED G(x|x < 1): MACRO real = 3*x/2 - ln(1-x) X : MACRO posreal = 0.5828 A_and_S : LEMMA G(X) > 0 %|- A_and_S : PROOF (metit) QED r(x) : MACRO real = x - (11184811/33554432) * x^3 - (13421773/67108864) * x^5 ex(x) : MACRO real = atan(x) - r(x) atan_implementation : LEMMA abs(x) <= 0.33 IMPLIES abs(ex(x)) <= 2^-9 %|- atan_implementation : PROOF (metit) QED % The following problem provided by Anthony Narkawicz comes from % the proof of the repulsive criteria in ACCoRD ajn : LEMMA FORALL(sx,sy,vx,vy,nvx,nvy,nwx,nwy,eps,pt,px:real) : px > 0 AND pt > 0 AND (eps = 1 OR eps = -1) AND nvx * sx + nvy * sy + nvx * nvx * pt + nvy * nvy * pt >= 0 AND sx * vx + sy * vy < 0 AND sx * vy * eps - sy * vx * eps <= 0 AND nvy * sx * eps - nvx * sy * eps < 0 AND nvx * vy * eps - nvy * vx * eps < 0 AND nvy * sx * eps - nvx * sy * eps <= 0 AND -1 * (nwx * sy * eps) - nvy * nwx * eps * pt + nwy * sx * eps + nvx * nwy * eps * pt < 0 AND nwx * sx + nwy * sy + nvx * nwx * pt + nvy * nwy * pt > nvx * sx + nvy * sy + nvx * nvx * pt + nvy * nvy * pt AND nwx * vy * eps - nwy * vx * eps < 0 IMPLIES -1 * (nvx * sy * eps * pt) - nwx * sy * eps * px + nvy * sx * eps * pt + nwy * sx * eps * px < 0 %|- ajn : PROOF %|- (metit) %|- QED % The following problems were suggested by Behzad Akbarpour epsilon : MACRO real = 0.1 ex1_ba : LEMMA x ## [|0,1|] IMPLIES x - x^2 - epsilon <= ln (1 + x) %|- ex1_ba : PROOF (metit) QED ex2_ba : LEMMA x ## [|0,0.9|] IMPLIES ln(1-x) - epsilon <= -x %|- ex2_ba : PROOF (metit) QED ex3_ba : LEMMA x ## [|0,1/2|] IMPLIES -x - 2*sq(x) - epsilon <= ln(1 - x) %|- ex3_ba : PROOF (metit) QED ex4_ba : LEMMA x ## [|0,1|] IMPLIES abs(ln(1+x) - x) - epsilon <= sq(x) %|- ex4_ba : PROOF (metit) QED ex5_ba : LEMMA x ## [|-1/2,0|] IMPLIES abs(ln(1+x) - x) - epsilon <= 2*sq(x) %|- ex5_ba : PROOF (metit) QED ex6_ba : LEMMA x ## [|0,1|] IMPLIES exp(x) - epsilon <= 1 + x + sq(x) %|- ex6_ba : PROOF (metit) QED ex7_ba : LEMMA x ## [|0,1|] IMPLIES exp(x-x^2) - epsilon <= 1 + x %|- ex7_ba : PROOF (metit) QED quadratic : LEMMA FORALL(a,b,c,t:real) : a > 0 AND a*sq(t) + b*t + c < 0 IMPLIES sq(b) > 4*a*c %|- quadratic : PROOF (metit) QED %% The following examples are taken from %% Formal verification of analog designs using MetiTarski %% William Denman, Behzad Akbarpour, Sofiene Tahar, Mohamed H. Zaki, and Lawrence C. Paulson, %% FMCAD 2009 Tunnel_3_IL : LEMMA x ## [| 0, 2.39*10^(-9) |] IMPLIES -0.0059 - 0.000016*exp(-2.55*10^8*x) + 0.031*exp(-5.49*10^7*x) <= 0.03 %|- Tunnel_3_IL : PROOF (metit) QED Tunnel_3_IL_LU : LEMMA x ## [| 0, 8.17*10^(-8) |] IMPLIES -0.0006427443996*exp(-2.559889987*(10^8*x)) - 0.07600397043 + 0.1443470449*exp(-4.211001275*(10^6*x)) ## [| 0, 0.08 |] %|- Tunnel_3_IL_LU : PROOF (metit) QED %% The following problem is taken from %% A. Ayad and C. Marche, Multi-prover verification of floating-point programs, %% 5th IJCAR 2010. Ayad_Marche : LEMMA FORALL (r:real) : abs(r) <= 1 IMPLIES abs(0.9890365552 + 1.130258690*r + 0.5540440796*r*r - exp(r)) <= (1-2^-16)*2^-4 %|- Ayad_Marche : PROOF (metit) QED END metit_examples