floats: Restored adequate post-condition for lt, gt

examples/bts/12475/why3session.xml

@@ -34,7 +34,7 @@
     name="toto"
     locfile="bts/12475/../12475.why"
     loclnum="6" loccnumb="7" loccnume="11"
-    sum="9277e7312956b5e244f4586258a899ba"
+    sum="1528698e7ee515779e096133af624d2f"
     proved="true"
     expanded="true"
     shape="ainfix <V0ainfix +aroundaUpV0c1.F">
@@ -44,7 +44,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.03"/>
+     <result status="valid" time="0.02"/>
     </proof>
     <proof
      prover="1"
@@ -52,7 +52,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.03"/>
     </proof>
     <proof
      prover="0"
@@ -60,7 +60,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.01"/>
     </proof>
     <proof
      prover="2"

examples/check-builtin/floats/why3session.xml

@@ -32,7 +32,7 @@
     name="Round_single_01"
     locfile="check-builtin/floats/../floats.why"
     loclnum="11" loccnumb="7" loccnume="22"
-    sum="8d5596f1dc7557ed743fea14f397c3bb"
+    sum="3242b4e9102c2fc37a9a7dd6cfd10efa"
     proved="true"
     expanded="true"
     shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
@@ -49,7 +49,7 @@
     name="Round_double_01"
     locfile="check-builtin/floats/../floats.why"
     loclnum="14" loccnumb="7" loccnume="22"
-    sum="32107838e0e998b61d3694c4f5f0009f"
+    sum="95147a77cfc066399edef8befff58feb"
     proved="true"
     expanded="true"
     shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
@@ -66,7 +66,7 @@
     name="Test00"
     locfile="check-builtin/floats/../floats.why"
     loclnum="17" loccnumb="8" loccnume="14"
-    sum="cd281225d4d500e7379dc6138cd16330"
+    sum="f04ce085ad30e1fb1b6594cd78d977bd"
     proved="true"
     expanded="true"
     shape="ainfix <=aprefix -c3.0V0Iainfix <=aabsV0c2.0F">
@@ -76,7 +76,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.06"/>
     </proof>
     <proof
      prover="1"
@@ -92,7 +92,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="2"
@@ -107,7 +107,7 @@
     name="Test01"
     locfile="check-builtin/floats/../floats.why"
     loclnum="19" loccnumb="8" loccnume="14"
-    sum="86dad2fc6873ddc0073bc0115e52c724"
+    sum="512a97ac8833620d3c1fe4338f5109c6"
     proved="true"
     expanded="true"
     shape="ainfix &lt;=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix &lt;=avalueV0c2.0Aainfix &lt;=aprefix -c2.0avalueV0F">
@@ -124,7 +124,7 @@
     name="Test02"
     locfile="check-builtin/floats/../floats.why"
     loclnum="25" loccnumb="8" loccnume="14"
-    sum="ac5095b33417c8bd32759846e5fb4881"
+    sum="303330d34dd6e52d73fcdcc7f34319f3"
     proved="true"
     expanded="true"
     shape="ainfix &lt;=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix &lt;=aabsavalueV0c2.0F">
@@ -141,7 +141,7 @@
     name="Test03"
     locfile="check-builtin/floats/../floats.why"
     loclnum="32" loccnumb="8" loccnume="14"
-    sum="41a813fab58ad82dd738ec1203c67376"
+    sum="2d6c2d43256f71efff7bd2e63cb3541e"
     proved="true"
     expanded="true"
     shape="ainfix &lt;=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix &lt;=aabsavalueV0c2.0F">

examples/my_cosine/why3session.xml

@@ -28,7 +28,7 @@
     name="MethodError"
     locfile="./my_cosine/../my_cosine.why"
     loclnum="13" loccnumb="6" loccnume="17"
