More lemmas on floats

5a715168 · MARCHE Claude · 5a01c422 · 5a715168 · 5a715168
Commit 5a715168 authored Jun 16, 2012 by MARCHE Claude
--- a/examples/programs/my_cosine/why3session.xml
+++ b/examples/programs/my_cosine/why3session.xml
 <?xml version="1.0" encoding="UTF-8"?>
+<<<<<<< HEAD
 <!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
+=======
+<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
+>>>>>>> More lemmas on floats
 <why3session
- name="examples/programs/my_cosine/why3session.xml">
+ name="programs/my_cosine/why3session.xml">
 <prover
  id="0"
  name="Coq"
-  version="8.3pl4"/>
+  version="8.3pl3"/>
 <prover
  id="1"
  name="Gappa"
@@ -16,16 +20,20 @@
  expanded="true">
  <theory
   name="WP M"
-   locfile="examples/programs/my_cosine/../my_cosine.mlw"
+   locfile="programs/my_cosine/../my_cosine.mlw"
   loclnum="1" loccnumb="7" loccnume="8"
   verified="true"
   expanded="true">
   <goal
    name="WP_parameter my_cosine"
-    locfile="examples/programs/my_cosine/../my_cosine.mlw"
+    locfile="programs/my_cosine/../my_cosine.mlw"
    loclnum="30" loccnumb="4" loccnume="13"
    expl="parameter my_cosine"
+<<<<<<< HEAD
    sum="43a387020a8494975293041bea91d995"
+=======
+    sum="e18349ec1631d3a17eea4de5481cd8cc"
+>>>>>>> More lemmas on floats
    proved="true"
    expanded="true"
    shape="ainfix &lt;=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FAainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FAainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
@@ -37,10 +45,14 @@
     expanded="true">
     <goal
      name="WP_parameter my_cosine.1"
-      locfile="examples/programs/my_cosine/../my_cosine.mlw"
+      locfile="programs/my_cosine/../my_cosine.mlw"
      loclnum="30" loccnumb="4" loccnume="13"
      expl="assertion"
+<<<<<<< HEAD
      sum="1847af31ffb0fc79bb3f99eb48677194"
+=======
+      sum="29cbc2fa0e49fc55e087329496e2da77"
+>>>>>>> More lemmas on floats
      proved="true"
      expanded="true"
      shape="ainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
@@ -53,15 +65,23 @@
       edited="my_cosine_M_WP_parameter_my_cosine_1.v"
       obsolete="false"
       archived="false">
+<<<<<<< HEAD
       <result status="valid" time="3.58"/>
+=======
+       <result status="valid" time="5.82"/>
+>>>>>>> More lemmas on floats
      </proof>
     </goal>
     <goal
      name="WP_parameter my_cosine.2"
-      locfile="examples/programs/my_cosine/../my_cosine.mlw"
+      locfile="programs/my_cosine/../my_cosine.mlw"
      loclnum="30" loccnumb="4" loccnume="13"
      expl="precondition"
+<<<<<<< HEAD
      sum="ed7fd59f8e3662b57ab5ff723e124166"
+=======
+      sum="d0aced220a37d7b4dddd73141f910e24"
+>>>>>>> More lemmas on floats
      proved="true"
      expanded="true"
      shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
@@ -78,10 +98,14 @@
     </goal>
     <goal
      name="WP_parameter my_cosine.3"
-      locfile="examples/programs/my_cosine/../my_cosine.mlw"
+      locfile="programs/my_cosine/../my_cosine.mlw"
      loclnum="30" loccnumb="4" loccnume="13"
      expl="precondition"
+<<<<<<< HEAD
      sum="01c28821422107c03234edd2f723d53e"
+=======
+      sum="02beb0cc288ba7cba469f3db5e3fd908"
+>>>>>>> More lemmas on floats
      proved="true"
      expanded="true"
      shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
@@ -98,10 +122,14 @@
     </goal>
     <goal
      name="WP_parameter my_cosine.4"
-      locfile="examples/programs/my_cosine/../my_cosine.mlw"
+      locfile="programs/my_cosine/../my_cosine.mlw"
      loclnum="30" loccnumb="4" loccnume="13"
      expl="precondition"
+<<<<<<< HEAD
      sum="d30950e1e41f800ca0172d07dda83ad4"
+=======
+      sum="60fab8199ea5cc9a793f777f2fdb559e"
+>>>>>>> More lemmas on floats
      proved="true"
      expanded="true"
      shape="ainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
@@ -113,15 +141,19 @@
       memlimit="0"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.00"/>
