Update error bounds proofs

coq/ErrorBounds.v

@@ -260,23 +260,70 @@ Qed.
 
 Lemma fma_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
       (e3:exp Q) (e3R:R) (e3F:R)
-      (vR:R) (vF:R) (E1 E2:env) (err1 err2 err3:Q) (m m1 m2:mType) defVars:
+      (vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars:
   eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
   eval_exp E2 defVars (toRExp e1) e1F m1->
   eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
   eval_exp E2 defVars (toRExp e2) e2F m2 ->
   eval_exp E1 (toRMap defVars) (toREval (toRExp e3)) e3R M0 ->
-  eval_exp E2 defVars (toRExp e3) e3F m1->
+  eval_exp E2 defVars (toRExp e3) e3F m3->
   eval_exp E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR M0 ->
-  eval_exp (upd Env 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
+  eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
            (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
            (Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
-  (Rabs (e1R - e1F) <= Q2R err1)%R ->
-  (Rabs (e2R - e2F) <= Q2R err2)%R ->
-  (Rabs (e3R - e3F) <= Q2R err3)%R ->
-  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (mTypeToQ m))))%R.
-  (Rabs (vR - vF) <= Rabs (err1 + (e2R * e3R - e2F * e3F)) + Rabs (e1F + e2F * e3F) * (Q2R (mTypeToQ m)))%R.
+  (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + Rabs (e1F + e2F * e3F) * (Q2R (mTypeToQ m)))%R.
 Proof.
+  intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
+  inversion fma_real; subst;
+  assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
+  assert (m4 = M0) by (eapply toRMap_eval_M0; eauto).
+  assert (m5 = M0) by (eapply toRMap_eval_M0; eauto).
+  subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+  rewrite delta_0_deterministic in fma_real; auto.
+  rewrite delta_0_deterministic; auto.
+  unfold evalFma in *; simpl in *.
+  clear delta H3.
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real);
+    rewrite (meps_0_deterministic (toRExp e3) H7 e3_real).
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in fma_real.
+  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in fma_real.
+  rewrite (meps_0_deterministic (toRExp e3) H7 e3_real) in fma_real.
+  clear H5 H6 v1 v2 v3 H7 H2.
+  inversion fma_float; subst.
+  unfold evalFma in *.
+  unfold perturb; simpl.
+  inversion H3; subst; inversion H6; subst; inversion H7; subst.
+  unfold updEnv in *; simpl in *.
+  inversion H5; inversion H1; inversion H9; subst.
+  clear fma_float H7 fma_real e1_real e1_float e2_real e2_float e3_real e3_float H6 H1 H5 H9 H3 H0 H4 H8.
+  repeat rewrite Rmult_plus_distr_l.
+  rewrite Rmult_1_r.
+  rewrite Rsub_eq_Ropp_Rplus.
+  rewrite Ropp_plus_distr.
+  rewrite <- Rplus_assoc.
+  setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
+  rewrite Rsub_eq_Ropp_Rplus.
+  rewrite Rsub_eq_Ropp_Rplus.
+  rewrite Rsub_eq_Ropp_Rplus.
+  rewrite <- Rplus_assoc.
+  setoid_rewrite Rplus_comm at 8.
+  rewrite <- Rplus_assoc.
+  setoid_rewrite Rplus_comm at 9.
+  rewrite Rplus_assoc.
+  setoid_rewrite Rplus_assoc at 2.
+  rewrite <- Rplus_assoc.
+  rewrite <- Rsub_eq_Ropp_Rplus.
+  rewrite <- Rsub_eq_Ropp_Rplus.
+  rewrite <- Ropp_plus_distr.
+  rewrite <- Rsub_eq_Ropp_Rplus.
+  eapply Rle_trans.
+  eapply Rabs_triang.
+  eapply Rplus_le_compat_l.
+  rewrite Rabs_Ropp.
+  repeat rewrite Rabs_mult.
+  eapply Rmult_le_compat_l; auto.
+  apply Rabs_pos.
 Qed.
   
 

coq/Expressions.v

@@ -92,7 +92,7 @@ Definition evalUnop (o:unop) (v:R):=
   end .
 
 Definition evalFma (v1:R) (v2:R) (v3:R):=
-  Rplus v1 (Rmult v2 v3).
+  evalBinop Plus v1 (evalBinop Mult v2 v3).
 
 (**
   Define expressions parametric over some value type V.

coq/Infra/Ltacs.v

@@ -65,11 +65,6 @@ Ltac NatSet_prop :=
   | _ => try auto
   end.
 
-Ltac match_simpl :=
-  match goal with
-  | [ H: ?t = ?u |- context [match ?t with _ => _ end]] => rewrite H; simpl
-  end.
-
 Ltac destruct_if :=
   match goal with
   | [H: (if ?c then ?a else ?b) = _ |- _ ] =>
@@ -80,6 +75,60 @@ Ltac destruct_if :=
     try congruence
   end.
 
+Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
+match v with
+|Some val => f val
+| None => e
+end.
+
+Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
+match v with |Some val => f val | None => e end = optionLift X Y v f e.
+Proof.
+cbv; auto.
+Qed.
+
+Lemma optionLift_cond X (a:bool) (b c :X):
+(if a then b else c) = match a with |true => b |false => c end.
+Proof.
+cbv; auto.
+Qed.
+
+Ltac remove_matches := rewrite optionLift_eq in *.
+
+Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *.
+
+Ltac match_factorize :=
+match goal with
+| [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]]
+=> rewrite H; cbn
+| [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ]
+=> rewrite H1 in H2; cbn in H2
+| [ H: context [optionLift _ _ ?t _ _] |- _ ]
+=> destruct t eqn:?; cbn in H; try congruence
+| [ |- context [optionLift _ _ ?t _ _] ]
+=> destruct t eqn:?; cbn; try congruence
+end.
+
+Ltac pair_factorize :=
+match goal with
+| [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H
+end.
+
+Ltac match_simpl :=
+try remove_conds;
+try remove_matches;
+repeat match_factorize;
+try pair_factorize.
+
+Ltac bool_factorize :=
+match goal with
+| [H: _ = true |- _] => andb_to_prop H
+end.
+
+Ltac Daisy_compute :=
+repeat
+(match_simpl || bool_factorize).
+
 (* HOL4 Style patter matching tactics *)
 Tactic Notation "lift " tactic(t) :=
   fun H => t H.
@@ -87,4 +136,4 @@ Tactic Notation "lift " tactic(t) :=
 Tactic Notation "match_pat" open_constr(pat) tactic(t) :=
   match goal with
   | [H: ?ty |- _ ] => unify pat ty; t H
-  end.
\ No newline at end of file
+  end.

coq/IntervalValidation.v

@@ -440,6 +440,7 @@ Proof.
         repeat rewrite <- Q2R_min4, <- Q2R_max4 in *.
       specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
       unfold evalFma.
+      unfold evalBinop.
       unfold perturb.
       lra.
   - env_assert absenv (Downcast m f) absenv_d;