-    sum="1e22c4edd1067353283e8362ea67fdf0"
+    sum="2467a67484295345557f0076ed412561"
     proved="true"
     expanded="true"
     shape="ainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix <=aabsV0c0x1.p-5F">
@@ -39,14 +39,14 @@
      edited="my_cosine_CosineSingle_MethodError_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="6.37"/>
+     <result status="valid" time="6.07"/>
     </proof>
    </goal>
    <goal
     name="TotalErrorFullyExpanded"
     locfile="./my_cosine/../my_cosine.why"
     loclnum="20" loccnumb="6" loccnume="29"
-    sum="aadcb6c321ae62976144a46205babd78"
+    sum="16c317808f261ff9cc5b16296167cd8b"
     proved="true"
     expanded="true"
     shape="ainfix &lt;=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix &lt;=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix &lt;=aabsavalueV0c0x1.p-5F">
@@ -63,7 +63,7 @@
     name="TotalErrorExpanded"
     locfile="./my_cosine/../my_cosine.why"
     loclnum="31" loccnumb="6" loccnume="24"
-    sum="d021d9680b1e11e1aa2c83fdd3c36d71"
+    sum="fe418525d8a2ed9a3cc54a44066dff60"
     proved="true"
     expanded="true"
     shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix &lt;=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix &lt;=aabsavalueV0c0x1.p-5F">
@@ -80,7 +80,7 @@
     name="TotalError"
     locfile="./my_cosine/../my_cosine.why"
     loclnum="51" loccnumb="6" loccnume="16"
-    sum="0d725bd8aa56715a6b6f3b5bc0299292"
+    sum="967dbbbd6b72c88306fbf58d0d697b15"
     proved="true"
     expanded="true"
     shape="Lacos_singleV0ainfix &lt;=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix &lt;=aabsavalueV0c0x1.p-5F">
@@ -90,7 +90,7 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="4.53"/>
+     <result status="valid" time="4.56"/>
     </proof>
    </goal>
   </theory>

examples/programs/my_cosine/why3session.xml

@@ -25,7 +25,7 @@
     locfile="programs/my_cosine/../my_cosine.mlw"
     loclnum="30" loccnumb="4" loccnume="13"
     expl="parameter my_cosine"
-    sum="613554e5135277438089d8ff16551aa7"
+    sum="e18349ec1631d3a17eea4de5481cd8cc"
     proved="true"
     expanded="true"
     shape="ainfix <=.aabsainfix -.avalueV5acosavalueV0c0x1.p-23Iainfix =avalueV5aroundaNearestTiesToEvenainfix -.avalueV1avalueV4FAainfix <=aabsaroundaNearestTiesToEvenainfix -.avalueV1avalueV4amax_singleIainfix =avalueV4aroundaNearestTiesToEvenainfix *.avalueV2avalueV3FAainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV2avalueV3amax_singleIainfix =avalueV3c0.5FIainfix =avalueV2aroundaNearestTiesToEvenainfix *.avalueV0avalueV0FAainfix <=aabsaroundaNearestTiesToEvenainfix *.avalueV0avalueV0amax_singleIainfix =avalueV1c1.0FAainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.aabsavalueV0c0x1.p-5F">
@@ -40,7 +40,7 @@
       locfile="programs/my_cosine/../my_cosine.mlw"
       loclnum="30" loccnumb="4" loccnume="13"
       expl="assertion"
-      sum="11c4f7c81d63da1453654b5cd6ff0639"
+      sum="29cbc2fa0e49fc55e087329496e2da77"
       proved="true"
       expanded="true"
       shape="ainfix <=.aabsainfix -.ainfix -.c1.0ainfix *.ainfix *.avalueV0avalueV0c0.5acosavalueV0c0x1.p-24Iainfix <=.aabsavalueV0c0x1.p-5F">
@@ -53,7 +53,7 @@
        edited="my_cosine_M_WP_parameter_my_cosine_1.v"
        obsolete="false"
        archived="false">
