%% examples.pvs
%% Interval package 
%% Release: Interval-4.0 (10/01/09)

examples : theory
begin

  x,y : var real
  X   : var Interval

  sqrt23 : lemma
    sqrt(2)+sqrt(3) < 3.15
  %|- sqrt23 : PROOF (numerical) QED

  sin6sqrt2 : lemma
    sin(6*pi/180)+sqrt(2) <= 2.11
  %|- sin6sqrt2 : PROOF (numerical) QED

  g:posreal=9.8        %[m/s^2]

  v:posreal=250*0.514  %[m/s]

  tr(phi:(Tan?)): real = g*tan(phi)/v

  tr_35 : lemma
    3*pi/180 <= tr(35*pi/180)
  %|- tr_35 :  PROOF (numerical :defs "tr") QED

  G(x|x < 1): real = 3*x/2 - ln(1-x)
  
  A_and_S : lemma
    let x = 0.5828 in
      G(x) > 0
  %|- A_and_S : PROOF (numerical :defs "G") QED 

  %% The proof-rule (instint) guesses the interval variables based on the
  %% antecedent, i.e., (instint) = (then (skeep) (numerical :vars ... ))

  sqrtx3 : lemma
    x ## [|0,2|] IMPLIES
    sqrt(x)+sqrt(3) < 315/100
  %|- sqrtx3 : PROOF (instint) QED

  test : lemma
    x ## [|0,1|]   and
    y ## [|10,20|] implies
    x*y <= y
  %|- test : PROOF (instint) QED

  %% The same example, different techniques

  fair : lemma
    x ## [|0,1|] implies
    x*(1-x) ## [|0,1|]
  %|- fair : PROOF (instint) QED

  better : lemma
    x ## [|0,1|] implies
    x*(1-x) ## [|0,9/32|]
  %|- better : PROOF
  %|-   (then (skeep) (numerical :vars ("x" 16)))
  %|- QED

  clever : lemma
     x ## [|0,1|] implies
     x*(1-x) ## [|0,1/4|]
  %|- clever : PROOF 
  %|- (then (skeep)
  %|-       (spread (case-replace "x*(1-x) = 1/4 - sq(1/2-x)")
  %|-               ((instint) (grind))))
  %|- QED

  F(X)  : MACRO Interval = X*(1-X)

  DF(X) : MACRO Interval = 1 - 2*X

  D2F(X): MACRO Interval = [| -2 |]

  ftaylor : LEMMA
    x ## [|0,1|] IMPLIES
    x*(1-x) ## Taylor2[[|0,1|]](F,DF,D2F)
  %|- ftaylor : PROOF (taylor) QED

  best : LEMMA
    x ## [|0,1|] IMPLIES
    x*(1-x) ## [|0,1/4|]
  %|- best : PROOF (instint :taylor "ftaylor") QED

  %% A few examples suggested by Behzad Akbarpour

  epsilon : MACRO real = 0.15

  ex1_ba : LEMMA
    x ## [|0,1|] IMPLIES
    exp(x) - epsilon <= 1 + x + sq(x)

  ex2_ba : LEMMA
    x ## [|0,1|] IMPLIES
    exp(x-x^2) - epsilon <= 1 + x

  ex3_ba : LEMMA
    x ## [|0,1|] IMPLIES
    x - x^2  - epsilon <= ln (1 + x)

  ex4_ba : LEMMA
    x ## [|0,0.9|] IMPLIES
    ln(1-x) - epsilon <= -x 

  ex5_ba : LEMMA
    x ## [|0,1/2|] IMPLIES
    -x - 2*sq(x) - epsilon <= ln(1 - x)

  ex6_ba : LEMMA
    x ## [|0,1|] IMPLIES
    abs(ln(1+x) - x) - epsilon <= sq(x)

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

  % Proof script for the lemmas above
  %|- ex*_ba : PROOF (then (skeep) (numerical :vars ("x" 10))) QED

  g(x)   : MACRO real = exp(x) - 1 - x - sq(x)

  G(X)   : MACRO Interval = Exp(X,5) - 1 - X - Sq(X)
  DG(X)  : MACRO Interval = Exp(X,5) - 1 - 2*X
  D2G(X) : MACRO Interval = Exp(X,5) - 2

  gtaylor : LEMMA
    x ## [|0,1|] IMPLIES
    g(x) ## Taylor2[[|0,1|]](G,DG,D2G)
  %|- gtaylor : PROOF (taylor) QED
	
  exba : LEMMA
    x ## [|0,1|] IMPLIES
    g(x) <= 0.2
  %|- exba : PROOF (instint :taylor "gtaylor") QED

end examples