%% 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