-       <result status="valid" time="5.96"/>
+       <result status="valid" time="5.90"/>
       </proof>
      </goal>
      <goal
@@ -61,7 +61,7 @@
       locfile="programs/my_cosine/../my_cosine.mlw"
       loclnum="30" loccnumb="4" loccnume="13"
       expl="precondition"
-      sum="12de20c84831e31ca300cde9629492ff"
+      sum="d0aced220a37d7b4dddd73141f910e24"
       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">
@@ -81,7 +81,7 @@
       locfile="programs/my_cosine/../my_cosine.mlw"
       loclnum="30" loccnumb="4" loccnume="13"
       expl="precondition"
-      sum="8347c5ae52a7c23d8b25cc34f50df355"
+      sum="02beb0cc288ba7cba469f3db5e3fd908"
       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">
@@ -101,7 +101,7 @@
       locfile="programs/my_cosine/../my_cosine.mlw"
       loclnum="30" loccnumb="4" loccnume="13"
       expl="precondition"
-      sum="084afefdd4400a264223024aa7592dfd"
+      sum="60fab8199ea5cc9a793f777f2fdb559e"
       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">
@@ -121,7 +121,7 @@
       locfile="programs/my_cosine/../my_cosine.mlw"
       loclnum="30" loccnumb="4" loccnume="13"
       expl="normal postcondition"
-      sum="d7405fa3fbaf989f038a1aa69e408d76"
+      sum="a0176bc5d22c4a84606639fb3a5ee329"
       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">

examples/tests-provers/gappa/why3session.xml

@@ -20,7 +20,7 @@
     name="Round_single_01"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="11" loccnumb="8" loccnume="23"
-    sum="8d5596f1dc7557ed743fea14f397c3bb"
+    sum="3242b4e9102c2fc37a9a7dd6cfd10efa"
     proved="true"
     expanded="false"
     shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.99999ap-4">
@@ -37,7 +37,7 @@
     name="Round_double_01"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="14" loccnumb="8" loccnume="23"
-    sum="0364393cc059ccdb3de99dd40d7cdf06"
+    sum="d39bb272fc8d9297bec1df1e1fb1106a"
     proved="true"
     expanded="false"
     shape="ainfix =aroundaNearestTiesToEvenc0.1c0x1.999999999999ap-4">
@@ -54,7 +54,7 @@
     name="Test00"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="17" loccnumb="9" loccnume="15"
-    sum="6bb1cae38eba2a75a66592be762b428b"
+    sum="9ebac93d6a57654f3787929bdc703aaf"
     proved="true"
     expanded="false"
     shape="ainfix <=aprefix -c3.0V0Iainfix <=aabsV0c2.0F">
@@ -71,7 +71,7 @@
     name="Test01"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="19" loccnumb="9" loccnume="15"
-    sum="5e3913f891b4a3baa2e8da1305e17f47"
+    sum="bf409087a884fe327065f5dbc2eb0d4d"
     proved="true"
     expanded="false"
     shape="ainfix <=aabsainfix -ainfix *avalueV0avalueV0aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix <=avalueV0c2.0Aainfix <=aprefix -c2.0avalueV0F">
@@ -88,7 +88,7 @@
     name="Test02"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="25" loccnumb="9" loccnume="15"
-    sum="c99b9e0886cc50bbd89f03d161e8da45"
+    sum="8feed07428304f0920d7f41124c883b3"
     proved="true"
     expanded="false"
     shape="ainfix <=aabsainfix -ainfix *avalueV1avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0c0x1.p-52Iainfix =V1V0Iainfix <=aabsavalueV0c2.0F">
