ErrorValidation.hl 73.3 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
(**
Heiko Becker's avatar
Heiko Becker committed
2 3 4 5 6 7
   This file contains the coq implementation of the error bound validator as well
   as its soundness proof. The function validErrorbound is the Error bound
   validator from the certificate checking process. Under the assumption that a
   valid range arithmetic result has been computed, it can validate error bounds
   encoded in the analysis result. The validator is used in the file
   CertificateChecker.hl to build the complete checker.
Heiko Becker's avatar
Heiko Becker committed
8
 **)
9 10 11
needs "Infra/ExpressionAbbrevs.hl";;
needs "IntervalValidation.hl";;
needs "ErrorBounds.hl";;
12

Heiko Becker's avatar
Heiko Becker committed
13
(** Error bound validator **)
Heiko Becker's avatar
Heiko Becker committed
14 15
let validErrorbound = new_recursive_definition exp_REC
    `(validErrorbound (Const n) (absenv:analysisResult) =
16
      let (intv, err) = absenv (Const n) in
17 18 19
        ((&0 <= err) /\
        (maxAbsFun intv * machineEpsilon) <= err)) /\
  (validErrorbound (Param v) (absenv:analysisResult) =
20
      let (intv, err) = absenv (Param v) in
21 22 23 24
        ((&0 <= err) /\
           (maxAbsFun intv * machineEpsilon) <= err )) /\
  (validErrorbound (Var v) (absenv:analysisResult) = F) /\
  (validErrorbound (Binop b e1 e2) (absenv:analysisResult) =
25 26 27
      let (intv, err) = absenv (Binop b e1 e2) in
      let (ive1, err1) = absenv e1 in
      let (ive2, err2) = absenv e2 in
Heiko Becker's avatar
Heiko Becker committed
28 29
      let errIve1 = widenInterval ive1 err1 in
      let errIve2 = widenInterval ive2 err2 in
30 31
      let upperBoundE1 = maxAbsFun ive1 in
      let upperBoundE2 = maxAbsFun ive2 in
Heiko Becker's avatar
Heiko Becker committed
32
        (validErrorbound e1 absenv /\ validErrorbound e2 absenv /\ (&0 <= err) /\
Heiko Becker's avatar
Heiko Becker committed
33 34 35 36 37 38 39 40 41
           (if (b = Plus)
            then (err1 + err2 + (maxAbsFun (addInterval errIve1 errIve2)) * machineEpsilon) <= err
            else
              if (b = Sub)
              then (err1 + err2 + (maxAbsFun (subtractInterval errIve1 errIve2)) * machineEpsilon) <= err
              else
                if b = Mult
                then ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbsFun (multInterval errIve1 errIve2)) * machineEpsilon) <= err
                else F)))`;;
42