+       <result status="valid" time="0.01"/>
      </proof>
     </goal>
     <goal
      name="WP_parameter my_cosine.5"
-      locfile="examples/programs/my_cosine/../my_cosine.mlw"
+      locfile="programs/my_cosine/../my_cosine.mlw"
      loclnum="30" loccnumb="4" loccnume="13"
      expl="normal postcondition"
+<<<<<<< HEAD
      sum="2eafda4f7656e405bda4587b4c59ab3c"
+=======
+      sum="a0176bc5d22c4a84606639fb3a5ee329"
+>>>>>>> More lemmas on floats
      proved="true"
      expanded="true"
      shape="ainfix &lt;=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FIainfix &lt;=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FIainfix &lt;=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix &lt;=.aabsavalueV0c0x1.p-5F">
@@ -133,7 +165,7 @@
       memlimit="0"
       obsolete="false"
       archived="false">
-       <result status="valid" time="0.00"/>
+       <result status="valid" time="0.01"/>
      </proof>
     </goal>
    </transf>

--- a/theories/floating_point.why
+++ b/theories/floating_point.why

 (** {1 Formalization of Floating-Point Arithmetic}

-This formalization follows the {h <a href="http://ieeexplore.ieee.org/servlet/opac?punumber=4610933">IEEE-754 standard</a>}.
+This formalization follows the {h <a
+href="http://ieeexplore.ieee.org/servlet/opac?punumber=4610933">IEEE-754
+standard</a>}.

 *)

@@ -10,7 +12,7 @@ This formalization follows the {h <a href="http://ieeexplore.ieee.org/servlet/op
 theory Rounding

  type mode = NearestTiesToEven | ToZero | Up | Down | NearestTiesToAway
-    (** nearest ties to even, to zero, upward, downward, nearest ties to away *)
+  (** nearest ties to even, to zero, upward, downward, nearest ties to away *)

 end

@@ -18,8 +20,8 @@ end

 Special values are +infinity, -infinity, NaN, +0, -0.  These are
 handled as described in {h <a
-href="http://www.lri.fr/~marche/ayad10ijcar.pdf">[Ayad, Marché,
-IJCAR, 2010]</a>}.
+href="http://www.lri.fr/~marche/ayad10ijcar.pdf">[Ayad, Marché, IJCAR,
+2010]</a>}.

 *)

@@ -35,12 +37,45 @@ theory SpecialValues
    | Neg_case: forall x:real. x < 0.0 -> same_sign_real Neg x
    | Pos_case: forall x:real. x > 0.0 -> same_sign_real Pos x