@@ -98,14 +98,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="Test03"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="32" loccnumb="9" loccnume="15"
-    sum="d60812e0448110f0c19061c777138b40"
+    sum="0da33f7c98ccd09c0d1e66fd78e72212"
     proved="true"
     expanded="false"
     shape="ainfix &lt;=asqrtainfix *ainfix -avalueV2ainfix *avalueV0avalueV0ainfix -avalueV1ainfix *avalueV0avalueV0c0x1.p-52Iainfix =V2V1Iainfix =avalueV1aroundaNearestTiesToEvenainfix *avalueV0avalueV0Iainfix &lt;=aabsavalueV0c2.0F">
@@ -129,7 +129,7 @@
     name="Test1"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="53" loccnumb="8" loccnume="13"
-    sum="780586c907131af3a8db711ff1bc314f"
+    sum="33c71394fca93d3d410fb722fcb970b5"
     proved="true"
     expanded="false"
     shape="ainfix &lt;=aabsainfix -avalueaac0.1c0x1.p-53Iainfix =aaarIainfix =avalueararoundaNearestTiesToEvenc0.1">
@@ -146,7 +146,7 @@
     name="Test2"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="58" loccnumb="8" loccnume="13"
-    sum="015ec5f2fb0c5fd25bd7b466a94304d7"
+    sum="65602af0f639b8cea8843b1fc07542b7"
     proved="true"
     expanded="false"
     shape="ainfix &lt;=aabsainfix -avalueafc0c0.1c0x1.p-53Iainfix =afc0arIainfix =avalueararoundaNearestTiesToEvenc0.1">
@@ -163,7 +163,7 @@
     name="Test3"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="63" loccnumb="8" loccnume="13"
-    sum="50182d48e211aae23d117c1ad6c2b06b"
+    sum="1764bc962492b20b5ca636eea0acb2b5"
     proved="true"
     expanded="false"
     shape="ainfix &lt;=aabsainfix -avalueagc0c1c0.1c0x1.p-53Iainfix =agc0c1arIainfix =avalueararoundaNearestTiesToEvenc0.1">
@@ -187,7 +187,7 @@
     name="G1"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="89" loccnumb="7" loccnume="9"
-    sum="28d9a8aaf749577fce6cee6e8d4b3192"
+    sum="f0532ec1f07ee528e1c4ad329cbd2426"
     proved="true"
     expanded="true"
     shape="ainfix &lt;=ainfix -avaluearesultainfix *avalueaq1avalueaq2c0x1.p-52">
@@ -197,14 +197,14 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="G2"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="91" loccnumb="7" loccnume="9"
-    sum="698acd79137ddd7dd8d1505a38c1e983"
+    sum="76fd08ebf94a56233e552dcc7ba63305"
     proved="true"
     expanded="true"
     shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
@@ -214,14 +214,14 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.01"/>
+     <result status="valid" time="0.00"/>
     </proof>
    </goal>
    <goal
     name="G3"
     locfile="tests-provers/gappa/../gappa.why"
     loclnum="94" loccnumb="7" loccnume="9"
-    sum="971eea20fcf064886923dae3a1ab58bf"
+    sum="147725714d029b09fa91b96558079798"
     proved="true"
     expanded="true"
     shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
@@ -231,7 +231,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.00"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
   </theory>

lib/coq/floating_point/Double.v

@@ -118,4 +118,50 @@ Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
 now apply Round_up_neg.
 Qed.
 