Heiko Becker's avatar
Heiko Becker committed
43 44 45 46 47
(**
    Since errors are intervals with 0 as center, we encode them as single values.
    This lemma enables us to deduce from each run of the validator the invariant
    that when it succeeds, the errors must be positive.
**)
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
let err_always_positive = prove (
  `!(e:(real)exp) (absenv:analysisResult) (iv:interval) (err:error).
    validErrorbound e absenv = T /\
    absenv e = (iv,err) ==>
    &0 <= err`,
  SIMP_TAC[] THEN intros "!e absenv iv err; validbound_e absenv_e"
     (* FIXME: Why can't I use SPEC `e:(real)exp` (cases "exp") here? *)
     THEN SUBGOAL_TAC "cases_e" `(?a:num. (e:(real)exp) = Var a) \/ (?a:num. e = Param a) \/ (?n:real. e = Const n) \/ (?(b:binop) (e1:(real)exp) (e2:(real)exp). e = Binop b e1 e2)` [MESON_TAC[cases "exp"]]
     THEN destruct "cases_e" "e_var | e_param | e_const | e_binop"
     THENL [
       destruct "e_var" "@v. e_var"
         THEN rewrite_asm "e_var" "validbound_e"
         THEN rewrite validErrorbound "validbound_e"
         THEN falsity "validbound_e";
       destruct "e_param" "@v. e_param"
         THEN rewrite_asm "e_param" "validbound_e"
         THEN rewrite_asm "e_param" "absenv_e"
         THEN rewrite validErrorbound "validbound_e"
         THEN rewrite_asm "absenv_e" "validbound_e"
         THEN simplify "validbound_e"
         THEN destruct "validbound_e" "goal _"
         THEN auto;
       destruct "e_const" "@n. e_const"
         THEN rewrite_asm "e_const" "validbound_e"
         THEN rewrite_asm "e_const" "absenv_e"
         THEN rewrite validErrorbound "validbound_e"
         THEN rewrite_asm "absenv_e" "validbound_e"
         THEN simplify "validbound_e"
         THEN destruct "validbound_e" "goal _"
         THEN auto;
       destruct "e_binop" "@b. @e1. @e2. e_binop"
         THEN rewrite_asm "e_binop" "validbound_e"
         THEN rewrite_asm "e_binop" "absenv_e"
         THEN rewrite validErrorbound "validbound_e"
         THEN rewrite_asm "absenv_e" "validbound_e"
         THEN SUBGOAL_TAC "absenv_e1_def" `?(iv1:interval) (err1:error). (absenv:analysisResult) e1 = (iv1,err1)` [MESON_TAC[cases "prod"]]
         THEN destruct "absenv_e1_def" "@iv1. @err1. absenv_e1"
         THEN rewrite_asm "absenv_e1" "validbound_e"
         THEN SUBGOAL_TAC "absenv_e2_def" `?(iv2:interval) (err2:error). (absenv:analysisResult) e2 = (iv2,err2)` [MESON_TAC[cases "prod"]]
         THEN destruct "absenv_e2_def" "@iv2. @err2. absenv_e2"
         THEN rewrite_asm "absenv_e2" "validbound_e"
         THEN simplify "validbound_e"
Heiko Becker's avatar
Heiko Becker committed
90
         THEN destruct "validbound_e" "_ _ goal _"
91
         THEN auto]);;
92 93 94 95 96 97 98 99 100 101

let validErrorboundCorrectConstant = prove (
  `!(cenv:env_ty) (absenv:analysisResult) (n:real) (nR:real) (nF:real) (e:real) (nlo:real) (nhi:real) (P:precond).
    eval_exp (&0) cenv (Const n) nR /\
    eval_exp machineEpsilon cenv (Const n) nF /\
    validErrorbound (Const n) absenv /\
    validIntervalbounds (Const n) absenv P /\
    absenv (Const n) = ((nlo,nhi),e) ==>
    (abs (nR - nF)) <= e`,
  intros "!cenv absenv n nR nF e nlo nhi P; eval_real eval_float error_valid intv_valid absenv_const"
102 103 104 105 106 107 108 109
    THEN rewrite validErrorbound "error_valid"
    THEN pose_spec const_inv [`&0:real`; `cenv:env_ty`; `n:real`; `nR:real`] "eval_real" "eval_inv"
    THEN destruct "eval_inv" "@d. perturb_nR abs_0"
    THEN ASM_SIMP_TAC[perturb_0_val]
    THEN pose_spec const_inv [`machineEpsilon:real`; `cenv:env_ty`; `n:real`; `nF:real`] "eval_float" "eval_inv"
    THEN destruct "eval_inv" "@d2. perturb_nF abs_leq_meps"
    THEN ASM_SIMP_TAC[perturb]
    THEN SIMP_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
110 111 112 113 114 115 116
     THEN mp REAL_LE_TRANS
     THEN EXISTS_TAC `abs (n:real) * (machineEpsilon:real)` THEN split
     THENL [
       mp REAL_LE_LMUL
         THEN split THENL [ SIMP_TAC[REAL_ABS_POS]; auto];
       rewrite validIntervalbounds "intv_valid"
         THEN rewrite_asm "absenv_const" "intv_valid"
117 118 119
         THEN rewrite isSupersetInterval "intv_valid"
         THEN rewrite IVlo "intv_valid"
         THEN rewrite IVhi "intv_valid"
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
         THEN rewrite SND "intv_valid"
         THEN destruct "intv_valid" "lo_le_n n_le_hi"
         THEN rewrite_asm "absenv_const" "error_valid" THEN simplify "error_valid"
         THEN mp REAL_LE_TRANS
         THEN EXISTS_TAC `maxAbsFun(nlo:real,nhi) * machineEpsilon`
         THEN split
         THENL [
           mp REAL_LE_RMUL
             THEN split
             THENL [
               SIMP_TAC[maxAbsFun]
                 THEN mp iv_le_maxAbs THEN split THEN auto;
               SIMP_TAC[mEps_geq_zero]
             ];
         auto]]);;

136 137 138 139 140 141 142 143 144
let validErrorboundCorrectParam = prove (
  `!(cenv:env_ty) (absenv:analysisResult) (v:num) (nR:real) (nF:real) (e:real) (P:precond) (plo:real) (phi:real).
    precondValidForExec P cenv /\
    eval_exp (&0) cenv (Param v) nR /\
    eval_exp machineEpsilon cenv (Param v) nF /\
    validErrorbound (Param v) absenv /\
    validIntervalbounds (Param v) absenv P /\
    absenv (Param v) = ((plo,phi),e) ==>
    (abs (nR - nF)) <= e`,
145 146 147 148
  intros "!cenv absenv v nR nF e P plo phi; cenv_approx_p eval_real eval_float error_valid intv_valid absenv_param"
    THEN pose_proof ivbounds_approximatesPrecond_sound "absenv_approx_p"
    [`(Param v):(real)exp`;`absenv:analysisResult`;`P:precond`]
    ["intv_valid"]
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189
    THEN rewrite validErrorbound "error_valid"
    THEN pose_spec param_inv [`&0:real`; `cenv:env_ty`; `v:num`; `nR:real`] "eval_real" "eval_inv"
    THEN destruct "eval_inv" "@d. perturb_nR abs_0"
    THEN ASM_SIMP_TAC[perturb_0_val]
    THEN pose_spec param_inv [`machineEpsilon:real`; `cenv:env_ty`; `v:num`; `nF:real`] "eval_float" "eval_inv"
    THEN destruct "eval_inv" "@d2. perturb_nF abs_leq_meps"
    THEN ASM_SIMP_TAC[perturb]
    THEN SIMP_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
    THEN rewrite precondValidForExec "cenv_approx_p"
    THEN rewrite precondValidForExecFun "cenv_approx_p"
    THEN lspecialize "cenv_approx_p" [`v:num`]
    THEN lspecialize "absenv_approx_p" [`v:num`]
    THEN SUBGOAL_TAC "p_v_def" `?ivlo ivhi. (P:precond) (v:num) = (ivlo,ivhi)` [MESON_TAC [cases "prod"]]
        THEN destruct "p_v_def" "@ivlo. @ivhi. p_v_def"
        THEN rewrite isSupersetInterval "absenv_approx_p"
        THEN rewrite_asm "p_v_def" "absenv_approx_p"
        THEN rewrite_asm "absenv_param" "absenv_approx_p"
        THEN rewrite_asm "p_v_def" "cenv_approx_p"
        THEN simplify "cenv_approx_p"
        THEN SUBGOAL_TAC "v_in_fVs" `MEM (v:num) ((freeVars:(real)exp->(num)list) (Param v))` [SIMP_TAC[freeVars; MEM]]
        THEN mp_spec "absenv_approx_p" "v_in_fVs"
        THEN rewrite IVlo "absenv_approx_p"
        THEN rewrite IVhi "absenv_approx_p"
        THEN rewrite FST "absenv_approx_p"
        THEN rewrite SND "absenv_approx_p"
        THEN destruct "absenv_approx_p" "approx_lo approx_hi"
        THEN rewrite_asm "absenv_param" "error_valid"
        THEN simplify "error_valid"
        THEN mp REAL_LE_TRANS
        THEN EXISTS_TAC `maxAbsFun (plo,phi) * machineEpsilon`
        THEN split
        THENL [
          mp REAL_LE_MUL2 THEN split
            THENL [
              SIMP_TAC[REAL_ABS_POS];
              split THENL [
                SIMP_TAC[maxAbsFun] THEN mp iv_le_maxAbs THEN split THEN mp REAL_LE_TRANS
                  THENL [
                    EXISTS_TAC `ivlo:real` THEN split THEN auto;
                    EXISTS_TAC `ivhi:real` THEN split THEN auto
                  ];
190
                split THENL [
191 192
                  SIMP_TAC[REAL_ABS_POS];
                  auto
193
                ]
194 195 196 197
              ]
            ];
          auto]
);;
Heiko Becker's avatar
Heiko Becker committed
198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216

let validErrorboundCorrectAddition = prove (
  `!(cenv:env_ty) (absenv:analysisResult) (e1:(real)exp) (e2:(real)exp) nR nR1
    nR2 nF (nF1:real) (nF2:real) (e:error) err1 err2 alo ahi e1lo e1hi e2lo e2hi (P:precond).
    precondValidForExec P cenv /\
    eval_exp (&0) cenv e1 nR1 /\
    eval_exp (&0) cenv e2 nR2 /\
    eval_exp (&0) cenv (Binop Plus e1 e2) nR /\
    eval_exp machineEpsilon cenv e1 nF1 /\
    eval_exp machineEpsilon cenv e2 nF2 /\
    eval_exp machineEpsilon (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (Binop Plus (Var 1) (Var 2)) nF /\
    validErrorbound (Binop Plus e1 e2) absenv /\
    validIntervalbounds (Binop Plus e1 e2) absenv P /\
    absenv e1 = ((e1lo,e1hi),err1) /\
    absenv e2 = ((e2lo, e2hi),err2) /\
    absenv (Binop Plus e1 e2) = ((alo,ahi),e) /\
    (abs (nR1 - nF1) <= err1) /\
    (abs (nR2 - nF2) <= err2) ==>
    (abs (nR - nF) <= e)`,
217 218
  SIMP_TAC[freeVars; MEM; MEM_APPEND]
    THEN intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1hi e2lo e2hi P;
219 220 221 222
     p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded"
    THEN pose_proof ivbounds_approximatesPrecond_sound "env_approx_p"
    [`(Binop Plus e1 e2):(real)exp`;`absenv:analysisResult`;`P:precond`]
    ["valid_intv"]
Heiko Becker's avatar
Heiko Becker committed
223 224 225 226 227 228 229 230 231 232 233 234 235 236
    THEN pose add_abs_err_bounded [`e1:(real)exp`; `nR1:real`; `nF1:real`; `e2:(real)exp`; `nR2:real`; `nF2:real`; `nR:real`; `nF:real`; `cenv:env_ty`; `err1:real`; `err2:real`] "add_bounded"
    THEN mp REAL_LE_TRANS
    THEN EXISTS_TAC `(err1:real) + (err2:real) + abs ((nF1:real) + (nF2:real)) * machineEpsilon`
    THEN split
    THENL [
      mp_asm "add_bounded" THEN clear["add_bounded"] THEN auto;
      clear ["add_bounded"]
        THEN rewrite validErrorbound "valid_error"
        THEN rewrite_asm "absenv_add" "valid_error"
        THEN simplify "valid_error"
        THEN rewrite_asm "absenv_e1" "valid_error"
        THEN rewrite_asm "absenv_e2" "valid_error"
        THEN rewrite validIntervalbounds "valid_intv"
        THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
237
        THEN simplify "valid_error"
Heiko Becker's avatar
Heiko Becker committed
238
        THEN destruct "valid_error" "valid_err1 valid_err2 e_pos valid_err"
Heiko Becker's avatar
Heiko Becker committed
239
        THEN mp REAL_LE_TRANS
Heiko Becker's avatar
Heiko Becker committed
240
        THEN EXISTS_TAC `err1 + err2 + (maxAbsFun (addInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2))) * machineEpsilon`
Heiko Becker's avatar
Heiko Becker committed
241 242 243 244 245
        THEN split
        THENL [
          mp REAL_LE_LADD_IMP
            THEN mp REAL_LE_LADD_IMP
            THEN mp REAL_LE_RMUL
Heiko Becker's avatar
Heiko Becker committed
246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
            THEN pose_proof validIntervalbounds_sound "validbounds_e1"
            [`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
            ["p_valid"; "valid_e1"; "e1_real"]
            THEN rewrite_asm "absenv_e1" "validbounds_e1"
            THEN rewrite FST "validbounds_e1"
            THEN rewrite FST "validbounds_e1"
            THEN destruct "validbounds_e1" "valid_lo_e1 valid_hi_e1"
            THEN pose_proof distance_gives_iv "errIve1"
            [`nR1:real`;`nF1:real`;`err1:real`;`e1lo:real`;`e1hi:real`]
            ["valid_lo_e1"; "valid_hi_e1"; "err1_bounded"]
            THEN pose_proof validIntervalbounds_sound "validbounds_e2"
            [`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
            ["p_valid"; "valid_e2"; "e2_real"]
            THEN rewrite_asm "absenv_e2" "validbounds_e2"
            THEN rewrite FST "validbounds_e2"
            THEN rewrite FST "validbounds_e2"
            THEN destruct "validbounds_e2" "valid_lo_e2 valid_hi_e2"
            THEN pose_proof distance_gives_iv "errIve2"
            [`nR2:real`;`nF2:real`;`err2:real`;`e2lo:real`;`e2hi:real`]
            ["valid_lo_e2"; "valid_hi_e2"; "err2_bounded"]
            THEN pose_proof interval_add_valid "add_valid"
            [`(widenInterval (e1lo,e1hi) err1)`;`widenInterval (e2lo,e2hi) err2`] []
            THEN rewrite validIntervalAdd "add_valid"
            THEN spec "add_valid" [`nF1:real`;`nF2:real`]
            THEN mp_ispecl "add_valid" ["errIve1"; "errIve2"]
Heiko Becker's avatar
Heiko Becker committed
271 272
            THEN split
            THENL [
Heiko Becker's avatar
Heiko Becker committed
273 274 275 276 277
              SUBGOAL_TAC "simp_iv" `?ivlo ivhi. addInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2) = (ivlo, ivhi)` [MESON_TAC [cases "prod"]]
                THEN destruct "simp_iv" "@ivlo. @ivhi. simp_iv"
                THEN ASM_SIMP_TAC[]
                THEN rewrite_asm "simp_iv" "add_valid"
                THEN mp contained_leq_maxAbs THEN auto;
Heiko Becker's avatar
Heiko Becker committed
278
              SIMP_TAC[mEps_geq_zero]
Heiko Becker's avatar
Heiko Becker committed
279 280
            ]
          ;
281 282
          auto]]);;

Heiko Becker's avatar
Heiko Becker committed
283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
 let validErrorboundCorrectSubtraction = prove (
   `!(cenv:env_ty) (absenv:analysisResult) (e1:(real)exp) (e2:(real)exp) nR nR1
     nR2 nF (nF1:real) (nF2:real) (e:error) err1 err2 alo ahi e1lo e1hi e2lo e2hi (P:precond).
     precondValidForExec P cenv /\
     eval_exp (&0) cenv e1 nR1 /\
     eval_exp (&0) cenv e2 nR2 /\
     eval_exp (&0) cenv (Binop Sub e1 e2) nR /\
     eval_exp machineEpsilon cenv e1 nF1 /\
     eval_exp machineEpsilon cenv e2 nF2 /\
     eval_exp machineEpsilon (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (Binop Sub (Var 1) (Var 2)) nF /\
     validErrorbound (Binop Sub e1 e2) absenv /\
     validIntervalbounds (Binop Sub e1 e2) absenv P /\
     absenv e1 = ((e1lo,e1hi),err1) /\
     absenv e2 = ((e2lo, e2hi),err2) /\
     absenv (Binop Sub e1 e2) = ((alo,ahi),e) /\
     (abs (nR1 - nF1) <= err1) /\
     (abs (nR2 - nF2) <= err2) ==>
     (abs (nR - nF) <= e)`,
301 302
   SIMP_TAC[freeVars; MEM; MEM_APPEND]
     THEN intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1hi e2lo e2hi P;
303 304 305 306
     p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_sub err1_bounded err2_bounded"
     THEN pose_proof ivbounds_approximatesPrecond_sound "env_approx_p"
    [`(Binop Sub e1 e2):(real)exp`;`absenv:analysisResult`;`P:precond`]
    ["valid_intv"]
Heiko Becker's avatar
Heiko Becker committed
307
     THEN pose sub_abs_err_bounded [`e1:(real)exp`; `nR1:real`; `nF1:real`; `e2:(real)exp`; `nR2:real`; `nF2:real`; `nR:real`; `nF:real`; `cenv:env_ty`; `err1:real`; `err2:real`] "sub_bounded"
308
     THEN mp REAL_LE_TRANS
Heiko Becker's avatar
Heiko Becker committed
309
     THEN EXISTS_TAC `(err1:real) + (err2:real) + (abs ((nF1:real) - nF2:real)) * machineEpsilon`
310 311
     THEN split
     THENL [
Heiko Becker's avatar
Heiko Becker committed
312 313
       mp_asm "sub_bounded" THEN clear["sub_bounded"] THEN auto;
       clear ["sub_bounded"]
314
         THEN rewrite validErrorbound "valid_error"
Heiko Becker's avatar
Heiko Becker committed
315
         THEN rewrite_asm "absenv_sub" "valid_error"
316 317 318
         THEN simplify "valid_error"
         THEN rewrite_asm "absenv_e1" "valid_error"
         THEN rewrite_asm "absenv_e2" "valid_error"
Heiko Becker's avatar
Heiko Becker committed
319 320
         THEN rewrite validIntervalbounds "valid_intv"
         THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
321
         THEN simplify "valid_error"
322
         THEN mp REAL_LE_TRANS
Heiko Becker's avatar
Heiko Becker committed
323
         THEN EXISTS_TAC `err1 + err2 + (maxAbsFun (subtractInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2))) * machineEpsilon`
324 325 326 327 328
         THEN split
         THENL [
           mp REAL_LE_LADD_IMP
             THEN mp REAL_LE_LADD_IMP
             THEN mp REAL_LE_RMUL
Heiko Becker's avatar
Heiko Becker committed
329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
             THEN pose_proof validIntervalbounds_sound "validbounds_e1"
            [`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
            ["p_valid"; "valid_e1"; "e1_real"]
            THEN rewrite_asm "absenv_e1" "validbounds_e1"
            THEN rewrite FST "validbounds_e1"
            THEN rewrite FST "validbounds_e1"
            THEN destruct "validbounds_e1" "valid_lo_e1 valid_hi_e1"
            THEN pose_proof distance_gives_iv "errIve1"
            [`nR1:real`;`nF1:real`;`err1:real`;`e1lo:real`;`e1hi:real`]
            ["valid_lo_e1"; "valid_hi_e1"; "err1_bounded"]
            THEN pose_proof validIntervalbounds_sound "validbounds_e2"
            [`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
            ["p_valid"; "valid_e2"; "e2_real"]
            THEN rewrite_asm "absenv_e2" "validbounds_e2"
            THEN rewrite FST "validbounds_e2"
            THEN rewrite FST "validbounds_e2"
            THEN destruct "validbounds_e2" "valid_lo_e2 valid_hi_e2"
            THEN pose_proof distance_gives_iv "errIve2"
            [`nR2:real`;`nF2:real`;`err2:real`;`e2lo:real`;`e2hi:real`]
            ["valid_lo_e2"; "valid_hi_e2"; "err2_bounded"]
            THEN pose_proof interval_subtraction_valid "sub_valid"
            [`(widenInterval (e1lo,e1hi) err1)`;`widenInterval (e2lo,e2hi) err2`] []
            THEN rewrite validIntervalSub "sub_valid"
            THEN spec "sub_valid" [`nF1:real`;`nF2:real`]
             THEN mp_ispecl "sub_valid" ["errIve1"; "errIve2"]
            THEN split
            THENL [
              SUBGOAL_TAC "simp_iv" `?ivlo ivhi. subtractInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2) = (ivlo, ivhi)` [MESON_TAC [cases "prod"]]
                THEN destruct "simp_iv" "@ivlo. @ivhi. simp_iv"
                THEN ASM_SIMP_TAC[]
                THEN rewrite_asm "simp_iv" "sub_valid"
                THEN mp contained_leq_maxAbs THEN auto;
              SIMP_TAC[mEps_geq_zero]
            ]
           ;
           destruct "valid_error" "_ _ _ valid_error"
             THEN REMOVE_THEN "valid_error"
             (fun th -> LABEL_TAC "valid_error" (SIMP_RULE[distinctness "binop"] (CONV_RULE COND_ELIM_CONV th)))
             THEN auto]]);;
368

Heiko Becker's avatar
Heiko Becker committed
369 370
let validErrorboundCorrectMultiplication = prove (
  `!(cenv:env_ty) (absenv:analysisResult) (e1:(real)exp) (e2:(real)exp) nR nR1
Heiko Becker's avatar
Heiko Becker committed
371 372 373 374 375 376 377 378 379 380 381 382 383 384 385
     nR2 nF (nF1:real) (nF2:real) (e:error) err1 err2 alo ahi e1lo e1hi e2lo e2hi (P:precond).
     precondValidForExec P cenv /\
     eval_exp (&0) cenv e1 nR1 /\
     eval_exp (&0) cenv e2 nR2 /\
     eval_exp (&0) cenv (Binop Mult e1 e2) nR /\
     eval_exp machineEpsilon cenv e1 nF1 /\
     eval_exp machineEpsilon cenv e2 nF2 /\
     eval_exp machineEpsilon (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (Binop Mult (Var 1) (Var 2)) nF /\
     validErrorbound (Binop Mult e1 e2) absenv /\
     validIntervalbounds (Binop Mult e1 e2) absenv P /\
     absenv e1 = ((e1lo,e1hi),err1) /\
     absenv e2 = ((e2lo, e2hi),err2) /\
     absenv (Binop Mult e1 e2) = ((alo,ahi),e) /\
     (abs (nR1 - nF1) <= err1) /\
     (abs (nR2 - nF2) <= err2) ==>
386
     (abs (nR - nF) <= e)`,
Heiko Becker's avatar
Heiko Becker committed
387
  SIMP_TAC[freeVars; MEM; MEM_APPEND]
388
     THEN intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1hi e2lo e2hi P;
389 390 391 392
     p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_mult err1_bounded err2_bounded"
     THEN pose_proof ivbounds_approximatesPrecond_sound "env_approx_p"
     [`(Binop Mult e1 e2):(real)exp`;`absenv:analysisResult`;`P:precond`]
     ["valid_intv"]
393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415
     THEN pose mul_abs_err_bounded [`e1:(real)exp`; `nR1:real`; `nF1:real`; `e2:(real)exp`; `nR2:real`; `nF2:real`; `nR:real`; `nF:real`; `cenv:env_ty`; `err1:real`; `err2:real`] "mult_bounded"
     THEN mp REAL_LE_TRANS
     THEN EXISTS_TAC `abs (nR1 * nR2 - nF1 * nF2) + abs (nF1 * nF2) * machineEpsilon`
     THEN split
     THENL [
       mp_asm "mult_bounded" THEN auto;
       clear ["mult_bounded"]
         THEN rewrite validErrorbound "valid_error"
         THEN rewrite_asm "absenv_mult" "valid_error"
         THEN simplify "valid_error"
         THEN rewrite_asm "absenv_e1" "valid_error"
         THEN rewrite_asm "absenv_e2" "valid_error"
         THEN rewrite validIntervalbounds "valid_intv"
         THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
         THEN simplify "valid_error"
         THEN destruct "valid_error" "valid_err_e1 valid_err_e2 err_geq_0 valid_error"
         THEN pose_proof err_always_positive "err1_pos" [`e1:(real)exp`; `absenv:analysisResult`; `(e1lo,e1hi):interval`; `err1:error`] ["valid_err_e1"; "absenv_e1"]
         THEN pose_proof err_always_positive "err2_pos" [`e2:(real)exp`; `absenv:analysisResult`; `(e2lo,e2hi):interval`; `err2:error`] ["valid_err_e2"; "absenv_e2"]
         THEN clear["valid_err_e1"; "valid_err_e2"]
         THEN mp REAL_LE_TRANS
         THEN EXISTS_TAC `(maxAbsFun ((e1lo:real),(e1hi:real)) * (err2:real) +
                             maxAbsFun ((e2lo:real),(e2hi:real)) * (err1:real) +
                             (err1:real) * (err2:real)) +
Heiko Becker's avatar
Heiko Becker committed
416
         maxAbsFun (multInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2)) *
417
         machineEpsilon`
Heiko Becker's avatar
Heiko Becker committed
418 419
         THEN pose_proof validIntervalbounds_sound "validbounds_e1" [`e1:(real)exp`; `absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `nR1:real`] ["p_valid"; "valid_e1"; "e1_real"]
         THEN pose_proof validIntervalbounds_sound "validbounds_e2" [`e2:(real)exp`; `absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `nR2:real`] ["p_valid"; "valid_e2"; "e2_real"]
420 421
         THEN split
         THENL [
Heiko Becker's avatar
Heiko Becker committed
422
           mp REAL_LE_ADD2
423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
             THEN split
             THENL[
               rewrite_asm "absenv_e1" "validbounds_e1"
                 THEN rewrite FST "validbounds_e1"
                 THEN rewrite FST "validbounds_e1"
                 THEN rewrite_asm "absenv_e2" "validbounds_e2"
                 THEN rewrite FST "validbounds_e2"
                 THEN rewrite FST "validbounds_e2"
                 (* Before doing case distinction, prove bounds that will be used many times: *)
                 THEN SUBGOAL_TAC "upperBound_nR1"
                 `(nR1:real) <= maxAbsFun(e1lo,e1hi)`
                 [mp contained_leq_maxAbs_val THEN SIMP_TAC[contained; IVlo; IVhi] THEN auto]
                 THEN SUBGOAL_TAC "upperBound_nR2"
                 `(nR2:real) <= maxAbsFun(e2lo,e2hi)`
                 [mp contained_leq_maxAbs_val THEN SIMP_TAC[contained; IVlo; IVhi] THEN auto]
                 THEN SUBGOAL_TAC "upperBound_opp_nR1"
                 `-- (nR1:real) <= maxAbsFun(e1lo,e1hi)`
                 [mp contained_leq_maxAbs_neg_val THEN SIMP_TAC[contained; IVlo; IVhi] THEN auto]
                 THEN SUBGOAL_TAC "upperBound_opp_nR2"
                 `-- (nR2:real) <= maxAbsFun(e2lo,e2hi)`
                 [mp contained_leq_maxAbs_neg_val THEN SIMP_TAC[contained; IVlo; IVhi] THEN auto]
                 THEN SUBGOAL_TAC "bound_nR1"
                 ` nR1 * (err2:real) <= maxAbsFun (e1lo, e1hi) * err2`
                 [mp REAL_LE_RMUL THEN auto]
                 THEN SUBGOAL_TAC "bound_neg_nR1"
                 ` -- nR1 * (err2:real) <= maxAbsFun (e1lo, e1hi) * err2`
                 [mp REAL_LE_RMUL THEN auto]
                 THEN SUBGOAL_TAC "bound_nR2"
                 ` nR2 * (err1:real) <= maxAbsFun (e2lo, e2hi) * err1`
                 [mp REAL_LE_RMUL THEN auto]
                 THEN SUBGOAL_TAC "bound_neg_nR2"
                 `-- nR2 * (err1:real) <= maxAbsFun (e2lo, e2hi) * err1`
                 [mp REAL_LE_RMUL THEN auto]
                 THEN SUBGOAL_TAC "err_neg_bound"
                 `-- ((err1:real) * err2) <= err1 * err2`
                 [ASM_SIMP_TAC[REAL_NEG_LMUL] THEN mp REAL_LE_RMUL THEN ASM_REAL_ARITH_TAC]
                 THEN SUBGOAL_TAC "zero_up_nR1"
                 `&0 <= maxAbsFun (e1lo:real,e1hi) * err2` [ASM_REAL_ARITH_TAC]
                 THEN SUBGOAL_TAC "nR1_to_sum"
                 `maxAbsFun (e1lo:real,e1hi) * err2 <= maxAbsFun (e1lo:real,e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1`
                 [ASM_REAL_ARITH_TAC]
                 THEN SUBGOAL_TAC "sum_to_errsum"
                 `maxAbsFun (e1lo:real, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1 <= maxAbsFun (e1lo:real, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1 + (err1 * err2)`
                 [ASM_REAL_ARITH_TAC]
                 (* Large case distinction for
Heiko Becker's avatar
Heiko Becker committed
468 469
                    a. different cases of the value of Rabs (...) and
                    b. wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *)
470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521
                 THEN rewrite REAL_ABS_CASES "err1_bounded"
                 THEN destruct "err1_bounded" "nR1_nF1_geq_0 nR1_nF1_le_err1 | nR1_nF1_lt_0 inv_nR1_nF1_le_err1"
                 THENL [
                   rewrite REAL_ABS_CASES "err2_bounded"
                     THEN destruct "err2_bounded" "nR2_nF2_geq_0 nR2_nF2_le_err2 | nR2_nF2_lt_0 inv_nR2_nF2_le_err2"
                     THENL [
                       (* SUBGOAL 1 *)
                       SUBGOAL_TAC "nF1_le"
                         `nF1:real <= err1 + nR1` [ASM_REAL_ARITH_TAC]
                         THEN SUBGOAL_TAC "nF2_le"
                         `nF2:real <= err2 + nR2` [ASM_REAL_ARITH_TAC]
                         THEN SIMP_TAC[REAL_ABS_CASES]
                         THEN LABEL_TAC "cases_sub" (SPECL [`(nR1:real * nR2) - (nF1 * nF2)`; `&0:real`] REAL_LTE_TOTAL)
                         THEN destruct "cases_sub" "sub_lt_0 | 0_leq_sub"
                         THENL [
                           (* nF1 * nF2 < nR1 * nR2 *)
                           right
                             THEN split
                             THEN (TRY ASM_REAL_ARITH_TAC)
                             THEN SIMP_TAC [real_sub; REAL_NEG_ADD; REAL_NEG_NEG]
                             THEN LABEL_TAC "cases_nF1" (SPECL [`nF1:real`; `&0:real`] REAL_LTE_TOTAL)
                             THEN destruct "cases_nF1" "nF1_lt_0 | 0_leq_nF1"
                             THENL[
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `-- ((nR1:real) * nR2) + nF1 * (nR2 - err2)`
                                 THEN SUBGOAL_TAC "lowerbound_nF2" `nR2 - err2:real <= nF2` [ASM_REAL_ARITH_TAC]
                                 THEN split
                                 THENL[
                                   SIMP_TAC[REAL_LE_LADD]
                                     THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_sub_err2" (SPECL [`nR2:real - err2`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_sub_err2" "nR2_lt_0 | 0_leq_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `--(nR1 * nR2:real) + (nR1 - err1) * (nR2 - err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `-- (nR1 * nR2:real) + (nR1 + err1) * (nR2 - err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
Heiko Becker's avatar
Heiko Becker committed
522

523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668
                                 ];
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `-- ((nR1:real) * nR2) + nF1 * (nR2 + err2)`
                                 THEN split
                                 THENL [
                                   SIMP_TAC [REAL_LE_LADD]
                                     THEN mp REAL_LE_LMUL
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_add_err2" (SPECL [`(nR2:real) + (err2:real)`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_add_err2" "nR2_lt_0 | 0_le_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `--(nR1 * nR2:real) + (nR1 - err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `-- (nR1 * nR2:real) + (nR1 + err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
                                 ]
                             ];
                           (* nF1 * nF2 >= nR1 * nR2 *)
                           left
                             THEN split
                             THEN (TRY ASM_REAL_ARITH_TAC)
                             THEN SIMP_TAC [real_sub; REAL_NEG_ADD; REAL_NEG_NEG; REAL_NEG_LMUL]
                             THEN LABEL_TAC "cases_nF1" (SPECL [`-- nF1:real`; `&0:real`] REAL_LTE_TOTAL)
                             THEN destruct "cases_nF1" "nF1_lt_0 | 0_leq_nF1"
                             THENL[
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `(nR1:real) * nR2 + -- nF1 * (nR2 - err2)`
                                 THEN SUBGOAL_TAC "lowerbound_nF2" `nR2 - err2:real <= nF2` [ASM_REAL_ARITH_TAC]
                                 THEN split
                                 THENL[
                                   SIMP_TAC[REAL_LE_LADD]
                                     THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_sub_err2" (SPECL [`nR2:real - err2`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_sub_err2" "nR2_lt_0 | 0_leq_nR2"]
                                 THENL [
                                   mp REAL_LE_TRANS
                                     THEN EXISTS_TAC `nR1 * (nR2:real) + -- (nR1 + err1) * (nR2 - err2)`
                                     THEN split
                                     THENL [
                                       SIMP_TAC[REAL_LE_LADD]
                                         THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                         THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                         THEN split THEN ASM_REAL_ARITH_TAC;
                                       ASM_REAL_ARITH_TAC];
                                   mp REAL_LE_TRANS
                                     THEN EXISTS_TAC `nR1 * (nR2:real) + -- (nR1 - err1) * (nR2 - err2)`
                                     THEN split
                                     THENL [
                                       SIMP_TAC [REAL_LE_LADD]
                                         THEN mp REAL_LE_RMUL
                                         THEN split THEN ASM_REAL_ARITH_TAC;
                                       ASM_REAL_ARITH_TAC]
                                 ];
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `((nR1:real) * nR2) + -- nF1 * (nR2 + err2)`
                                 THEN split
                                 THENL [
                                   SIMP_TAC [REAL_LE_LADD]
                                     THEN mp REAL_LE_LMUL
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_add_err2" (SPECL [`(nR2:real) + (err2:real)`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_add_err2" "nR2_lt_0 | 0_le_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `(nR1 * nR2:real) + -- (nR1 + err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `(nR1 * nR2:real) + -- (nR1 - err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
                                 ]
                             ]
                         ]
                       ;
                       (* SUBGOAL 2 *)
                       SUBGOAL_TAC "nF1_le"
                         `nF1:real <= err1 + nR1` [ASM_REAL_ARITH_TAC]
                         THEN SUBGOAL_TAC "nF2_le"
                         `nF2:real <= err2 + nR2` [ASM_REAL_ARITH_TAC]
                         THEN SIMP_TAC[REAL_ABS_CASES]
                         THEN LABEL_TAC "cases_sub" (SPECL [`(nR1:real * nR2) - (nF1 * nF2)`; `&0:real`] REAL_LTE_TOTAL)
                         THEN destruct "cases_sub" "sub_lt_0 | 0_leq_sub"
                         THENL [
                           (* nF1 * nF2 < nR1 * nR2 *)
                           right
                             THEN split
                             THEN (TRY ASM_REAL_ARITH_TAC)
                             THEN SIMP_TAC [real_sub; REAL_NEG_ADD; REAL_NEG_NEG]
                             THEN LABEL_TAC "cases_nF1" (SPECL [`nF1:real`; `&0:real`] REAL_LTE_TOTAL)
                             THEN destruct "cases_nF1" "nF1_lt_0 | 0_leq_nF1"
                             THENL[
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `-- ((nR1:real) * nR2) + nF1 * (nR2 - err2)`
                                 THEN SUBGOAL_TAC "lowerbound_nF2" `nR2 - err2:real <= nF2` [ASM_REAL_ARITH_TAC]
                                 THEN split
                                 THENL[
                                   SIMP_TAC[REAL_LE_LADD]
                                     THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_sub_err2" (SPECL [`nR2:real - err2`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_sub_err2" "nR2_lt_0 | 0_leq_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `--(nR1 * nR2:real) + (nR1 - err1) * (nR2 - err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `-- (nR1 * nR2:real) + (nR1 + err1) * (nR2 - err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
Heiko Becker's avatar
Heiko Becker committed
669

670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818
                                 ];
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `-- ((nR1:real) * nR2) + nF1 * (nR2 + err2)`
                                 THEN split
                                 THENL [
                                   SIMP_TAC [REAL_LE_LADD]
                                     THEN mp REAL_LE_LMUL
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_add_err2" (SPECL [`(nR2:real) + (err2:real)`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_add_err2" "nR2_lt_0 | 0_le_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `--(nR1 * nR2:real) + (nR1 - err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `-- (nR1 * nR2:real) + (nR1 + err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
                                 ]
                             ];
                           (* nF1 * nF2 >= nR1 * nR2 *)
                           left
                             THEN split
                             THEN (TRY ASM_REAL_ARITH_TAC)
                             THEN SIMP_TAC [real_sub; REAL_NEG_ADD; REAL_NEG_NEG; REAL_NEG_LMUL]
                             THEN LABEL_TAC "cases_nF1" (SPECL [`-- nF1:real`; `&0:real`] REAL_LTE_TOTAL)
                             THEN destruct "cases_nF1" "nF1_lt_0 | 0_leq_nF1"
                             THENL[
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `(nR1:real) * nR2 + -- nF1 * (nR2 - err2)`
                                 THEN SUBGOAL_TAC "lowerbound_nF2" `nR2 - err2:real <= nF2` [ASM_REAL_ARITH_TAC]
                                 THEN split
                                 THENL[
                                   SIMP_TAC[REAL_LE_LADD]
                                     THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_sub_err2" (SPECL [`nR2:real - err2`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_sub_err2" "nR2_lt_0 | 0_leq_nR2"]
                                 THENL [
                                   mp REAL_LE_TRANS
                                     THEN EXISTS_TAC `nR1 * (nR2:real) + -- (nR1 + err1) * (nR2 - err2)`
                                     THEN split
                                     THENL [
                                       SIMP_TAC[REAL_LE_LADD]
                                         THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                         THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                         THEN split THEN ASM_REAL_ARITH_TAC;
                                       ASM_REAL_ARITH_TAC];
                                   mp REAL_LE_TRANS
                                     THEN EXISTS_TAC `nR1 * (nR2:real) + -- (nR1 - err1) * (nR2 - err2)`
                                     THEN split
                                     THENL [
                                       SIMP_TAC [REAL_LE_LADD]
                                         THEN mp REAL_LE_RMUL
                                         THEN split THEN ASM_REAL_ARITH_TAC;
                                       ASM_REAL_ARITH_TAC]
                                 ];
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `((nR1:real) * nR2) + -- nF1 * (nR2 + err2)`
                                 THEN split
                                 THENL [
                                   SIMP_TAC [REAL_LE_LADD]
                                     THEN mp REAL_LE_LMUL
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_add_err2" (SPECL [`(nR2:real) + (err2:real)`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_add_err2" "nR2_lt_0 | 0_le_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `(nR1 * nR2:real) + -- (nR1 + err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `(nR1 * nR2:real) + -- (nR1 - err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
                                 ]
                             ]
                         ]
                     ];
                   rewrite REAL_ABS_CASES "err2_bounded"
                     THEN destruct "err2_bounded" "nR2_nF2_geq_0 nR2_nF2_le_err2 | nR2_nF2_lt_0 inv_nR2_nF2_le_err2"
                     THENL [
                       (* SUBGOAL 3 *)
                       SUBGOAL_TAC "nF1_le"
                         `nF1:real <= err1 + nR1` [ASM_REAL_ARITH_TAC]
                         THEN SUBGOAL_TAC "nF2_le"
                         `nF2:real <= err2 + nR2` [ASM_REAL_ARITH_TAC]
                         THEN SIMP_TAC[REAL_ABS_CASES]
                         THEN LABEL_TAC "cases_sub" (SPECL [`(nR1:real * nR2) - (nF1 * nF2)`; `&0:real`] REAL_LTE_TOTAL)
                         THEN destruct "cases_sub" "sub_lt_0 | 0_leq_sub"
                         THENL [
                           (* nF1 * nF2 < nR1 * nR2 *)
                           right
                             THEN split
                             THEN (TRY ASM_REAL_ARITH_TAC)
                             THEN SIMP_TAC [real_sub; REAL_NEG_ADD; REAL_NEG_NEG]
                             THEN LABEL_TAC "cases_nF1" (SPECL [`nF1:real`; `&0:real`] REAL_LTE_TOTAL)
                             THEN destruct "cases_nF1" "nF1_lt_0 | 0_leq_nF1"
                             THENL[
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `-- ((nR1:real) * nR2) + nF1 * (nR2 - err2)`
                                 THEN SUBGOAL_TAC "lowerbound_nF2" `nR2 - err2:real <= nF2` [ASM_REAL_ARITH_TAC]
                                 THEN split
                                 THENL[
                                   SIMP_TAC[REAL_LE_LADD]
                                     THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_sub_err2" (SPECL [`nR2:real - err2`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_sub_err2" "nR2_lt_0 | 0_leq_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `--(nR1 * nR2:real) + (nR1 - err1) * (nR2 - err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `-- (nR1 * nR2:real) + (nR1 + err1) * (nR2 - err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
819

820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965
                                 ];
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `-- ((nR1:real) * nR2) + nF1 * (nR2 + err2)`
                                 THEN split
                                 THENL [
                                   SIMP_TAC [REAL_LE_LADD]
                                     THEN mp REAL_LE_LMUL
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_add_err2" (SPECL [`(nR2:real) + (err2:real)`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_add_err2" "nR2_lt_0 | 0_le_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `--(nR1 * nR2:real) + (nR1 - err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `-- (nR1 * nR2:real) + (nR1 + err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
                                 ]
                             ];
                           (* nF1 * nF2 >= nR1 * nR2 *)
                           left
                             THEN split
                             THEN (TRY ASM_REAL_ARITH_TAC)
                             THEN SIMP_TAC [real_sub; REAL_NEG_ADD; REAL_NEG_NEG; REAL_NEG_LMUL]
                             THEN LABEL_TAC "cases_nF1" (SPECL [`-- nF1:real`; `&0:real`] REAL_LTE_TOTAL)
                             THEN destruct "cases_nF1" "nF1_lt_0 | 0_leq_nF1"
                             THENL[
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `(nR1:real) * nR2 + -- nF1 * (nR2 - err2)`
                                 THEN SUBGOAL_TAC "lowerbound_nF2" `nR2 - err2:real <= nF2` [ASM_REAL_ARITH_TAC]
                                 THEN split
                                 THENL[
                                   SIMP_TAC[REAL_LE_LADD]
                                     THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_sub_err2" (SPECL [`nR2:real - err2`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_sub_err2" "nR2_lt_0 | 0_leq_nR2"]
                                 THENL [
                                   mp REAL_LE_TRANS
                                     THEN EXISTS_TAC `nR1 * (nR2:real) + -- (nR1 + err1) * (nR2 - err2)`
                                     THEN split
                                     THENL [
                                       SIMP_TAC[REAL_LE_LADD]
                                         THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                         THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                         THEN split THEN ASM_REAL_ARITH_TAC;
                                       ASM_REAL_ARITH_TAC];
                                   mp REAL_LE_TRANS
                                     THEN EXISTS_TAC `nR1 * (nR2:real) + -- (nR1 - err1) * (nR2 - err2)`
                                     THEN split
                                     THENL [
                                       SIMP_TAC [REAL_LE_LADD]
                                         THEN mp REAL_LE_RMUL
                                         THEN split THEN ASM_REAL_ARITH_TAC;
                                       ASM_REAL_ARITH_TAC]
                                 ];
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `((nR1:real) * nR2) + -- nF1 * (nR2 + err2)`
                                 THEN split
                                 THENL [
                                   SIMP_TAC [REAL_LE_LADD]
                                     THEN mp REAL_LE_LMUL
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_add_err2" (SPECL [`(nR2:real) + (err2:real)`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_add_err2" "nR2_lt_0 | 0_le_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `(nR1 * nR2:real) + -- (nR1 + err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `(nR1 * nR2:real) + -- (nR1 - err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
                                 ]
                             ]
                         ]
                       ;
                       (* SUBGOAL 4 *)
                       SUBGOAL_TAC "nF1_le"
                         `nF1:real <= err1 + nR1` [ASM_REAL_ARITH_TAC]
                         THEN SUBGOAL_TAC "nF2_le"
                         `nF2:real <= err2 + nR2` [ASM_REAL_ARITH_TAC]
                         THEN SIMP_TAC[REAL_ABS_CASES]
                         THEN LABEL_TAC "cases_sub" (SPECL [`(nR1:real * nR2) - (nF1 * nF2)`; `&0:real`] REAL_LTE_TOTAL)
                         THEN destruct "cases_sub" "sub_lt_0 | 0_leq_sub"
                         THENL [
                           (* nF1 * nF2 < nR1 * nR2 *)
                           right
                             THEN split
                             THEN (TRY ASM_REAL_ARITH_TAC)
                             THEN SIMP_TAC [real_sub; REAL_NEG_ADD; REAL_NEG_NEG]
                             THEN LABEL_TAC "cases_nF1" (SPECL [`nF1:real`; `&0:real`] REAL_LTE_TOTAL)
                             THEN destruct "cases_nF1" "nF1_lt_0 | 0_leq_nF1"
                             THENL[
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `-- ((nR1:real) * nR2) + nF1 * (nR2 - err2)`
                                 THEN SUBGOAL_TAC "lowerbound_nF2" `nR2 - err2:real <= nF2` [ASM_REAL_ARITH_TAC]
                                 THEN split
                                 THENL[
                                   SIMP_TAC[REAL_LE_LADD]
                                     THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_sub_err2" (SPECL [`nR2:real - err2`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_sub_err2" "nR2_lt_0 | 0_leq_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `--(nR1 * nR2:real) + (nR1 - err1) * (nR2 - err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `-- (nR1 * nR2:real) + (nR1 + err1) * (nR2 - err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
966

967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068
                                 ];
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `-- ((nR1:real) * nR2) + nF1 * (nR2 + err2)`
                                 THEN split
                                 THENL [
                                   SIMP_TAC [REAL_LE_LADD]
                                     THEN mp REAL_LE_LMUL
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_add_err2" (SPECL [`(nR2:real) + (err2:real)`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_add_err2" "nR2_lt_0 | 0_le_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `--(nR1 * nR2:real) + (nR1 - err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `-- (nR1 * nR2:real) + (nR1 + err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
                                 ]
                             ];
                           (* nF1 * nF2 >= nR1 * nR2 *)
                           left
                             THEN split
                             THEN (TRY ASM_REAL_ARITH_TAC)
                             THEN SIMP_TAC [real_sub; REAL_NEG_ADD; REAL_NEG_NEG; REAL_NEG_LMUL]
                             THEN LABEL_TAC "cases_nF1" (SPECL [`-- nF1:real`; `&0:real`] REAL_LTE_TOTAL)
                             THEN destruct "cases_nF1" "nF1_lt_0 | 0_leq_nF1"
                             THENL[
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `(nR1:real) * nR2 + -- nF1 * (nR2 - err2)`
                                 THEN SUBGOAL_TAC "lowerbound_nF2" `nR2 - err2:real <= nF2` [ASM_REAL_ARITH_TAC]
                                 THEN split
                                 THENL[
                                   SIMP_TAC[REAL_LE_LADD]
                                     THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_sub_err2" (SPECL [`nR2:real - err2`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_sub_err2" "nR2_lt_0 | 0_leq_nR2"]
                                 THENL [
                                   mp REAL_LE_TRANS
                                     THEN EXISTS_TAC `nR1 * (nR2:real) + -- (nR1 + err1) * (nR2 - err2)`
                                     THEN split
                                     THENL [
                                       SIMP_TAC[REAL_LE_LADD]
                                         THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                         THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                         THEN split THEN ASM_REAL_ARITH_TAC;
                                       ASM_REAL_ARITH_TAC];
                                   mp REAL_LE_TRANS
                                     THEN EXISTS_TAC `nR1 * (nR2:real) + -- (nR1 - err1) * (nR2 - err2)`
                                     THEN split
                                     THENL [
                                       SIMP_TAC [REAL_LE_LADD]
                                         THEN mp REAL_LE_RMUL
                                         THEN split THEN ASM_REAL_ARITH_TAC;
                                       ASM_REAL_ARITH_TAC]
                                 ];
                               mp REAL_LE_TRANS
                                 THEN EXISTS_TAC `((nR1:real) * nR2) + -- nF1 * (nR2 + err2)`
                                 THEN split
                                 THENL [
                                   SIMP_TAC [REAL_LE_LADD]
                                     THEN mp REAL_LE_LMUL
                                     THEN split THEN ASM_REAL_ARITH_TAC;
                                   LABEL_TAC "cases_nR2_add_err2" (SPECL [`(nR2:real) + (err2:real)`; `&0:real`] REAL_LTE_TOTAL)
                                     THEN destruct "cases_nR2_add_err2" "nR2_lt_0 | 0_le_nR2"
                                     THENL [
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `(nR1 * nR2:real) + -- (nR1 + err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC[REAL_LE_LADD]
                                             THEN ONCE_REWRITE_TAC[REAL_MUL_SYM]
                                             THEN mp REAL_MUL_LE_COMPAT_NEG_L
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC];
                                       mp REAL_LE_TRANS
                                         THEN EXISTS_TAC `(nR1 * nR2:real) + -- (nR1 - err1) * (nR2 + err2)`
                                         THEN split
                                         THENL [
                                           SIMP_TAC [REAL_LE_LADD]
                                             THEN mp REAL_LE_RMUL
                                             THEN split THEN ASM_REAL_ARITH_TAC;
                                           ASM_REAL_ARITH_TAC]
                                     ]
                                 ]
                             ]
                         ]
                     ]
                 ]
               ;
Heiko Becker's avatar
Heiko Becker committed
1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088
               rewrite_asm "absenv_e1" "validbounds_e1"
                 THEN rewrite FST "validbounds_e1"
                 THEN rewrite FST "validbounds_e1"
                 THEN destruct "validbounds_e1" "valid_lo_e1 valid_hi_e1"
                 THEN pose_proof distance_gives_iv "errIve1"
                 [`nR1:real`;`nF1:real`;`err1:real`;`e1lo:real`;`e1hi:real`]
                 ["valid_lo_e1"; "valid_hi_e1"; "err1_bounded"]
                 THEN rewrite_asm "absenv_e2" "validbounds_e2"
                 THEN rewrite FST "validbounds_e2"
                 THEN rewrite FST "validbounds_e2"
                 THEN destruct "validbounds_e2" "valid_lo_e2 valid_hi_e2"
                 THEN pose_proof distance_gives_iv "errIve2"
                 [`nR2:real`;`nF2:real`;`err2:real`;`e2lo:real`;`e2hi:real`]
                 ["valid_lo_e2"; "valid_hi_e2"; "err2_bounded"]
                 THEN pose_proof interval_mult_valid "mult_valid"
                 [`(widenInterval (e1lo,e1hi) err1)`;`widenInterval (e2lo,e2hi) err2`] []
                 THEN spec "mult_valid" [`nF1:real`;`nF2:real`]
                 THEN mp_ispecl "mult_valid" ["errIve1"; "errIve2"]
                 THEN mp REAL_LE_RMUL
                 THEN split
1089
                 THENL [
Heiko Becker's avatar
Heiko Becker committed
1090 1091 1092 1093 1094
                   SUBGOAL_TAC "simp_iv" `?ivlo ivhi. multInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2) = (ivlo, ivhi)` [MESON_TAC [cases "prod"]]
                     THEN destruct "simp_iv" "@ivlo. @ivhi. simp_iv"
                     THEN ASM_SIMP_TAC[]
                     THEN rewrite_asm "simp_iv" "mult_valid"
                     THEN mp contained_leq_maxAbs THEN auto;
1095 1096 1097
                   SIMP_TAC[mEps_geq_zero]
                 ]
             ];
Heiko Becker's avatar
Heiko Becker committed
1098 1099
           REMOVE_THEN "valid_error"
             (fun th -> LABEL_TAC "valid_error" (SIMP_RULE[distinctness "binop"] (CONV_RULE COND_ELIM_CONV th)))
1100
             THEN auto
1101
         ]
Heiko Becker's avatar
Heiko Becker committed
1102 1103
     ]
 );;
1104

Heiko Becker's avatar
Heiko Becker committed
1105 1106 1107 1108 1109
(**
   Soundness theorem for the error bound validator.
   Proof is by induction on the expression e.
   Each case requires the application of one of the soundness lemmata proven before
**)
1110 1111 1112 1113 1114 1115 1116 1117 1118 1119
 let validErrorbound_sound = prove (
   `!(e:(real)exp) (cenv:env_ty) (absenv:analysisResult) (nR:real) (nF:real) (err:real) (P:precond) (elo:real) (ehi:real).
     precondValidForExec P cenv /\
     eval_exp (&0) cenv e nR /\
     eval_exp machineEpsilon cenv e nF /\
     validErrorbound e absenv = T /\
     validIntervalbounds e absenv P = T /\
     absenv e = ((elo,ehi),err) ==>
     abs (nR - nF) <= err`,
   mp exp_IND THEN SIMP_TAC[validErrorbound] THEN split
1120
     THENL [
1121 1122 1123 1124
       intros "!a cenv absenv nR nF err P elo ehi; p_valid eval_real eval_float bound_correct iv_correct absenv_param"
         THEN pose_proof ivbounds_approximatesPrecond_sound "fV_sound"
         [`(Param a):(real)exp`;`absenv:analysisResult`;`P:precond`]
         ["iv_correct"]
1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142
         THEN mp validErrorboundCorrectParam
         THEN EXISTS_TAC `cenv:env_ty`
         THEN EXISTS_TAC `absenv:analysisResult`
         THEN EXISTS_TAC `a:num`
         THEN EXISTS_TAC `P:precond`
         THEN EXISTS_TAC `elo:real`
         THEN EXISTS_TAC `ehi:real`
         THEN (REPEAT split) THEN SIMP_TAC[validErrorbound] THEN auto
         THEN intros "!n; MEM_n" THEN specialize "fV_sound" `n:num` THEN mp_spec "fV_sound" "MEM_n"
         THEN rewrite freeVars "MEM_n" THEN rewrite MEM "MEM_n"
         THEN destruct "MEM_n" "n_eq | false"
         THENL[
           rewrite_asm "n_eq" "fV_sound"
             THEN rewrite_asm "absenv_param" "fV_sound" THEN rewrite FST "fV_sound" THEN auto;
           rewrite MEM "false" THEN falsity "false"];
       split
         THENL [
           intros "!a cenv absenv nR nF err P elo ehi;
1143 1144 1145 1146
             p_valid eval_real eval_float bound_correct iv_correct absenv_const"
             THEN pose_proof ivbounds_approximatesPrecond_sound "fV_sound"
             [`(Const a):(real)exp`;`absenv:analysisResult`;`P:precond`]
             ["iv_correct"]
1147 1148 1149 1150 1151 1152 1153 1154 1155
             THEN mp validErrorboundCorrectConstant
             THEN EXISTS_TAC `cenv:env_ty`
             THEN EXISTS_TAC `absenv:analysisResult`
             THEN EXISTS_TAC `a:real`
             THEN EXISTS_TAC `elo:real`
             THEN EXISTS_TAC `ehi:real`
             THEN EXISTS_TAC `P:precond`
             THEN (REPEAT split) THEN SIMP_TAC[validErrorbound] THEN auto;
           intros "!a0 a1 a2; IH1 IH2"
1156 1157 1158 1159
             THEN intros "!cenv absenv nR nF err P elo ehi; p_valid eval_real eval_float valid_error valid_intv absenv_bin"
             THEN pose_proof ivbounds_approximatesPrecond_sound "fV_sound"
             [`(Binop a0 a1 a2):(real)exp`;`absenv:analysisResult`;`P:precond`]
             ["valid_intv"]
1160
             THEN SUBGOAL_TAC "absenv_e1" `?ivlo1 ivhi1 err1. (absenv:analysisResult) a1 = ((ivlo1,ivhi1),err1)` [MESON_TAC[cases "prod"]]
1161
             THEN destruct "absenv_e1" "@ivlo1. @ivhi1. @err1. absenv_e1"
1162
             THEN SUBGOAL_TAC "absenv_e2" `?ivlo2 ivhi2 err2. (absenv:analysisResult) a2 = ((ivlo2,ivhi2),err2)` [MESON_TAC[cases "prod"]]
1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180
             THEN destruct "absenv_e2" "@ivlo2. @ivhi2. @err2. absenv_e2"
             THEN rewrite_asm "absenv_bin" "valid_error"
             THEN rewrite_asm "absenv_e1" "valid_error"
             THEN rewrite_asm "absenv_e2" "valid_error"
             THEN simplify "valid_error"
             THEN destruct "valid_error" "valid_rec1 valid_rec2 err_geq_0 valid_error"
             THEN rewrite existential_rewriting "eval_float"
             THEN destruct "eval_float" "@v1F. @v2F. eval_a1F eval_a2F eval_float"
             THEN pose_proof binop_inv "real_inv"
             [`&0:real`; `cenv:env_ty`; `a0:binop`;`a1:(real)exp`;`a2:(real)exp`;`nR:real`]
             ["eval_real"]
             THEN LABEL_TAC "cases_bin" (SPEC `a0:binop` (cases "binop"))
             THEN destruct "cases_bin" "a0_eq | a0_eq | a0_eq | a0_eq"
             THEN rewrite_asm "a0_eq" "valid_error"
             THEN rewrite_asm "a0_eq" "valid_intv"
             THEN rewrite_asm "a0_eq" "real_inv"
             THEN rewrite_asm "a0_eq" "eval_real"
             THEN rewrite_asm "a0_eq" "eval_float"
1181
             THEN rewrite_asm "a0_eq" "absenv_bin"
1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192
             THEN destruct "real_inv" "@d. @v1R. @v2R. nR_eq eval_a1R eval_a2R d_less"
             THEN rewrite_asm "nR_eq" "eval_real"
             THEN rewrite validIntervalbounds "valid_intv"
             THEN rewrite_asm "absenv_bin" "valid_intv"
             THEN rewrite_asm "absenv_e1" "valid_intv"
             THEN rewrite_asm "absenv_e2" "valid_intv"
             THEN rewrite FST "valid_intv"
             THEN (TRY (destruct "valid_intv" "valid_intv_a1 valid_intv_a2 valid_intv"))
             THENL[
               mp validErrorboundCorrectAddition
                 THEN existsl [`cenv:env_ty`; `absenv:analysisResult`; `a1:(real)exp`; `a2:(real)exp`; `v1R:real`;`v2R:real`; `v1F:real`; `v2F:real`; `err1:real`; `err2:real`; `elo:real`; `ehi:real`; `ivlo1:real`; `ivhi1:real`; `ivlo2:real`; `ivhi2:real`; `P:precond`]
1193
                 THEN ASM_SIMP_TAC[validErrorbound; validIntervalbounds]
1194
                 THEN (REPEAT split)
1195 1196 1197 1198 1199 1200 1201 1202 1203 1204
                 THEN (TRY auto)
                 THENL [
                   REPEAT (CONV_TAC let_CONV)
                     THEN SUBGOAL_TAC "plus_eq_plus" `Plus = Plus <=> T` [MESON_TAC[]]
                     THEN rewrite_asm "plus_eq_plus" "valid_error"
                     THEN rewrite (SPEC `Plus = Sub` OR_CLAUSES) "valid_error"
                     THEN REMOVE_THEN "valid_error" (fun th -> LABEL_TAC "valid_error" (CONV_RULE (ONCE_SIMP_CONV[]) th))
                     THEN ASM_REWRITE_TAC[];
                   mp_asm "IH1"
                     THEN existsl [`cenv:env_ty`; `absenv:analysisResult`; `P:precond`; `ivlo1:real`; `ivhi1:real`]
1205
                     THEN (REPEAT split) THEN (TRY auto);
1206 1207 1208 1209
                   mp_asm "IH2"
                     THEN existsl [`cenv:env_ty`; `absenv:analysisResult`; `P:precond`; `ivlo2:real`; `ivhi2:real`]
                     THEN (REPEAT split) THEN (TRY auto)
                 ];
1210
               mp validErrorboundCorrectSubtraction
1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223
                 THEN existsl [`cenv:env_ty`; `absenv:analysisResult`; `a1:(real)exp`; `a2:(real)exp`; `v1R:real`;`v2R:real`; `v1F:real`; `v2F:real`; `err1:real`; `err2:real`; `elo:real`; `ehi:real`; `ivlo1:real`; `ivhi1:real`; `ivlo2:real`; `ivhi2:real`; `P:precond`]
                 THEN ASM_SIMP_TAC[validErrorbound; validIntervalbounds]
                 THEN (REPEAT split)
                 THEN (TRY auto)
                 THENL [
                   REPEAT (CONV_TAC let_CONV)
                     THEN SUBGOAL_TAC "plus_eq_plus" `Plus = Plus <=> T` [MESON_TAC[]]
                     THEN rewrite_asm "plus_eq_plus" "valid_error"
                     THEN rewrite (SPEC `Plus = Sub` OR_CLAUSES) "valid_error"
                     THEN REMOVE_THEN "valid_error" (fun th -> LABEL_TAC "valid_error" (CONV_RULE (ONCE_SIMP_CONV[]) th))
                     THEN ASM_REWRITE_TAC[];
                   mp_asm "IH1"
                     THEN existsl [`cenv:env_ty`; `absenv:analysisResult`; `P:precond`; `ivlo1:real`; `ivhi1:real`]
1224
                     THEN (REPEAT split) THEN (TRY auto);
1225 1226 1227 1228
                   mp_asm "IH2"
                     THEN existsl [`cenv:env_ty`; `absenv:analysisResult`; `P:precond`; `ivlo2:real`; `ivhi2:real`]
                     THEN (REPEAT split) THEN (TRY auto)
                 ];
1229
               mp validErrorboundCorrectMultiplication
1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242
                 THEN existsl [`cenv:env_ty`; `absenv:analysisResult`; `a1:(real)exp`; `a2:(real)exp`; `v1R:real`;`v2R:real`; `v1F:real`; `v2F:real`; `err1:real`; `err2:real`; `elo:real`; `ehi:real`; `ivlo1:real`; `ivhi1:real`; `ivlo2:real`; `ivhi2:real`; `P:precond`]
                 THEN ASM_SIMP_TAC[validErrorbound; validIntervalbounds]
                 THEN (REPEAT split)
                 THEN (TRY auto)
                 THENL [
                   REPEAT (CONV_TAC let_CONV)
                     THEN SUBGOAL_TAC "plus_eq_plus" `Plus = Plus <=> T` [MESON_TAC[]]
                     THEN rewrite_asm "plus_eq_plus" "valid_error"
                     THEN rewrite (SPEC `Plus = Sub` OR_CLAUSES) "valid_error"
                     THEN REMOVE_THEN "valid_error" (fun th -> LABEL_TAC "valid_error" (CONV_RULE (ONCE_SIMP_CONV[]) th))
                     THEN ASM_REWRITE_TAC[];
                   mp_asm "IH1"
                     THEN existsl [`cenv:env_ty`; `absenv:analysisResult`; `P:precond`; `ivlo1:real`; `ivhi1:real`]
1243
                     THEN (REPEAT split) THEN (TRY auto);
1244 1245 1246 1247
                   mp_asm "IH2"
                     THEN existsl [`cenv:env_ty`; `absenv:analysisResult`; `P:precond`; `ivlo2:real`; `ivhi2:real`]
                     THEN (REPEAT split) THEN (TRY auto)
                 ];
1248 1249 1250 1251
               falsity "valid_intv"
             ]
         ]
     ]);;