foo 3.88 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
e (intros "!e1 e1R e1F e2 e2R e2F vR vF cenv err1 err2; e1_real e1_float e2_real e2_float plus_real plus_float abs_e1 abs_e2");;
e (USE_THEN "plus_real"
     (fun th -> LABEL_TAC "plus_real_inv"
        (MP (SPECL [`&0:real`;`cenv:num->real`; `Sub:binop`;`e1:(real)exp`; `e2:(real)exp`; `vR:real`] binop_inv) th)));;
e (destruct "plus_real_inv" "@delta. @v1. @v2. vR_eq eval_e1_v1 eval_e2_v2 abs_0");;
e (ASM_SIMP_TAC[]
     THEN (USE_THEN "abs_0"
             (fun th -> REWRITE_TAC [MP (SPECL [`vR:real`; `delta:real`] perturb_0_val) th])));;
(* FIXME: UGLY REWRITES *)
e (LABEL_TAC "eval_e1_0_det"
     (SPECL [`e1:(real)exp`; `v1:real`; `e1R:real`; `cenv:num->real`] eval_0_det));;
e (SUBGOAL_TAC "eval_e1_conj" `eval_exp (&0) cenv e1 v1 /\ eval_exp (&0) cenv e1 e1R` [split THEN auto]);;
e (mp_spec "eval_e1_0_det" "eval_e1_conj");;
e (LABEL_TAC "eval_e2_0_det" (SPECL [`e2:(real)exp`; `v2:real`; `e2R:real`; `cenv:num->real`] eval_0_det));;
e (SUBGOAL_TAC "eval_e2_conj" `eval_exp (&0) cenv e2 v2 /\ eval_exp (&0) cenv e2 e2R` [split THEN auto]);;
e (mp_spec "eval_e2_0_det" "eval_e2_conj");;
e (ASM_SIMP_TAC[eval_binop]);;
e (clear ["eval_e2_0_det"; "eval_e2_conj"; "eval_e1_0_det"; "eval_e1_conj"; "eval_e1_v1"; "eval_e2_v2"]);;
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
e (USE_THEN "plus_float"
     (fun th -> LABEL_TAC "plus_float_inv"
        (MP (SPECL [`machineEpsilon:real`;
                    `(updEnv:num->real->(num->real)->num->real) 2 (e2F:real)
                        ((updEnv:num->real->(num->real)->num->real) 1 (e1F:real)
                           (cenv:num->real))`;
                    `Sub:binop`;`(Var 1):(real)exp`; `(Var 2):(real)exp`; `vF:real`] binop_inv) th)));;
e (destruct "plus_float_inv" "@delta2. @v1F. @v2F. vF_eq eval_e1_v1F eval_e2_v2F abs_mEps");;
e (USE_THEN "eval_e1_v1F"
     (fun th -> LABEL_TAC "v1F_inv"
        (MP (SPECL [`machineEpsilon:real`;
                    `(updEnv:num->real->(num->real)->num->real) 2 (e2F:real)
                        ((updEnv:num->real->(num->real)->num->real) 1 (e1F:real)
                           (cenv:num->real))`;
                    `1:num`; `v1F:real`] var_inv) th)));;
e (USE_THEN "eval_e2_v2F"
     (fun th -> LABEL_TAC "v2F_inv"
        (MP (SPECL [`machineEpsilon:real`;
                    `(updEnv:num->real->(num->real)->num->real) 2 (e2F:real)
                        ((updEnv:num->real->(num->real)->num->real) 1 (e1F:real)
                           (cenv:num->real))`;
                    `2:num`; `v2F:real`] var_inv) th)));;
e (ASM_REWRITE_TAC[updEnv; eval_binop; perturb]);;
(* TODO: Find out how to evaluate the conditional here! *)
e (SUBGOAL_TAC "1_neq_2" `1:num = 2:num <=> F` [ARITH_TAC]);;
e (ASM_REWRITE_TAC[]);;
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
e (clear ["1_neq_2"; "v2F_inv"; "v1F_inv"; "eval_e2_v2F"; "eval_e1_v1F"; "vF_eq"; "vR_eq"; "e1_real"; "e2_real"; "plus_real"; "plus_float"]);;
e (REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID; real_sub]);;
e (SUBGOAL_TAC "bounds_simplify" `((e1R:real) + e2R) + -- ((e1F + e2F) + (e1F + e2F) * delta2) =
    ((e1R:real) + -- e1F) + (e2R + -- e2F) + -- ((e1F + e2F) * delta2)` [REAL_ARITH_TAC]);;
e (ASM_SIMP_TAC[]);;

e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `abs (((e1R:real) + --(e1F:real))) + abs (((e2R:real) + --(e2F:real)) + --(((e1F:real) + (e2F:real)) * (delta2:real)))`);;
e (split);;
e (REWRITE_TAC[REAL_ABS_TRIANGLE]);;
e (mp REAL_LE_ADD2);;
e (split THENL [REWRITE_TAC[GSYM real_sub] THEN auto; ALL_TAC]);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `abs (((e2R:real) + --(e2F:real))) + abs (--(((e1F:real) + (e2F:real)) * (delta2:real)))`);;
e (split THENL [REWRITE_TAC [REAL_ABS_TRIANGLE]; ALL_TAC]);;
e (mp REAL_LE_ADD2);;
e (split THENL [REWRITE_TAC[GSYM real_sub] THEN auto; REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_MUL]]);;
e (mp REAL_LE_LMUL);;
e (split THENL [REWRITE_TAC[REAL_ABS_POS]; auto]);;