%% interval_examples.pvs
%% 
%% These examples deal with arbitrary real-valued expressions, for that reason the theory 
%% imports strategies instead of strategies4Q.
%%  

interval_examples : theory
BEGIN

  IMPORTING interval_arith@strategies

  x,y : var real

  %%%% Examples of numerical

  sqrt23 : LEMMA
    sqrt(2)+sqrt(3)-pi ## [|0.002, 0.007|]
%% The expression (! 1 1) refers to formula 1, 1st term: sqrt(2)+sqrt(3)-pi
%|- sqrt23 : PROOF
%|- (numerical (! 1 1) :verbose? t)
%|- QED

  sin6sqrt2 : LEMMA
    sin(6*pi/180)+sqrt(2) ## [|1.517, 1.520|]
%% The expression (! 1 1) refers to formula 1, 1st term: sin(6*pi/180)+sqrt(2)
%|- sin6sqrt2 : PROOF (numerical (! 1 1)) QED

  %%%% Examples of interval

  sqrtx3 : LEMMA
    x ## [|1,2|] IMPLIES
    sqrt(x)+sqrt(3) <  pi + 0.01
%|- sqrtx3 : PROOF (interval) QED

  g : posreal = 9.8 % Gravitational acceleration [m/s^2]
  
  v     : VAR posreal % Ground speed [knots]
  phi   : VAR {deg:real| Tan?(pi*deg/180)} % Bank angle [deg]

  %% Turn rate [deg/sec]
  tr(v,phi) : MACRO real =
    LET PI = pi IN
      ((180*g)/(PI*v*0.514) )*tan((PI*phi)/180)

  tr_250_35 : LEMMA
    LET tr = tr(250,35) IN
      3 <= tr AND tr <= 3.1
%|- tr_250_35 : PROOF (interval) QED

  tr_200_250_abs_35 : LEMMA
    abs(phi) <= 35 AND 
    v   ## [| 200, 250 |] IMPLIES
    abs(tr(v,phi)) <= 3.825
%|- tr_200_250_abs_35 : PROOF
%|- (then (skeep) (interval))
%|- QED

  G(x|x < 1): MACRO real = 3*x/2 - ln(1-x)

  X : posreal = 0.5828
  
  A_and_S : LEMMA
    G(X) > 0
%|- A_and_S : PROOF
%|- (interval)
%|- QED

  common_point: LEMMA EXISTS (x,y,theta,r:real): 
    abs(x) <= 1 AND abs(y) <= 1 AND abs(theta) <= 3 AND r ## [|0,1|] AND
    x^2 + y^2 < 3-2*sqrt(2)+0.1 AND (x-(1+r*cos(theta)))^2 + (y-(1+r*sin(theta)))^2 < 0.1
%|- common_point : PROOF (interval :verbose? t) 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 (interval) QED

% The following problems were suggested by Behzad Akbarpour

  epsilon : real = 0.1

  ex1_ba : LEMMA
    x ## [|0,1|] IMPLIES
    x - x^2  - epsilon <= ln (1 + x)
%|- ex1_ba : PROOF (interval) QED

  ex2_ba : LEMMA
    x ## [|0,0.9|] IMPLIES
    ln(1-x) - epsilon <= -x 
%|- ex2_ba : PROOF (interval) QED

  ex3_ba : LEMMA
    x ## [|0,1/2|] IMPLIES
    -x - 2*sq(x) - epsilon <= ln(1 - x)
%|- ex3_ba : PROOF (interval) QED

  ex4_ba : LEMMA
    x ## [|0,1|] IMPLIES
    abs(ln(1+x) - x) - epsilon <= sq(x)
%|- ex4_ba : PROOF (interval) QED

  ex5_ba : LEMMA
    x ## [|-1/2,0|] IMPLIES
    abs(ln(1+x) - x) - epsilon <= 2*sq(x)
%|- ex5_ba : PROOF (interval) QED

  ex6_ba : LEMMA
    x ## [|0,1|] IMPLIES
    exp(x) - epsilon <= 1 + x + sq(x)
%|- ex6_ba : PROOF (interval) QED

  ex7_ba : LEMMA
    x ## [|0,1|] IMPLIES
    exp(x-x^2) - epsilon <= 1 + x
%|- ex7_ba : PROOF (interval) 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
    FORALL (x:real | x ## [| 0, 2.39*10^(-9) |]):
    -0.0059 - 0.000016*exp(-2.55*10^8*x) + 0.031*exp(-5.49*10^7*x) <= 0.03
%|- Tunnel_3_IL : PROOF (interval) QED

  Tunnel_3_IL_LU : LEMMA
    FORALL (x:real | x ## [| 0, 8.17*10^(-8) |]):
    -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 (interval) QED

END interval_examples