+(* useful ???
+
+lemma sign_not_pos_neg : forall x:t.
+      sign(x) <> Pos -> sign(x) = Neg
+lemma sign_not_neg_pos : forall x:t.
+      sign(x) <> Neg -> sign(x) = Pos
+
+lemma sign_not_pos_neg : forall x:double.
+      sign(x) <> Pos -> sign(x) = Neg
+lemma sign_not_neg_pos : forall x:double.
+      sign(x) <> Neg -> sign(x) = Pos
+*)
+
+lemma same_sign_real_zero1 :
+  forall b:sign. not same_sign_real b 0.0
+
+lemma same_sign_real_zero2 :
+  forall x:real.
+    same_sign_real Neg x /\ same_sign_real Pos x -> false
+
+lemma same_sign_real_zero3 :
+  forall b:sign, x:real. same_sign_real b x -> x <> 0.0
+
+lemma same_sign_real_correct2 :
+  forall b:sign, x:real.
+    same_sign_real b x -> (x < 0.0 <-> b = Neg)
+
+lemma same_sign_real_correct3 :
+  forall b:sign, x:real.
+    same_sign_real b x -> (x > 0.0 <-> b = Pos)
+
+
 end

 (** {2 Generic theory of floats}

 The theory is parametrized by the real constant [max] which denotes
-the maximal representable number, and the integer constant
+the maximal representable number, the real constant [min] which denotes
+the minimal number whose rounding is not null, and the integer constant
 [max_representable_integer] which is the maximal integer [n] such that
 every integer between [0] and [n] are representable.

@@ -250,6 +285,8 @@ theory GenFloatFull

  function sign t  : sign

+  predicate same_sign_real (x:t) (y:real) =
+    SpecialValues.same_sign_real (sign x) y
  predicate same_sign (x:t) (y:t)  = sign x = sign y
  predicate diff_sign (x:t) (y:t)  = sign x <> sign y

@@ -266,6 +303,41 @@ theory GenFloatFull
  predicate is_gen_zero_plus (x:t) = is_gen_zero x /\ sign x = Pos
  predicate is_gen_zero_minus (x:t) = is_gen_zero x /\ sign x = Neg

+  (** {3 Useful lemmas on sign} *)
+
+  (* non-zero finite gen_float has the same sign as its float_value *)
+  lemma finite_sign :
+    forall x:t.
+      class x = Finite /\ value x <> 0.0 -> same_sign_real x (value x)
+
+  lemma finite_sign_pos1:
+    forall x:t.
+      class x = Finite /\ value x > 0.0 -> sign x = Pos
+
+  lemma finite_sign_pos2:
+    forall x:t.
+      class x = Finite /\ value x <> 0.0 /\ sign x = Pos -> value x > 0.0
+
+  lemma finite_sign_neg1:
+    forall x:t. class x = Finite /\ value x < 0.0 -> sign x = Neg
+
+  lemma finite_sign_neg2:
+    forall x:t.
+      class x = Finite /\ value x <> 0.0 /\ sign x = Neg -> value x < 0.0
+
+  lemma diff_sign_trans:
+    forall x y z:t. diff_sign x y /\ diff_sign y z -> same_sign x z
+
+  lemma diff_sign_product:
+    forall x y:t.
+      class x = Finite /\ class y = Finite /\ value x * value y < 0.0
+      -> diff_sign x y
+
+  lemma same_sign_product:
+    forall x y:t.
+      class x = Finite /\ class y = Finite /\ same_sign x y
+      -> value x * value y >= 0.0
+
  (** {3 overflow} *)

  (** This predicate tells what is the result of a rounding in case
@@ -282,6 +354,56 @@ theory GenFloatFull
    end


+  (** rounding in logic *)
+  lemma round1 :
+    forall m:mode, x:real.
+      no_overflow m x ->
+        is_finite (round_logic m x) /\ value(round_logic m x) = round m x
+
+  lemma round2 :
+    forall m:mode, x:real.
+      not no_overflow m x ->
+        same_sign_real (round_logic m x) x /\
+        overflow_value m (round_logic m x)
+
+  lemma round3 : forall m:mode, x:real. exact (round_logic m x) = x
+
+  lemma round4 : forall m:mode, x:real. model (round_logic m x) = x
+
+  (** rounding of zero *)
+
+  lemma round_of_zero : forall m:mode. is_gen_zero (round_logic m 0.0)
+
+  use import real.Abs
+
+  lemma round_logic_le : forall m:mode, x:real.
+    is_finite (round_logic m x) -> abs (value (round_logic m x)) <= max
+
+  lemma round_no_overflow : forall m:mode, x:real.
+    abs x <= max ->
+    is_finite (round_logic m x) /\ value (round_logic m x) = round m x
+
+  constant min : real
+
+  lemma positive_constant : forall m:mode, x:real.
+    min <= x <= max ->
+    is_finite (round_logic m x) /\ value (round_logic m x) > 0.0 /\
+    sign (round_logic m x) = Pos
+
+  lemma negative_constant : forall m:mode, x:real.
+    - max <= x <= - min ->
+    is_finite (round_logic m x) /\ value (round_logic m x) < 0.0 /\
+    sign (round_logic m x) = Neg
+
+  (** lemmas on gen_zero *)
+
+  lemma is_gen_zero_comp1 : forall x y:t.
+    is_gen_zero x /\ value x = value y /\ is_finite y -> is_gen_zero y
+
+  lemma is_gen_zero_comp2 : forall x y:t.
+    is_finite x /\ not (is_gen_zero x) /\ value x = value y
+    -> not (is_gen_zero y)
+
 end

 theory GenFloatSpecFull
@@ -418,6 +540,10 @@ theory SingleFull

  use export SingleFormat

+  constant max_single : real = 0x1.FFFFFEp127
+  constant min_single : real = 0x1p-149
+  constant max_int : int = 16777216 (* 2^24 *)
+
  clone export GenFloatSpecFull with
    type t = single,
    constant max = max_single,
@@ -431,6 +557,10 @@ theory DoubleFull

  use export DoubleFormat

+  constant max_double : real = 0x1.FFFFFFFFFFFFFp1023
+  constant min_double : real = 0x1p-1074
+  constant max_int : int = 9007199254740992 (* 2^53 *)
+
  clone export GenFloatSpecFull with
    type t = double,
    constant max = max_double,
@@ -556,4 +686,4 @@ theory DoubleMultiRounding
    constant eps_normalized = eps_normalized_double,
    constant eta_normalized = eta_normalized_double

-end
\ No newline at end of file
+end