+(* Why3 assumption *)
+Definition add_post(m:floating_point.Rounding.mode) (x:double) (y:double)
+  (res:double): Prop := ((value res) = (round m
+  ((value x) + (value y))%R)) /\
+  (((exact res) = ((exact x) + (exact y))%R) /\
+  ((model res) = ((model x) + (model y))%R)).
+
+(* Why3 assumption *)
+Definition sub_post(m:floating_point.Rounding.mode) (x:double) (y:double)
+  (res:double): Prop := ((value res) = (round m
+  ((value x) - (value y))%R)) /\
+  (((exact res) = ((exact x) - (exact y))%R) /\
+  ((model res) = ((model x) - (model y))%R)).
+
+(* Why3 assumption *)
+Definition mul_post(m:floating_point.Rounding.mode) (x:double) (y:double)
+  (res:double): Prop := ((value res) = (round m
+  ((value x) * (value y))%R)) /\
+  (((exact res) = ((exact x) * (exact y))%R) /\
+  ((model res) = ((model x) * (model y))%R)).
+
+(* Why3 assumption *)
+Definition div_post(m:floating_point.Rounding.mode) (x:double) (y:double)
+  (res:double): Prop := ((value res) = (round m
+  (Rdiv (value x) (value y))%R)) /\
+  (((exact res) = (Rdiv (exact x) (exact y))%R) /\
+  ((model res) = (Rdiv (model x) (model y))%R)).
+
+(* Why3 assumption *)
+Definition neg_post(x:double) (res:double): Prop :=
+  ((value res) = (-(value x))%R) /\ (((exact res) = (-(exact x))%R) /\
+  ((model res) = (-(model x))%R)).
+
+(* Why3 assumption *)
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+(* Why3 assumption *)
+Definition lt(x:double) (y:double): Prop := ((value x) < (value y))%R.
+
+(* Why3 assumption *)
+Definition gt(x:double) (y:double): Prop := ((value y) < (value x))%R.
+
 

lib/coq/floating_point/Single.v

@@ -126,4 +126,50 @@ Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
 now apply Round_up_neg.
 Qed.
 
+(* Why3 assumption *)
+Definition add_post(m:floating_point.Rounding.mode) (x:single) (y:single)
+  (res:single): Prop := ((value res) = (round m
+  ((value x) + (value y))%R)) /\
+  (((exact res) = ((exact x) + (exact y))%R) /\
+  ((model res) = ((model x) + (model y))%R)).
+
+(* Why3 assumption *)
+Definition sub_post(m:floating_point.Rounding.mode) (x:single) (y:single)
+  (res:single): Prop := ((value res) = (round m
+  ((value x) - (value y))%R)) /\
+  (((exact res) = ((exact x) - (exact y))%R) /\
+  ((model res) = ((model x) - (model y))%R)).
+
+(* Why3 assumption *)
+Definition mul_post(m:floating_point.Rounding.mode) (x:single) (y:single)
+  (res:single): Prop := ((value res) = (round m
+  ((value x) * (value y))%R)) /\
+  (((exact res) = ((exact x) * (exact y))%R) /\
+  ((model res) = ((model x) * (model y))%R)).
+
+(* Why3 assumption *)
+Definition div_post(m:floating_point.Rounding.mode) (x:single) (y:single)
+  (res:single): Prop := ((value res) = (round m
+  (Rdiv (value x) (value y))%R)) /\
+  (((exact res) = (Rdiv (exact x) (exact y))%R) /\
+  ((model res) = (Rdiv (model x) (model y))%R)).
+
+(* Why3 assumption *)
+Definition neg_post(x:single) (res:single): Prop :=
+  ((value res) = (-(value x))%R) /\ (((exact res) = (-(exact x))%R) /\
+  ((model res) = (-(model x))%R)).
+
+(* Why3 assumption *)
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+(* Why3 assumption *)
+Definition lt(x:single) (y:single): Prop := ((value x) < (value y))%R.
+
+(* Why3 assumption *)
+Definition gt(x:single) (y:single): Prop := ((value y) < (value x))%R.
+
 

theories/floating_point.why

@@ -142,8 +142,10 @@ theory GenFloatSpecStrict
 
   use import bool.Bool
 
-  predicate lt_post (x:t) (y:t) (r:bool) =
-    if r = True then value x < value y else value x >= value y
+  predicate lt (x:t) (y:t) = value x < value y
+
+  predicate gt (x:t) (y:t) = value x > value y
+
 
 end
 
@@ -244,46 +246,6 @@ theory GenFloatFull
     | (NearestTiesToAway | NearestTiesToEven), _ -> is_infinite x
     end
 
