More work on bound proofs

hol/Commands.hl

@@ -13,12 +13,6 @@ let cmd_INDUCT, cmd_REC = define_type
        | Ret (V)exp
        | Nop ";;
 
-(*
-  Define environment update function for arbitrary type as abbreviation
-*)
-let upd_env_simps = define
-  `upd_env (x:num) (v:V) (E:num->V) =(\y. if y = x then v else E y)`;;
-
 (*
    Small Step semantics for Daisy language, parametric by evaluation function.
 *)

hol/ErrorBounds.hl

 needs "Infra/Abbrevs.hl";;
 needs "Expressions.hl";;
 
+(*
+  TOD: Move me
+  Define environment update function for arbitrary type as abbreviation
+*)
+let updEnv = define
+  `updEnv (x:num) (v:V) (E:num->V) =(\y. if y = x then v else E y)`;;
+
 let const_abs_err_bounded =
   prove (
     `!(n:real) (nR:real) (nF:real) (cenv:num->real).
@@ -52,3 +59,89 @@ let param_abs_err_bounded =
       THEN mp REAL_LE_TRANS
       THEN EXISTS_TAC `machineEpsilon:real` THEN split THEN TRY auto
       THEN SIMP_TAC[REAL_ABS_LE]);;
+
+g
+  `!(e1:(real)exp) (e1R:real) (e1F:real) (e2:(real)exp) (e2R:real) (e2F:real)
+  (vR:real) (vF:real) (cenv:num->real) (err1:real) (err2:real).
+  eval_exp (&0) cenv e1 e1R /\
+  eval_exp machineEpsilon cenv e1 e1F /\
+  eval_exp (&0) cenv e2 e2R /\
+  eval_exp machineEpsilon cenv e2 e2F /\
+  eval_exp (&0) cenv (Binop Plus e1 e2) vR /\
+  eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Plus (Var 1) (Var 2)) vF /\
+  abs (e1R - e1F) <= err1 /\
+  abs (e2R - e2F) <= err2 ==>
+  abs (vR - vF) <= err1 + err2 + (abs (e1F + e2F) * machineEpsilon)`;;
+(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
+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`; `Plus: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 "test" (SPECL [`e1:(real)exp`; `v1:real`; `e1R:real`; `cenv:num->real`] eval_0_det));;
+e (USE_THEN "e1_real" (fun th1 -> USE_THEN "eval_e1_v1" (fun th2 -> REMOVE_THEN "test" (fun th -> ASM_REWRITE_TAC [MP th (CONJ th2 th1)]))));;
+e (LABEL_TAC "test" (SPECL [`e2:(real)exp`; `v2:real`; `e2R:real`; `cenv:num->real`] eval_0_det));;
+e (USE_THEN "e2_real" (fun th1 -> USE_THEN "eval_e2_v2" (fun th2 -> REMOVE_THEN "test" (fun th -> ASM_REWRITE_TAC [MP th (CONJ th2 th1)]))));;
+e (SIMP_TAC[eval_binop]);;
+(* TODO: Make this a tactic *)
+e (REMOVE_THEN "abs_0" (fun _ -> REMOVE_THEN "eval_e1_v1" ( fun _ -> REMOVE_THEN "eval_e2_v2" (fun th -> ALL_TAC))));;
+(* 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))`;
+                    `Plus: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]);;
+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" THEN clear "v2F_inv" THEN clear "v1F_inv" THEN clear "eval_e2_v2F" THEN clear "eval_e1_v1F" THEN clear "vF_eq" THEN clear "vR_eq" THEN clear "e1_real" THEN clear "e2_real" THEN clear "plus_real" THEN clear "plus_float");;
+e (REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID; real_sub]);;
+e (ONCE_REWRITE_TAC [REAL_NEG_ADD]);;
+e (mp REAL_LE_TRANS);;
+e (EXISTS_TAC `abs ((e1R:real) + (e2R:real)) + abs (--((e1F:real) + (e2F:real)) +
+             --(((e1F:real) + (e2F:real)) * (delta2:real)))`);;
+e (split);;
+e (REWRITE_TAC[REAL_ABS_TRIANGLE]);;
+(* TODO !! *)
+search [`abs((a:real) + b) <= abs a + abs b`];;
+
+  rewrite Rplus_assoc.
+  eapply Rle_trans.
+  apply H.
+  pose proof (Rabs_triang (e2R + - e2F) (- ((e1F + e2F) * delta))).
+  pose proof (Rplus_le_compat_l (Rabs (e1R + - e1F)) _ _ H0).
+  eapply Rle_trans.
+  apply H1.
+  rewrite <- Rplus_assoc.
+  repeat rewrite <- Rsub_eq_Ropp_Rplus.
+  rewrite Rabs_Ropp.
+  eapply Rplus_le_compat.
+  - eapply Rplus_le_compat; auto.
+  - rewrite Rabs_mult.
+    eapply Rle_trans.
+    eapply Rmult_le_compat_l.
+    apply Rabs_pos.
+    apply H2.
+    apply Req_le; auto.

hol/Infra/tactics.hl

@@ -46,3 +46,5 @@ let assume lab t =
 let auto = TRY reflexivity THEN TRY (ASM_SIMP_TAC[]);;
 
 let mp = MATCH_MP_TAC;;
+
+let clear thn = REMOVE_THEN thn (fun th -> ALL_TAC);;