Quelle  examples4Q.pvs

%% examples4Q.pvs
%% 
%% These examples only deal with rational expressions, for that reason the theory 
%% just imports strategies4Q. 
%%  

examples4Q : theory
BEGIN

  IMPORTING strategies4Q

  x,y : var real

  %%%% Examples of numerical

  zero_to_one_quarter : LEMMA
    x ## [|0,1|] IMPLIES
    x*(1-x) ## [|0.0000, 0.2501|]
%% The expression (! 1 1) refers to formula 1, 1st term, i.e., x*(1-x)
%|- zero_to_one_quarter : PROOF
%|- (then (skeep) (numerical (! 1 1) :precision 4 :maxdepth 20 :verbose? t))
%|- QED

  x0,x1,x2,x3,x4,x5,x6,x7 : VAR real

  Heart(x0,x1,x2,x3,x4,x5,x6,x7): MACRO real = 
    -x0*x5^3+3*x0*x5*x6^2-x2*x6^3+3*x2*x6*x5^2-x1*x4^3+3*x1*x4*x7^2-x3*x7^3+3*x3*x7*x4^2-0.9563453

  hdp_mm: LEMMA 
    -0.1 <= x0 AND x0 <= 0.4 AND 
     0.4 <= x1  AND x1 <= 1 AND 
    -0.7 <= x2 AND x2 <= -0.4 AND 
    -0.7 <= x3 AND x3 <= 0.4 AND 
     0.1 <= x4  AND x4 <= 0.2 AND
    -0.1 <= x5 AND x5 <= 0.2 AND 
    -0.3 <= x6 AND x6 <= 1.1 AND 
    -1.1 <= x7 AND x7 <= -0.3 IMPLIES 
     Heart(x0,x1,x2,x3,x4,x5,x6,x7) ## [|-1.852, 1.518|]

%% The expression (! 1 1) refers to formula 1, 1st term, i.e., polynomial Heart
%|- hdp_mm : PROOF
%|- (then (skeep) (numerical (! 1 1) :verbose? t))
%|- QED

  %%%% Examples of interval

  hdp_minmax: LEMMA 
    -0.1 <= x0 AND x0 <= 0.4 AND 
     0.4 <= x1  AND x1 <= 1 AND 
    -0.7 <= x2 AND x2 <= -0.4 AND 
    -0.7 <= x3 AND x3 <= 0.4 AND 
     0.1 <= x4  AND x4 <= 0.2 AND
    -0.1 <= x5 AND x5 <= 0.2 AND 
    -0.3 <= x6 AND x6 <= 1.1 AND 
    -1.1 <= x7 AND x7 <= -0.3 IMPLIES 
     Heart(x0,x1,x2,x3,x4,x5,x6,x7) ## [| -1.76, 1.46 |]

%|- hdp_minmax : PROOF
%|- (then (skeep) (interval))
%|- QED

  common_point: LEMMA 
    EXISTS (x,y,z:real): abs(x) <= 10 AND abs(y) <= 10 AND z ## [|0,1/2|] AND 
      LET x2 = x^2,
          y2 = y^2 IN
        x2-2*x+1+y2-2*y+1<1 AND x2 + y2 < 3-2*y+0.01

%|- common_point : PROOF (interval :verbose? t) QED

   Eps : posreal = 0.0001

   simple_ite : LEMMA
     FORALL (x:real | x ## [| 0, 10 |]) :
       IF x <= 1 THEN sq(x) <= x+Eps
       ELSE sq(x) >= x-Eps
       ENDIF

%|- simple_ite : PROOF
%|- (interval)
%|- QED


END examples4Q