-  (** {3 binary operations} *)
-
-
-  (** {3 Comparisons} *)
-
-  predicate le_full (x:t) (y:t) =
-    (is_finite x /\ is_finite y /\ value x <= value y)
-    \/ (is_minus_infinity x /\ is_not_NaN y)
-    \/ (is_not_NaN x /\ is_plus_infinity y)
-
-  predicate lt_full (x:t) (y:t) =
-    (is_finite x /\ is_finite y /\ value x < value y)
-    \/ (is_minus_infinity x /\ is_not_NaN y /\ not (is_minus_infinity y))
-    \/ (is_not_NaN x /\ not (is_plus_infinity x) /\ is_plus_infinity y)
-
-  predicate ge_full (x:t) (y:t) = le_full y x
-
-  predicate gt_full (x:t) (y:t) = lt_full y x
-
-  predicate eq_full (x:t) (y:t) =
-    is_not_NaN x /\ is_not_NaN y /\
-      ((is_finite x /\ is_finite y /\ value x = value y) \/
-       (is_infinite x /\ is_infinite y /\ same_sign x y))
-
-  predicate ne_full (x:t) (y:t) = not (eq_full x y)
-
-  lemma le_lt_full_trans:
-    forall x y z:t. le_full x y /\ lt_full y z -> lt_full x z
-
-  lemma lt_le_full_trans:
-    forall x y z:t. lt_full x y /\ le_full y z -> lt_full x z
-
-  lemma le_ge_full_asym:
-    forall x y:t. le_full x y /\ ge_full x y -> eq_full x y
-
-  lemma not_lt_ge_full: forall x y:t.
-    not (lt_full x y) /\ is_not_NaN x /\ is_not_NaN y -> ge_full x y
-
-  lemma not_gt_le_full: forall x y:t.
-    not (gt_full x y) /\ is_not_NaN x /\ is_not_NaN y -> le_full x y
 
 end
 
@@ -376,10 +338,41 @@ theory GenFloatSpecFull
 
   (** {3 Comparisons} *)
 
-  use import bool.Bool
+  predicate le (x:t) (y:t) =
+    (is_finite x /\ is_finite y /\ value x <= value y)
+    \/ (is_minus_infinity x /\ is_not_NaN y)
+    \/ (is_not_NaN x /\ is_plus_infinity y)
+
+  predicate lt (x:t) (y:t) =
+    (is_finite x /\ is_finite y /\ value x < value y)
+    \/ (is_minus_infinity x /\ is_not_NaN y /\ not (is_minus_infinity y))
+    \/ (is_not_NaN x /\ not (is_plus_infinity x) /\ is_plus_infinity y)
+
+  predicate ge (x:t) (y:t) = le y x
+
+  predicate gt (x:t) (y:t) = lt y x
+
+  predicate eq (x:t) (y:t) =
+    is_not_NaN x /\ is_not_NaN y /\
+      ((is_finite x /\ is_finite y /\ value x = value y) \/
+       (is_infinite x /\ is_infinite y /\ same_sign x y))
+
+  predicate ne (x:t) (y:t) = not (eq x y)
+
+  lemma le_lt_trans:
+    forall x y z:t. le x y /\ lt y z -> lt x z
+
+  lemma lt_le_trans:
+    forall x y z:t. lt x y /\ le y z -> lt x z
+
+  lemma le_ge_asym:
+    forall x y:t. le x y /\ ge x y -> eq x y
+
+  lemma not_lt_ge: forall x y:t.
+    not (lt x y) /\ is_not_NaN x /\ is_not_NaN y -> ge x y
 
-  predicate lt_post (x:t) (y:t) (r:bool) =
-    if r = True then lt_full x y else not (lt_full x y)
+  lemma not_gt_le: forall x y:t.
+    not (gt x y) /\ is_not_NaN x /\ is_not_NaN y -> le x y
 
 end