(** 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.v to build the complete checker. **) From Coq Require Import QArith.QArith QArith.Qminmax QArith.Qabs QArith.Qreals micromega.Psatz Reals.Reals. From Flover Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing ErrorBounds. (** Error bound validator **) Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *) (typeMap:FloverMap.t mType) (* derived types for e *) (A:analysisResult) (* encoded result of Flover *) (dVars:NatSet.t) (* let-bound variables encountered previously *):= match FloverMap.find e A, FloverMap.find e typeMap with | Some (intv, err), Some m => if (Qleb 0 err) (* encoding soundness: errors are positive *) then match e with (* case analysis for the expression *) |Var _ v => if (NatSet.mem v dVars) then true (* defined variables are checked at definition point *) else Qleb (computeErrorQ (maxAbs intv) m) err |Const m n => Qleb (computeErrorQ (maxAbs intv) m) err |Unop Neg e1 => if (validErrorbound e1 typeMap A dVars) then match FloverMap.find e1 A with | Some (iv_e1, err1) => Qeq_bool err err1 | None => false end else false |Unop Inv e1 => false |Binop b e1 e2 => if ((validErrorbound e1 typeMap A dVars) && (validErrorbound e2 typeMap A dVars)) then match FloverMap.find e1 A, FloverMap.find e2 A with | Some (ive1, err1), Some (ive2, err2) => let errIve1 := widenIntv ive1 err1 in let errIve2 := widenIntv ive2 err2 in let upperBoundE1 := maxAbs ive1 in let upperBoundE2 := maxAbs ive2 in match b with | Plus => let mAbs := (maxAbs (addIntv errIve1 errIve2)) in Qleb (err1 + err2 + computeErrorQ mAbs m) err | Sub => let mAbs := (maxAbs (subtractIntv errIve1 errIve2)) in Qleb (err1 + err2 + computeErrorQ mAbs m) err | Mult => let mAbs := (maxAbs (multIntv errIve1 errIve2)) in let eProp := (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) in Qleb (eProp + computeErrorQ mAbs m) err | Div => if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) || ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0)))) then let upperBoundInvE2 := maxAbs (invertIntv ive2) in let minAbsIve2 := minAbs (errIve2) in let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in let mAbs := (maxAbs (divideIntv errIve1 errIve2)) in let eProp := (upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) in Qleb (eProp + computeErrorQ mAbs m) err else false end | _, _ => false end else false | Fma e1 e2 e3 => if ((validErrorbound e1 typeMap A dVars) && (validErrorbound e2 typeMap A dVars) && (validErrorbound e3 typeMap A dVars)) then match FloverMap.find e1 A, FloverMap.find e2 A, FloverMap.find e3 A with | Some (ive1, err1), Some (ive2, err2), Some (ive3, err3) => let errIve1 := widenIntv ive1 err1 in let errIve2 := widenIntv ive2 err2 in let errIve3 := widenIntv ive3 err3 in let upperBoundE1 := maxAbs ive1 in let upperBoundE2 := maxAbs ive2 in let upperBoundE3 := maxAbs ive3 in let errIntv_prod := multIntv errIve2 errIve3 in let mult_error_bound := (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in let mAbs := (maxAbs (addIntv errIve1 errIntv_prod)) in Qleb (err1 + mult_error_bound + computeErrorQ mAbs m) err | _, _, _ => false end else false |Downcast m1 e1 => if validErrorbound e1 typeMap A dVars then match FloverMap.find e1 A with | Some (ive1, err1) => let errIve1 := widenIntv ive1 err1 in let mAbs := maxAbs errIve1 in Qleb (err1 + computeErrorQ mAbs m1) err | None => false end else false end else false | _, _ => false end. (** Error bound command validator **) Fixpoint validErrorboundCmd (f:cmd Q) (* analyzed cmd with let's *) typeMap (* inferred types *) (A:analysisResult) (* Flover's encoded result *) (dVars:NatSet.t) (* defined variables *) : bool := match f with |Let m x e g => match FloverMap.find e A, FloverMap.find (Var Q x) A with | Some (iv_e, err_e), Some (iv_x, err_x) => if ((validErrorbound e typeMap A dVars) && (Qeq_bool err_e err_x)) then validErrorboundCmd g typeMap A (NatSet.add x dVars) else false | _,_ => false end |Ret e => validErrorbound e typeMap A dVars end. (* Hide mTypeToQ from simplification since it will blow up the goal buffer *) Arguments mTypeToQ _ :simpl nomatch. (** 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. **) Lemma err_always_positive e tmap (A:analysisResult) dVars iv err: validErrorbound e tmap A dVars = true -> FloverMap.find e A = Some (iv,err) -> (0 <= Q2R err)%R. Proof. destruct e; cbn; intros; Flover_compute; canonize_hyps; auto. Qed. Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi P fVars dVars Gamma exprTypes: eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL -> typeCheck (Var Q v) Gamma exprTypes = true -> approxEnv E1 Gamma A fVars dVars E2 -> validIntervalbounds (Var Q v) A P dVars = true -> validErrorbound (Var Q v) exprTypes A dVars = true -> NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars -> dVars_range_valid dVars E1 A -> fVars_P_sound fVars E1 P -> vars_typed (NatSet.union fVars dVars) Gamma -> FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) -> exists nF m, eval_expr E2 Gamma (toRExp (Var Q v)) nF m. Proof. intros eval_real typing_ok approxCEnv bounds_valid error_valid v_sound dVars_sound P_valid types_valid A_var. eapply validIntervalbounds_sound in bounds_valid; eauto. destruct_smart [find_v [eval_real2 bounds_valid]] bounds_valid. pose proof (meps_0_deterministic _ eval_real eval_real2). subst. cbn in *. inversion eval_real; subst. Flover_compute; type_conv. destruct (approxEnv_gives_value approxCEnv H1); try eauto. set_tac. case_eq (NatSet.mem v dVars); intros v_case; set_tac. left; apply v_sound. apply NatSetProps.FM.diff_3; set_tac. Qed. Lemma validErrorboundCorrectVariable: forall E1 E2 A (v:nat) e nR nF mF nlo nhi P fVars dVars Gamma exprTypes, eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL -> eval_expr E2 Gamma (toRExp (Var Q v)) nF mF -> typeCheck (Var Q v) Gamma exprTypes = true -> approxEnv E1 Gamma A fVars dVars E2 -> validIntervalbounds (Var Q v) A P dVars = true -> validErrorbound (Var Q v) exprTypes A dVars = true -> NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars -> dVars_range_valid dVars E1 A -> fVars_P_sound fVars E1 P -> vars_typed (NatSet.union fVars dVars) Gamma -> FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. intros * eval_real eval_float typing_ok approxCEnv bounds_valid error_valid v_sound dVars_sound P_valid types_valid A_var. eapply validIntervalbounds_sound in bounds_valid; eauto. destruct_smart [find_v [eval_real2 bounds_valid]] bounds_valid. pose proof (meps_0_deterministic _ eval_real eval_real2); subst. cbn in *; Flover_compute; type_conv. inversion eval_real; inversion eval_float; subst. rename H1 into E1_v. rename L into error_pos. rename R into error_valid. case_eq (v mem dVars); [intros v_dVar | intros v_fVar]. - rewrite v_dVar in *; simpl in *. rewrite NatSet.mem_spec in v_dVar. eapply approxEnv_dVar_bounded; eauto. - rewrite v_fVar in *; simpl in *. apply not_in_not_mem in v_fVar. assert (v ∈ fVars) as v_in_fVars by set_tac. pose proof (approxEnv_fVar_bounded approxCEnv E1_v H6 v_in_fVars H5). eapply Rle_trans; eauto. canonize_hyps. repeat destr_factorize. rewrite computeErrorQ_computeErrorR in error_valid. eapply Rle_trans; eauto. rewrite <- maxAbs_impl_RmaxAbs. apply computeErrorR_up. apply contained_leq_maxAbs. simpl in *; auto. Qed. Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR Gamma: eval_expr E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR REAL -> exists nF m', eval_expr E2 Gamma (toRExp (Const m n)) nF m'. Proof. intros eval_real . repeat eexists. eapply Const_dist'; eauto. instantiate (1:= 0%R). rewrite Rabs_R0. auto using mTypeToR_pos_R. Qed. Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma defVars: eval_expr E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR REAL -> eval_expr E2 defVars (toRExp (Const m n)) nF m -> typeCheck (Const m n) defVars Gamma = true -> validErrorbound (Const m n) Gamma A dVars = true -> (Q2R nlo <= nR <= Q2R nhi)%R -> FloverMap.find (Const m n) A = Some ((nlo,nhi),e) -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. intros eval_real eval_float subexprr_ok error_valid intv_valid A_const. cbn in *; Flover_compute; type_conv. eapply Rle_trans. eapply const_abs_err_bounded; eauto. rename R into error_valid. inversion eval_real; subst. canonize_hyps. eapply Rle_trans; eauto. rewrite computeErrorQ_computeErrorR. rewrite <- maxAbs_impl_RmaxAbs. apply computeErrorR_up. apply contained_leq_maxAbs. simpl in *; auto. Qed. Lemma validErrorboundCorrectAddition E1 E2 A (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars: m = join m1 m2 -> eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR REAL -> eval_expr E2 defVars (toRExp e1) nF1 m1 -> eval_expr E2 defVars (toRExp e2) nF2 m2 -> eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m -> typeCheck (Binop Plus e1 e2) defVars Gamma = true -> validErrorbound (Binop Plus e1 e2) Gamma A dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> FloverMap.find e1 A = Some ((e1lo,e1hi),err1) -> FloverMap.find e2 A = Some ((e2lo, e2hi),err2) -> FloverMap.find (Binop Plus e1 e2) A = Some ((alo,ahi),e)-> (Rabs (nR1 - nF1) <= (Q2R err1))%R -> (Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float subexprr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add err1_bounded err2_bounded. cbn in *; Flover_compute; type_conv. eapply Rle_trans. eapply (add_abs_err_bounded e1 e2); try eauto. pose proof (typingSoundnessExp _ _ R2 e1_float). pose proof (typingSoundnessExp _ _ R1 e2_float). repeat destr_factorize. rename R0 into valid_error. eapply Rle_trans. apply Rplus_le_compat_l. Focus 2. rewrite Qle_bool_iff in valid_error. apply Qle_Rle in valid_error. repeat rewrite Q2R_plus in valid_error. eauto. clear L R. assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded) as contained_widen1. assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. pose proof (distance_gives_iv (a:=nR2) _ (Q2R e2lo, Q2R e2hi) contained_intv2 err2_bounded) as contained_widen2. pose proof (IntervalArith.interval_addition_valid _ _ contained_widen1 contained_widen2). rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv. apply computeErrorR_up. apply contained_leq_maxAbs. simpl in *; split. - rewrite Q2R_min4. repeat rewrite Q2R_plus; repeat rewrite Q2R_minus; lra. - rewrite Q2R_max4. repeat rewrite Q2R_plus; repeat rewrite Q2R_minus; lra. Qed. Lemma validErrorboundCorrectSubtraction E1 E2 A (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars: m = join m1 m2 -> eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR REAL -> eval_expr E2 defVars (toRExp e1) nF1 m1-> eval_expr E2 defVars (toRExp e2) nF2 m2 -> eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m -> typeCheck (Binop Sub e1 e2) defVars Gamma = true -> validErrorbound (Binop Sub e1 e2) Gamma A dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> FloverMap.find e1 A = Some ((e1lo,e1hi),err1) -> FloverMap.find e2 A = Some ((e2lo, e2hi),err2) -> FloverMap.find (Binop Sub e1 e2) A = Some ((alo,ahi),e)-> (Rabs (nR1 - nF1) <= (Q2R err1))%R -> (Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float subexprr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub err1_bounded err2_bounded. cbn in *; Flover_compute; type_conv. eapply Rle_trans. eapply (subtract_abs_err_bounded e1 e2); try eauto. pose proof (typingSoundnessExp _ _ R2 e1_float). pose proof (typingSoundnessExp _ _ R1 e2_float). repeat destr_factorize. rename R0 into valid_error. canonize_hyps. repeat rewrite Q2R_plus in valid_error. repeat rewrite Q2R_mult in valid_error. repeat rewrite Q2R_plus in valid_error. eapply Rle_trans. apply Rplus_le_compat_l. Focus 2. apply valid_error. rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv. assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded) as contained_widen1. assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded) as contained_widen2. pose proof (IntervalArith.interval_subtraction_valid _ _ contained_widen1 contained_widen2). apply computeErrorR_up. apply contained_leq_maxAbs. simpl in *; split. - rewrite Q2R_min4. repeat rewrite Q2R_plus; repeat rewrite Q2R_minus; repeat rewrite Q2R_opp; repeat rewrite Q2R_plus; repeat rewrite Q2R_minus; lra. - rewrite Q2R_max4. repeat rewrite Q2R_plus; repeat rewrite Q2R_minus; repeat rewrite Q2R_opp; repeat rewrite Q2R_plus; repeat rewrite Q2R_minus; lra. Qed. Lemma multiplicationErrorBounded e1lo e1hi e2lo e2hi nR1 nF1 nR2 nF2 err1 err2 : (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> (Rabs (nR1 - nF1) <= Q2R err1)%R -> (Rabs (nR2 - nF2) <= Q2R err2)%R -> (0 <= Q2R err1)%R -> (0 <= Q2R err2)%R -> (Rabs (nR1 * nR2 - nF1 * nF2) <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 + Q2R err1 * Q2R err2)%R. Proof. intros valid_e1 valid_e2 err1_bounded err2_bounded err1_pos err2_pos. unfold Rabs in err1_bounded. unfold Rabs in err2_bounded. (* Before doing case distinction, prove bounds that will be used many times: *) assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R as upperBound_nR1 by (apply contained_leq_maxAbs_val; auto). assert (nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R as upperBound_nR2 by (apply contained_leq_maxAbs_val; auto). assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R as upperBound_Ropp_nR1 by (apply contained_leq_maxAbs_neg_val; auto). assert (- nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R as upperBound_Ropp_nR2 by (apply contained_leq_maxAbs_neg_val; auto). assert (nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as bound_nR1 by (apply Rmult_le_compat_r; auto). assert (- nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as bound_neg_nR1 by (apply Rmult_le_compat_r; auto). assert (nR2 * Q2R err1 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R as bound_nR2 by (apply Rmult_le_compat_r; auto). assert (- nR2 * Q2R err1 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R as bound_neg_nR2 by (apply Rmult_le_compat_r; auto). assert (- (Q2R err1 * Q2R err2) <= Q2R err1 * Q2R err2)%R as err_neg_bound by (rewrite Ropp_mult_distr_l; apply Rmult_le_compat_r; lra). assert (0 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as zero_up_nR1 by lra. assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R as nR1_to_sum by lra. assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 + Q2R err1 * Q2R err2)%R as sum_to_errsum by lra. (* Large case distinction for a) different cases of the value of Rabs (...) and b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *) destruct Rcase_abs in err1_bounded; destruct Rcase_abs in err2_bounded. + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. rewrite Ropp_plus_distr in err1_bounded, err2_bounded. rewrite Ropp_involutive in err1_bounded, err2_bounded. assert (nF1 <= Q2R err1 + nR1)%R by lra. assert (nF2 <= Q2R err2 + nR2)%R by lra. unfold Rabs. destruct Rcase_abs. * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. rewrite Ropp_involutive. destruct (Rle_lt_dec 0 nF1). { (* Upper Bound ... *) eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. apply H0. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 <= nF1)%R by lra. apply H1. lra. } { eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR2 < nF2)%R by lra. apply Rlt_le in H1; apply H1. destruct (Rle_lt_dec 0 nR2). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 < nF1)%R by lra. apply Rlt_le in H1; apply H1. lra. } * rewrite Rsub_eq_Ropp_Rplus. destruct (Rle_lt_dec 0 nF1). { rewrite Ropp_mult_distr_r. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. assert (- nF2 <= - nR2)%R by lra. apply H1. destruct (Rle_lt_dec 0 (- nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 < nF1)%R by lra. apply Rlt_le in H1; apply H1. lra. } { rewrite Ropp_mult_distr_l. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l. rewrite <- (Ropp_involutive 0). apply Ropp_ge_le_contravar. apply Rle_ge. rewrite Ropp_0. hnf. left; auto. apply H0. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. assert (- nF1 <= -nR1)%R by lra. apply H1. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. apply Ropp_le_ge_contravar in H. apply Rge_le in H. apply H. lra. } + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. rewrite Ropp_plus_distr in err1_bounded. rewrite Ropp_involutive in err1_bounded. assert (nF1 <= Q2R err1 + nR1)%R by lra. assert (nF2 <= Q2R err2 + nR2)%R by lra. unfold Rabs. destruct Rcase_abs. * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. rewrite Ropp_involutive. destruct (Rle_lt_dec 0 nF1). { (* Upper Bound ... *) eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. apply H0. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 <= nF1)%R by lra. apply H1. lra. } { eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (- nF2 <= - (nR2 - Q2R err2))%R by lra. apply Ropp_le_ge_contravar in H1. repeat rewrite Ropp_involutive in H1. apply Rge_le in H1. apply H1. destruct (Rle_lt_dec 0 (nR2 - Q2R err2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 < nF1)%R by lra. apply Rlt_le in H1; apply H1. lra. } * rewrite Rsub_eq_Ropp_Rplus. destruct (Rle_lt_dec 0 nF1). { rewrite Ropp_mult_distr_r. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. assert (- nF2 <= - nR2 + Q2R err2)%R by lra. apply H1. destruct (Rle_lt_dec 0 (- nR2 + Q2R err2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 < nF1)%R by lra. apply Rlt_le in H1; apply H1. lra. } { rewrite Ropp_mult_distr_l. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l. rewrite <- (Ropp_involutive 0). apply Ropp_ge_le_contravar. apply Rle_ge. rewrite Ropp_0. hnf. left; auto. apply H0. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. assert (- nF1 <= -nR1)%R by lra. apply H1. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. apply Ropp_le_ge_contravar in H. apply Rge_le in H. apply H. lra. } + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. rewrite Ropp_plus_distr in err2_bounded. rewrite Ropp_involutive in err2_bounded. assert (nF1 <= Q2R err1 + nR1)%R by lra. assert (nF2 <= Q2R err2 + nR2)%R by lra. unfold Rabs. destruct Rcase_abs. * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. rewrite Ropp_involutive. destruct (Rle_lt_dec 0 nF1). { (* Upper Bound ... *) eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. apply H0. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. apply Ropp_le_ge_contravar in H1. repeat rewrite Ropp_involutive in H1. apply Rge_le in H1. apply H1. lra. } { eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR2 < nF2)%R by lra. apply Rlt_le in H1; apply H1. destruct (Rle_lt_dec 0 nR2). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. apply Ropp_le_ge_contravar in H1. repeat rewrite Ropp_involutive in H1. apply Rge_le in H1. apply H1. lra. } * rewrite Rsub_eq_Ropp_Rplus. destruct (Rle_lt_dec 0 nF1). { rewrite Ropp_mult_distr_r. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. assert (- nF2 <= - nR2)%R by lra. apply H1. destruct (Rle_lt_dec 0 (- nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. apply Ropp_le_ge_contravar in H1. repeat rewrite Ropp_involutive in H1. apply Rge_le in H1. apply H1. lra. } { rewrite Ropp_mult_distr_l. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l. lra. apply H0. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. apply H1. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l; try lra. apply Ropp_le_ge_contravar in H. apply Rge_le in H. apply H. lra. } (* All positive *) + assert (nF1 <= Q2R err1 + nR1)%R by lra. assert (nF2 <= Q2R err2 + nR2)%R by lra. unfold Rabs. destruct Rcase_abs. * rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_plus_distr. rewrite Ropp_involutive. destruct (Rle_lt_dec 0 nF1). { (* Upper Bound ... *) eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. apply H0. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 - Q2R err1 <= nF1)%R by lra. apply H1. lra. } { eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR2 - Q2R err2 <= nF2)%R by lra. apply H1. destruct (Rle_lt_dec 0 (nR2 - Q2R err2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. lra. assert (nR1 - Q2R err1 <= nF1)%R by lra. apply H1. lra. } * rewrite Rsub_eq_Ropp_Rplus. destruct (Rle_lt_dec 0 nF1). { rewrite Ropp_mult_distr_r. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. assert (- nF2 <= Q2R err2 - nR2)%R by lra. apply H1. destruct (Rle_lt_dec 0 (Q2R err2 - nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. apply H. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. lra. assert (nR1 - Q2R err1 <= nF1)%R by lra. apply H1. lra. } { rewrite Ropp_mult_distr_l. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l. rewrite <- (Ropp_involutive 0). apply Ropp_ge_le_contravar. apply Rle_ge. rewrite Ropp_0. lra. apply H0. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. assert (- nF1 <= Q2R err1 - nR1)%R by lra. apply H1. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. lra. apply Ropp_le_ge_contravar in H. apply Rge_le in H. apply H. lra. } Qed. Lemma validErrorboundCorrectMult E1 E2 A (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars: m = join m1 m2 -> eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR REAL -> eval_expr E2 defVars (toRExp e1) nF1 m1 -> eval_expr E2 defVars (toRExp e2) nF2 m2 -> eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m -> typeCheck (Binop Mult e1 e2) defVars Gamma = true -> validErrorbound (Binop Mult e1 e2) Gamma A dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> FloverMap.find e1 A = Some ((e1lo,e1hi),err1) -> FloverMap.find e2 A = Some ((e2lo, e2hi),err2) -> FloverMap.find (Binop Mult e1 e2) A = Some ((alo,ahi),e)-> (Rabs (nR1 - nF1) <= (Q2R err1))%R -> (Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float subexprr_ok valid_error valid_e1 valid_e2 A_e1 A_e2 A_mult err1_bounded err2_bounded. cbn in *; Flover_compute; type_conv; subst. eapply Rle_trans. eapply (mult_abs_err_bounded e1 e2); eauto. pose proof (typingSoundnessExp _ _ R2 e1_float). pose proof (typingSoundnessExp _ _ R1 e2_float). rewrite H in Heqo0; rewrite H0 in Heqo1; inversion Heqo0; inversion Heqo1; subst. clear H H0. rename R0 into valid_error. assert (0 <= Q2R err1)%R as err1_pos. { pose proof (err_always_positive e1 Gamma A dVars); eauto. } assert (0 <= Q2R err2)%R as err2_pos. { pose proof (err_always_positive e2 Gamma A dVars); eauto. } clear R2 R1. canonize_hyps. repeat rewrite Q2R_plus in valid_error. repeat rewrite Q2R_mult in valid_error. repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error. eapply Rle_trans. Focus 2. apply valid_error. apply Rplus_le_compat. - eauto using multiplicationErrorBounded. - rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv. apply computeErrorR_up. apply contained_leq_maxAbs. assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded) as cont_err1. assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded) as cont_err2. pose proof (IntervalArith.interval_multiplication_valid _ _ cont_err1 cont_err2) as valid_mult. simpl in *; split. + rewrite Q2R_min4. repeat rewrite Q2R_mult; repeat rewrite Q2R_minus; repeat rewrite Q2R_plus. lra. + rewrite Q2R_max4. repeat rewrite Q2R_mult; repeat rewrite Q2R_minus; repeat rewrite Q2R_plus; lra. Qed. Lemma validErrorboundCorrectDiv E1 E2 A (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars: m = join m1 m2 -> eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR REAL -> eval_expr E2 defVars (toRExp e1) nF1 m1 -> eval_expr E2 defVars (toRExp e2) nF2 m2 -> eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m -> typeCheck (Binop Div e1 e2) defVars Gamma = true -> validErrorbound (Binop Div e1 e2) Gamma A dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> (Qleb e2hi 0 && negb (Qeq_bool e2hi 0) || Qleb 0 e2lo && negb (Qeq_bool e2lo 0) = true) -> FloverMap.find e1 A = Some ((e1lo,e1hi),err1) -> FloverMap.find e2 A = Some ((e2lo, e2hi),err2) -> FloverMap.find (Binop Div e1 e2) A = Some ((alo,ahi),e)-> (Rabs (nR1 - nF1) <= (Q2R err1))%R -> (Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float subexprr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real A_e1 A_e2 A_div err1_bounded err2_bounded. cbn in *; Flover_compute; type_conv; subst. eapply Rle_trans. eapply (div_abs_err_bounded e1 e2); eauto. pose proof (typingSoundnessExp _ _ R2 e1_float). pose proof (typingSoundnessExp _ _ R0 e2_float). rewrite H in Heqo0; rewrite H0 in Heqo1; inversion Heqo0; inversion Heqo1; subst. clear H H0. rename L0 into no_div_zero_float. assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded). assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded). assert (0 <= Q2R err1)%R as err1_pos. { pose proof (err_always_positive e1 Gamma A); eauto. } assert (0 <= Q2R err2)%R as err2_pos. { pose proof (err_always_positive e2 Gamma A); eauto. } canonize_hyps. rename R1 into valid_error. repeat rewrite Q2R_plus in valid_error. repeat rewrite Q2R_mult in valid_error. rewrite Q2R_div in valid_error. - rewrite Q2R_mult in valid_error. repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error. rewrite <- maxAbs_impl_RmaxAbs_iv in valid_error. repeat rewrite <- minAbs_impl_RminAbs_iv in valid_error. apply le_neq_bool_to_lt_prop in no_div_zero_float; apply le_neq_bool_to_lt_prop in no_div_zero_real. assert ((IVhi (Q2R e2lo,Q2R e2hi) < 0)%R \/ (0 < IVlo (Q2R e2lo,Q2R e2hi))%R) as no_div_zero_real_R by (simpl; rewrite <- Q2R0_is_0; simpl in no_div_zero_real; destruct no_div_zero_real as [ndiv | ndiv]; apply Qlt_Rlt in ndiv; auto). apply Q_case_div_to_R_case_div in no_div_zero_float; apply Q_case_div_to_R_case_div in no_div_zero_real. assert (Q2R e2lo = 0 -> False)%R by (apply (lt_or_gt_neq_zero_lo _ (Q2R e2hi)); try auto; lra). assert (Q2R e2hi = 0 -> False)%R by (apply (lt_or_gt_neq_zero_hi (Q2R e2lo)); try auto; lra). eapply Rle_trans. Focus 2. apply valid_error. apply Rplus_le_compat. (* Error Propagation proof *) + clear A_e1 A_e2 valid_error eval_float eval_real e1_float e1_real e2_float e2_real A_div E1 E2 alo ahi nR nF e L. unfold widenInterval in *. simpl in *. rewrite Q2R_plus, Q2R_minus in no_div_zero_float. assert (Q2R e2lo - Q2R err2 = 0 -> False)%R by (apply (lt_or_gt_neq_zero_lo _ (Q2R e2hi + Q2R err2)); try auto; lra). assert (Q2R e2hi + Q2R err2 = 0 -> False)%R by (apply (lt_or_gt_neq_zero_hi (Q2R e2lo - Q2R err2)); try auto; lra). pose proof (interval_inversion_valid (Q2R e2lo,Q2R e2hi) no_div_zero_real_R valid_bounds_e2) as valid_bounds_inv_e2. clear no_div_zero_real_R. (* Before doing case distinction, prove bounds that will be used many times: *) assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R as upperBound_nR1 by (apply contained_leq_maxAbs_val; auto). assert (/ nR2 <= RmaxAbsFun (invertInterval (Q2R e2lo, Q2R e2hi)))%R as upperBound_nR2 by (apply contained_leq_maxAbs_val; auto). assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R as upperBound_Ropp_nR1 by (apply contained_leq_maxAbs_neg_val; auto). assert (- / nR2 <= RmaxAbsFun (invertInterval (Q2R e2lo, Q2R e2hi)))%R as upperBound_Ropp_nR2 by (apply contained_leq_maxAbs_neg_val; auto). assert (nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as bound_nR1 by (apply Rmult_le_compat_r; auto). assert (- nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as bound_neg_nR1 by (apply Rmult_le_compat_r; auto). unfold invertInterval in *; simpl in upperBound_nR2, upperBound_Ropp_nR2. (* Case distinction for the divisor range positive or negative in float and real valued execution *) destruct no_div_zero_real as [ real_iv_neg | real_iv_pos]; destruct no_div_zero_float as [float_iv_neg | float_iv_pos]. (* The range of the divisor lies in the range from -infinity until 0 *) * unfold widenIntv in *; simpl in *. rewrite <- Q2R_plus in float_iv_neg. rewrite <- Q2R0_is_0 in float_iv_neg. rewrite <- Q2R0_is_0 in real_iv_neg. pose proof (err_prop_inversion_neg float_iv_neg real_iv_neg err2_bounded valid_bounds_e2 H0 err2_pos) as err_prop_inv. rewrite Q2R_plus in float_iv_neg. rewrite Q2R0_is_0 in float_iv_neg. rewrite Q2R0_is_0 in real_iv_neg. rewrite Q2R_minus, Q2R_plus. repeat rewrite minAbs_negative_iv_is_hi; try lra. unfold Rdiv. repeat rewrite Q2R1. rewrite Rmult_1_l. (* Prove inequality to 0 in Q *) assert (e2lo == 0 -> False) by (rewrite <- Q2R0_is_0 in real_iv_neg; apply Rlt_Qlt in real_iv_neg; assert (e2lo < 0) by (apply (Qle_lt_trans _ e2hi); try auto; apply Rle_Qle; lra); lra). assert (e2hi == 0 -> False) by (rewrite <- Q2R0_is_0 in real_iv_neg; apply Rlt_Qlt in real_iv_neg; lra). rewrite Rabs_case_inverted in err1_bounded, err2_bounded. assert (nF1 <= Q2R err1 + nR1)%R as ub_nF1 by lra. assert (nR1 - Q2R err1 <= nF1)%R as lb_nF1 by lra. destruct err2_bounded as [[nR2_sub_pos err2_bounded] | [nR2_sub_neg err2_bounded]]. (* Positive case for abs (nR2 - nF2) <= err2 *) { rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, Ropp_involutive. apply Rgt_lt in nR2_sub_pos. assert (nF2 < nR2)%R as nF2_le_nR2 by lra. apply Ropp_lt_contravar in nF2_le_nR2. apply Rinv_lt_contravar in nF2_le_nR2; [ | apply Rmult_0_lt_preserving; try lra]. repeat (rewrite <- Ropp_inv_permute in nF2_le_nR2; try lra). apply Ropp_lt_contravar in nF2_le_nR2. repeat rewrite Ropp_involutive in nF2_le_nR2. assert (/ nR2 - / nF2 < 0)%R as abs_inv_neg by lra. rewrite Rabs_left in err_prop_inv; try lra. rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded, err_prop_inv. assert (/nF2 <= /nR2 + Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R as error_prop_inv_up by lra. assert (/nR2 - Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) <= /nF2)%R as error_prop_inv_down by lra. (* Next do a case distinction for the absolute value*) unfold Rabs. destruct Rcase_abs. (* Case 1: Absolute value negative *) - rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr. rewrite Ropp_involutive. (* To upper bound terms, do a case distinction for nF1 *) destruct (Rle_lt_dec 0 nF1). (* 0 <= nF1 *) + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; try lra. apply error_prop_inv_up. destruct (Rle_lt_dec 0 (/ nR2 + Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))). * eapply Rle_trans. eapply Rplus_le_compat_l. apply Rmult_le_compat_r; try lra. apply ub_nF1. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (Q2R err1 + nR1) * (/ nR2 + err_inv) = nR1 * err_inv + / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. apply Rmult_le_compat_neg_l; try lra. apply lb_nF1. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (/ nR2 + err_inv) * (nR1 - Q2R err1) = nR1 * err_inv - / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. repeat rewrite Rsub_eq_Ropp_Rplus. apply Rplus_le_compat. { apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. rewrite Ropp_mult_distr_l. apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_lt_0_inverting; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } (* nF1 < 0 *) + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l; try lra. apply error_prop_inv_down. destruct (Rle_lt_dec 0 (/ nR2 - Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))). * eapply Rle_trans. apply Rplus_le_compat_l. eapply Rmult_le_compat_r; try lra. apply ub_nF1. rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (Q2R err1 + nR1) * (/ nR2 - err_inv) = - nR1 * err_inv + / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_lt_0_inverting; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf; left; auto. apply lb_nF1. rewrite Rmult_comm. setoid_rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (- (/ nR2 * nR1) + (/ nR2 - err_inv) * (nR1 - Q2R err1) = - nR1 * err_inv + - / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } (* Case 2: Absolute value positive *) - rewrite Rsub_eq_Ropp_Rplus, Ropp_mult_distr_l. destruct (Rle_lt_dec 0 (- nF1)). (* 0 <= - nF1 *) + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; try lra. apply error_prop_inv_up. destruct (Rle_lt_dec 0 (/ nR2 + Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))). * eapply Rle_trans. eapply Rplus_le_compat_l. apply Rmult_le_compat_r; try lra. apply Ropp_le_contravar. apply lb_nF1. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + - (nR1 - Q2R err1) * (/ nR2 + err_inv) = - nR1 * err_inv + / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. apply Rmult_le_compat_neg_l; try lra. apply Ropp_le_contravar. apply ub_nF1. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + (/ nR2 + err_inv) * - (Q2R err1 + nR1) = - nR1 * err_inv + - / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. repeat rewrite Rsub_eq_Ropp_Rplus. apply Rplus_le_compat. { apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_lt_0_inverting; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } (* - nF1 <= 0 *) + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l; try lra. apply error_prop_inv_down. destruct (Rle_lt_dec 0 (/ nR2 - Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))). * eapply Rle_trans. apply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_l; try lra. apply Ropp_le_contravar. apply lb_nF1. rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + (/ nR2 - err_inv) * - (nR1 - Q2R err1) = nR1 * err_inv + / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_lt_0_inverting; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf; left; auto. apply Ropp_le_contravar. apply ub_nF1. setoid_rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + (/ nR2 - err_inv) * - (Q2R err1 + nR1) = nR1 * err_inv + - / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } } { rewrite <- Ropp_mult_distr_l, <- Ropp_mult_distr_r, Ropp_involutive. assert (nR2 <= nF2)%R as nR2_le_nF2 by lra. apply Ropp_le_contravar in nR2_le_nF2. apply Rinv_le_contravar in nR2_le_nF2; [ | lra]. repeat (rewrite <- Ropp_inv_permute in nR2_le_nF2; try lra). apply Ropp_le_contravar in nR2_le_nF2. repeat rewrite Ropp_involutive in nR2_le_nF2. assert (0 <= / nR2 - / nF2)%R as abs_inv_pos by lra. rewrite Rabs_right in err_prop_inv; try lra. rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded, err_prop_inv. assert (/nF2 <= /nR2 + Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R as error_prop_inv_up by lra. assert (/nR2 - Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) <= /nF2)%R as error_prop_inv_down by lra. (* Next do a case distinction for the absolute value*) unfold Rabs. destruct Rcase_abs. - rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr. rewrite Ropp_involutive. (* To upper bound terms, do a case distinction for nF1 *) destruct (Rle_lt_dec 0 nF1). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; try lra. apply error_prop_inv_up. destruct (Rle_lt_dec 0 (/ nR2 + Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))). * eapply Rle_trans. eapply Rplus_le_compat_l. apply Rmult_le_compat_r; try lra. apply ub_nF1. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (Q2R err1 + nR1) * (/ nR2 + err_inv) = nR1 * err_inv + / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. apply Rmult_le_compat_neg_l; try lra. apply lb_nF1. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (/ nR2 + err_inv) * (nR1 - Q2R err1) = nR1 * err_inv - / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. repeat rewrite Rsub_eq_Ropp_Rplus. apply Rplus_le_compat. { apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. rewrite Ropp_mult_distr_l. apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_lt_0_inverting; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l; try lra. apply error_prop_inv_down. destruct (Rle_lt_dec 0 (/ nR2 - Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))). * eapply Rle_trans. apply Rplus_le_compat_l. eapply Rmult_le_compat_r; try lra. apply ub_nF1. rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (Q2R err1 + nR1) * (/ nR2 - err_inv) = - nR1 * err_inv + / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_lt_0_inverting; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf; left; auto. apply lb_nF1. rewrite Rmult_comm. setoid_rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (- (/ nR2 * nR1) + (/ nR2 - err_inv) * (nR1 - Q2R err1) = - nR1 * err_inv + - / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } - rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_mult_distr_l. destruct (Rle_lt_dec 0 (- nF1)). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; try lra. apply error_prop_inv_up. destruct (Rle_lt_dec 0 (/ nR2 + Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))). * eapply Rle_trans. eapply Rplus_le_compat_l. apply Rmult_le_compat_r; try lra. apply Ropp_le_contravar. apply lb_nF1. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + - (nR1 - Q2R err1) * (/ nR2 + err_inv) = - nR1 * err_inv + / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. apply Rmult_le_compat_neg_l; try lra. apply Ropp_le_contravar. apply ub_nF1. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + (/ nR2 + err_inv) * - (Q2R err1 + nR1) = - nR1 * err_inv + - / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. repeat rewrite Rsub_eq_Ropp_Rplus. apply Rplus_le_compat. { apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_lt_0_inverting; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l; try lra. apply error_prop_inv_down. destruct (Rle_lt_dec 0 (/ nR2 - Q2R err2 * / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))). * eapply Rle_trans. apply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_l; try lra. apply Ropp_le_contravar. apply lb_nF1. rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + (/ nR2 - err_inv) * - (nR1 - Q2R err1) = nR1 * err_inv + / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_lt_0_inverting; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf; left; auto. apply Ropp_le_contravar. apply ub_nF1. setoid_rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2hi + Q2R err2) * (Q2R e2hi + Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + (/ nR2 - err_inv) * - (Q2R err1 + nR1) = nR1 * err_inv + - / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } } * unfold widenIntv in *; simpl in *. exfalso. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi)%R by lra. assert (Q2R e2hi < Q2R e2lo - Q2R err2)%R by (apply (Rlt_trans _ 0 _); auto). lra. * unfold widenIntv in *; simpl in *. exfalso. assert (Q2R e2lo <= Q2R e2hi + Q2R err2)%R by lra. assert (Q2R e2hi + Q2R err2 < Q2R e2lo)%R as hierr_lt_lo by (apply (Rlt_trans _ 0 _); auto). apply Rlt_not_le in hierr_lt_lo. apply hierr_lt_lo; auto. * (** FIXME: Get rid of rewrites by fixing Lemma **) rewrite <- Q2R_minus in float_iv_pos. rewrite <- Q2R0_is_0 in float_iv_pos. rewrite <- Q2R0_is_0 in real_iv_pos. pose proof (err_prop_inversion_pos float_iv_pos real_iv_pos err2_bounded valid_bounds_e2 H0 err2_pos) as err_prop_inv. rewrite Q2R_minus in float_iv_pos. rewrite Q2R0_is_0 in float_iv_pos. rewrite Q2R0_is_0 in real_iv_pos. rewrite Q2R_minus, Q2R_plus. repeat rewrite minAbs_positive_iv_is_lo; try lra. unfold Rdiv. repeat rewrite Q2R1. rewrite Rmult_1_l. (* Prove inequality to 0 in Q *) assert (e2lo == 0 -> False) by (rewrite <- Q2R0_is_0 in real_iv_pos; apply Rlt_Qlt in real_iv_pos; lra). assert (e2hi == 0 -> False) by (rewrite <- Q2R0_is_0 in real_iv_pos; apply Rlt_Qlt in real_iv_pos; assert (0 < e2hi) by (apply (Qlt_le_trans _ e2lo); try auto; apply Rle_Qle; lra); lra). rewrite Rabs_case_inverted in err1_bounded, err2_bounded. assert (nF1 <= Q2R err1 + nR1)%R as ub_nF1 by lra. assert (nR1 - Q2R err1 <= nF1)%R as lb_nF1 by lra. destruct err2_bounded as [[nR2_sub_pos err2_bounded] | [nR2_sub_neg err2_bounded]]. { apply Rgt_lt in nR2_sub_pos. assert (nF2 < nR2)%R as nF2_le_nR2 by lra. apply Rinv_lt_contravar in nF2_le_nR2; [ | apply Rmult_0_lt_preserving; try lra]. assert (/ nR2 - / nF2 <= 0)%R as abs_inv_neg by lra. rewrite Rabs_left in err_prop_inv; try lra. rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. assert (/nR2 - Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) <= /nF2)%R as error_prop_inv_down by lra. assert (/nF2 <= /nR2 + Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))%R as error_prop_inv_up by lra. (* Next do a case distinction for the absolute value*) unfold Rabs. destruct Rcase_abs. - rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr. rewrite Ropp_involutive. (* To upper bound terms, do a case distinction for nF1 *) destruct (Rle_lt_dec 0 nF1). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat; try lra. hnf. left. apply Rinv_0_lt_compat; try lra. apply ub_nF1. apply error_prop_inv_up. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (Q2R err1 + nR1) * (/ nR2 + err_inv) = nR1 * err_inv + / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. apply Rmult_le_compat; try lra. * hnf; left. apply Rinv_0_lt_compat; lra. * repeat (rewrite Q2R_inv; try auto). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l; try lra. apply error_prop_inv_down. destruct (Rle_lt_dec 0 (/ nR2 - Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))). * eapply Rle_trans. apply Rplus_le_compat_l. eapply Rmult_le_compat_r; try lra. apply ub_nF1. rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (Q2R err1 + nR1) * (/ nR2 - err_inv) = - nR1 * err_inv + / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_0_lt_preserving; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf; left; auto. apply lb_nF1. rewrite Rmult_comm. setoid_rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (- (/ nR2 * nR1) + (/ nR2 - err_inv) * (nR1 - Q2R err1) = - nR1 * err_inv + - / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } - rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_mult_distr_l. destruct (Rle_lt_dec 0 (- nF1)). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat; try lra. hnf; left. apply Rinv_0_lt_compat. apply (Rlt_le_trans _ (Q2R e2lo - Q2R err2)); try lra. apply Ropp_le_contravar. apply lb_nF1. apply error_prop_inv_up. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert ((nR1 * / nR2) + - (nR1 - Q2R err1) * (/ nR2 + err_inv) = - nR1 * err_inv + / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. * apply Rmult_le_compat_r; try lra. * apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l; try lra. apply error_prop_inv_down. destruct (Rle_lt_dec 0 (/ nR2 - Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))). * eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; try lra. apply Ropp_le_contravar. apply lb_nF1. rewrite Rmult_comm. setoid_rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (/ nR2 * nR1 + - (nR1 - Q2R err1) * (/ nR2 - err_inv) = nR1 * err_inv + / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_0_lt_preserving; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf; left; auto. apply Ropp_le_contravar. apply ub_nF1. rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + (/ nR2 - err_inv) * - (Q2R err1 + nR1) = nR1 * err_inv + - / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } } { apply Rminus_le in nR2_sub_neg. apply Rinv_le_contravar in nR2_sub_neg; [ | lra]. assert (0 <= / nR2 - / nF2)%R as abs_inv_pos by lra. rewrite Rabs_right in err_prop_inv; try lra. rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. rewrite Ropp_plus_distr in err2_bounded. rewrite Ropp_involutive in err2_bounded. assert (/nR2 - Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) <= /nF2)%R as error_prop_inv_down by lra. assert (/nF2 <= /nR2 + Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))%R as error_prop_inv_up by lra. (* Next do a case distinction for the absolute value*) unfold Rabs. destruct Rcase_abs. - rewrite Rsub_eq_Ropp_Rplus, Ropp_plus_distr. rewrite Ropp_involutive. (* To upper bound terms, do a case distinction for nF1 *) destruct (Rle_lt_dec 0 nF1). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat; try lra. hnf. left. apply Rinv_0_lt_compat; try lra. apply ub_nF1. apply error_prop_inv_up. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (Q2R err1 + nR1) * (/ nR2 + err_inv) = nR1 * err_inv + / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat; [ apply Rmult_le_compat_r; lra | ]. apply Rmult_le_compat; try lra. * hnf; left. apply Rinv_0_lt_compat; lra. * repeat (rewrite Q2R_inv; try auto). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l; try lra. apply error_prop_inv_down. destruct (Rle_lt_dec 0 (/ nR2 - Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))). * eapply Rle_trans. apply Rplus_le_compat_l. eapply Rmult_le_compat_r; try lra. apply ub_nF1. rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (- (nR1 * / nR2) + (Q2R err1 + nR1) * (/ nR2 - err_inv) = - nR1 * err_inv + / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_0_lt_preserving; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf; left; auto. apply lb_nF1. rewrite Rmult_comm. setoid_rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (- (/ nR2 * nR1) + (/ nR2 - err_inv) * (nR1 - Q2R err1) = - nR1 * err_inv + - / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } - rewrite Rsub_eq_Ropp_Rplus. rewrite Ropp_mult_distr_l. destruct (Rle_lt_dec 0 (- nF1)). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat; try lra. hnf; left. apply Rinv_0_lt_compat. apply (Rlt_le_trans _ (Q2R e2lo - Q2R err2)); try lra. apply Ropp_le_contravar. apply lb_nF1. apply error_prop_inv_up. rewrite (Rmult_comm (Q2R err2) _). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert ((nR1 * / nR2) + - (nR1 - Q2R err1) * (/ nR2 + err_inv) = - nR1 * err_inv + / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. * apply Rmult_le_compat_r; try lra. * apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). + eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_neg_l; try lra. apply error_prop_inv_down. destruct (Rle_lt_dec 0 (/ nR2 - Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))). * eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; try lra. apply Ropp_le_contravar. apply lb_nF1. rewrite Rmult_comm. setoid_rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (/ nR2 * nR1 + - (nR1 - Q2R err1) * (/ nR2 - err_inv) = nR1 * err_inv + / nR2 * Q2R err1 - Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } { assert (0 <= err_inv)%R. - subst. assert (0 < / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)))%R by (apply Rinv_0_lt_compat; apply Rmult_0_lt_preserving; try lra). lra. - assert (0 <= (Q2R err1 * err_inv))%R by (rewrite <- (Rmult_0_l 0); apply Rmult_le_compat; lra). apply (Rle_trans _ 0); lra. } * eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf; left; auto. apply Ropp_le_contravar. apply ub_nF1. rewrite (Rmult_comm (Q2R err2)). remember (/ ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) * Q2R err2)%R as err_inv. assert (nR1 * / nR2 + (/ nR2 - err_inv) * - (Q2R err1 + nR1) = nR1 * err_inv + - / nR2 * Q2R err1 + Q2R err1 * err_inv)%R as simpl_properr by lra. rewrite simpl_properr. apply Rplus_le_compat_r. apply Rplus_le_compat. { apply Rmult_le_compat_r; try lra. } { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } } + assert (IVhi (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)) < 0 \/ 0 < IVlo (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)))%R as no_div_zero_widen by (unfold widenInterval in *; simpl in *; rewrite Q2R_plus, Q2R_minus in no_div_zero_float; auto). pose proof (IntervalArith.interval_division_valid _ _ no_div_zero_widen H H0) as valid_div_float. unfold widenInterval in *; simpl in *. assert (e2lo - err2 == 0 -> False). * hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; rewrite <- Q2R0_is_0 in float_iv; apply Rlt_Qlt in float_iv; try lra. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra. rewrite<- Q2R_minus, <- Q2R_plus in H4. apply Rle_Qle in H4. lra. * assert (e2hi + err2 == 0 -> False). { hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; rewrite <- Q2R0_is_0 in float_iv; apply Rlt_Qlt in float_iv; try lra. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra. rewrite<- Q2R_minus, <- Q2R_plus in H5. apply Rle_Qle in H5. lra. } { destruct valid_div_float. rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv. apply computeErrorR_up. apply contained_leq_maxAbs. simpl in *; split. - rewrite Q2R_min4. repeat rewrite Q2R_mult. repeat (rewrite Q2R_inv; auto). repeat rewrite Q2R_minus, Q2R_plus; auto. - rewrite Q2R_max4. repeat rewrite Q2R_mult. repeat (rewrite Q2R_inv; auto). repeat rewrite Q2R_minus. repeat rewrite Q2R_plus; auto. } - apply le_neq_bool_to_lt_prop in no_div_zero_float. unfold widenInterval in *; simpl in *. assert (e2lo - err2 == 0 -> False). + hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; try lra. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra. rewrite<- Q2R_minus, <- Q2R_plus in H2. apply Rle_Qle in H2. lra. + assert (e2hi + err2 == 0 -> False). * hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; try lra. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra. rewrite<- Q2R_minus, <- Q2R_plus in H3. apply Rle_Qle in H3. lra. * unfold widenIntv; simpl. hnf. intros. assert (forall a, Qabs a == 0 -> a == 0). { intros. unfold Qabs in H4. destruct a. rewrite <- Z.abs_0 in H4. inversion H4. rewrite Zmult_1_r in *. rewrite Z.abs_0_iff in H6. rewrite H6. rewrite Z.abs_0. hnf. simpl; auto. } { assert (minAbs (e2lo - err2, e2hi + err2) == 0 -> False). - unfold minAbs. unfold fst, snd. apply Q.min_case_strong. + intros. apply H6; rewrite H5; auto. + intros. apply H1. rewrite (H4 (e2lo-err2) H6). hnf. auto. + intros. apply H2. rewrite H4; auto. hnf; auto. - rewrite <- (Qmult_0_l (minAbs (e2lo - err2, e2hi + err2))) in H3. rewrite (Qmult_inj_r) in H3; auto. } Qed. Lemma validErrorboundCorrectFma E1 E2 A (e1:expr Q) (e2:expr Q) (e3: expr Q) (nR nR1 nR2 nR3 nF nF1 nF2 nF3: R) (e err1 err2 err3 :error) (alo ahi e1lo e1hi e2lo e2hi e3lo e3hi:Q) dVars (m m1 m2 m3:mType) Gamma defVars: m = join3 m1 m2 m3 -> eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) nR3 REAL -> eval_expr E1 (toRMap defVars) (toREval (toRExp (Fma e1 e2 e3))) nR REAL -> eval_expr E2 defVars (toRExp e1) nF1 m1 -> eval_expr E2 defVars (toRExp e2) nF2 m2 -> eval_expr E2 defVars (toRExp e3) nF3 m3 -> eval_expr (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))) (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars))) (toRExp (Fma (Var Q 1) (Var Q 2) (Var Q 3))) nF m -> typeCheck (Fma e1 e2 e3) defVars Gamma = true -> validErrorbound (Fma e1 e2 e3) Gamma A dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> (Q2R e3lo <= nR3 <= Q2R e3hi)%R -> FloverMap.find e1 A = Some ((e1lo,e1hi),err1) -> FloverMap.find e2 A = Some ((e2lo, e2hi),err2) -> FloverMap.find e3 A = Some ((e3lo, e3hi),err3) -> FloverMap.find (Fma e1 e2 e3) A = Some ((alo,ahi),e)-> (Rabs (nR1 - nF1) <= (Q2R err1))%R -> (Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR3 - nF3) <= (Q2R err3))%R -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. intros mIsJoin e1_real e2_real e3_real eval_real e1_float e2_float e3_float eval_float subexprr_ok valid_error valid_e1 valid_e2 valid_e3 A_e1 A_e2 A_e3 A_fma err1_bounded err2_bounded err3_bounded. cbn in *; Flover_compute; type_conv; subst. eapply Rle_trans. eapply (fma_abs_err_bounded e1 e2 e3); eauto. pose proof (typingSoundnessExp _ _ R4 e1_float). pose proof (typingSoundnessExp _ _ R3 e2_float). pose proof (typingSoundnessExp _ _ R2 e3_float). rewrite H in Heqo0; rewrite H0 in Heqo1; rewrite H1 in Heqo2; inversion Heqo0; inversion Heqo1; inversion Heqo2; subst. rename R0 into valid_error. assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma A dVars); eauto). assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma A dVars); eauto). assert (0 <= Q2R err3)%R as err3_pos by (eapply (err_always_positive e3 Gamma A dVars); eauto). apply Qle_bool_iff in valid_error. apply Qle_Rle in valid_error. repeat rewrite Q2R_plus in valid_error. repeat rewrite Q2R_mult in valid_error. repeat rewrite Q2R_plus in valid_error. repeat rewrite <- Rabs_eq_Qabs in valid_error. repeat rewrite Q2R_plus in valid_error. repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error. eapply Rle_trans; eauto. apply Rplus_le_compat. - eauto using Rle_trans, Rabs_triang, Rplus_le_compat, multiplicationErrorBounded. - assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded) as valid_err1. assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded) as valid_err2. assert (contained nR3 (Q2R e3lo, Q2R e3hi)) as contained_intv3 by auto. pose proof (distance_gives_iv (a:=nR3) _ _ contained_intv3 err3_bounded) as valid_err3. pose proof (IntervalArith.interval_multiplication_valid _ _ valid_err2 valid_err3) as valid_err_mult. pose proof (IntervalArith.interval_addition_valid _ _ valid_err1 valid_err_mult). rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv. apply computeErrorR_up. apply contained_leq_maxAbs. simpl in *; split. + rewrite Q2R_min4. repeat rewrite Q2R_mult; repeat rewrite Q2R_minus; repeat rewrite Q2R_plus; repeat rewrite Q2R_minus. rewrite Q2R_max4. rewrite Q2R_min4. repeat rewrite Q2R_mult; repeat rewrite Q2R_minus; repeat rewrite Q2R_plus; repeat rewrite Q2R_minus. lra. + rewrite Q2R_max4. repeat rewrite Q2R_mult; repeat rewrite Q2R_minus; repeat rewrite Q2R_plus; repeat rewrite Q2R_minus. rewrite Q2R_max4. rewrite Q2R_min4. repeat rewrite Q2R_mult; repeat rewrite Q2R_minus; repeat rewrite Q2R_plus; repeat rewrite Q2R_minus. lra. Qed. Lemma validErrorboundCorrectRounding E1 E2 A (e: expr Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars: eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL -> eval_expr E2 defVars (toRExp e) nF1 m -> eval_expr (updEnv 1 nF1 emptyEnv) (updDefVars 1 m defVars) (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon -> typeCheck (Downcast machineEpsilon e) defVars Gamma = true -> validErrorbound (Downcast machineEpsilon e) Gamma A dVars = true -> (Q2R elo <= nR <= Q2R ehi)%R -> FloverMap.find e A = Some ((elo, ehi), err) -> FloverMap.find (Downcast machineEpsilon e) A = Some ((alo, ahi), err') -> (Rabs (nR - nF1) <= (Q2R err))%R -> (Rabs (nR - nF) <= (Q2R err'))%R. Proof. intros eval_real eval_float eval_float_rnd subexprr_ok valid_error valid_intv A_e A_rnd err_bounded. cbn in *; Flover_compute; type_conv; subst. eapply Rle_trans. eapply round_abs_err_bounded; eauto. assert (contained nR (Q2R elo, Q2R ehi)) as valid_intv_c by (auto). pose proof (distance_gives_iv _ _ valid_intv_c err_bounded) as dgi. destruct dgi as [dgi1 dgi2]; simpl in dgi1, dgi2. canonize_hyps. eapply Rle_trans; eauto. rewrite Q2R_plus. apply Rplus_le_compat_l. rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv. apply computeErrorR_up. apply contained_leq_maxAbs. simpl in *; split; try rewrite Q2R_plus in *; try rewrite Q2R_minus in *; lra. Qed. (** Soundness theorem for the error bound validator. Proof is by induction on the exprression e. Each case requires the application of one of the soundness lemmata proven before **) Theorem validErrorbound_sound (e:expr Q): forall E1 E2 fVars dVars A nR err P elo ehi Gamma defVars, typeCheck e defVars Gamma = true -> approxEnv E1 defVars A fVars dVars E2 -> NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars -> eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL -> validErrorbound e Gamma A dVars = true -> validIntervalbounds e A P dVars = true -> dVars_range_valid dVars E1 A -> fVars_P_sound fVars E1 P -> vars_typed (NatSet.union fVars dVars) defVars -> FloverMap.find e A = Some ((elo,ehi),err) -> (exists nF m, eval_expr E2 defVars (toRExp e) nF m) /\ (forall nF m, eval_expr E2 defVars (toRExp e) nF m -> (Rabs (nR - nF) <= (Q2R err))%R). Proof. revert e; induction e; intros * typing_ok approxCEnv fVars_subset eval_real valid_error valid_intv valid_dVars P_valid vars_wellTyped A_eq. - split. + eapply validErrorboundCorrectVariable_eval; eauto. + intros * eval_float. eapply validErrorboundCorrectVariable; eauto. - edestruct validIntervalbounds_sound as [? [ ? [? [? [? ?]]]]]; eauto. rewrite H in A_eq; inversion A_eq; subst. rewrite (meps_0_deterministic _ eval_real H0) in *; auto. split. + eapply validErrorboundCorrectConstant_eval; eauto. + intros * eval_float. eapply validErrorboundCorrectConstant; eauto. pose proof (typingSoundnessExp _ _ typing_ok eval_float). cbn in *; Flover_compute; type_conv; eauto. - simpl in *. rewrite A_eq in valid_error. cbn in *; Flover_compute; try congruence; type_conv; subst. destruct u; try congruence. inversion eval_real; subst. rewrite <- andb_lazy_alt in R0; Flover_compute. destruct (IHe E1 E2 fVars dVars A v1 e1 P (fst i0) (snd i0) Gamma defVars) as [[nF [mF eval_float]] valid_bounds_e]; eauto. + destruct i0; auto. + split. * exists (evalUnop Neg nF); exists mF. simpl; eauto. * intros * eval_float_op. inversion eval_float_op; subst; simpl. apply bound_flip_sub. canonize_hyps. rewrite R; eapply valid_bounds_e; eauto. - cbn in *. rewrite A_eq in *. Flover_compute; try congruence; type_conv; subst; simpl in *. inversion eval_real; subst. assert (m0 = REAL /\ m3 = REAL) as [? ?] by (split; eapply toRMap_eval_REAL; eauto); subst. destruct i as [ivlo1 ivhi1]; destruct i1 as [ivlo2 ivhi2]; rename e into err1; rename e3 into err2. destruct (IHe1 E1 E2 fVars dVars A v1 err1 P ivlo1 ivhi1 Gamma defVars) as [[vF1 [mF1 eval_float_e1]] bounded_e1]; try auto; set_tac. destruct (IHe2 E1 E2 fVars dVars A v2 err2 P ivlo2 ivhi2 Gamma defVars) as [[vF2 [mF2 eval_float_e2]] bounded_e2]; try auto; set_tac. destruct (validIntervalbounds_sound _ (E:=E1) (Gamma:=defVars) L0 (fVars := fVars) (dVars:=dVars)) as [iv1' [ err1' [v1' [map_e1 [eval_real_e1 bounds_e1]]]]]; try auto; set_tac. inversion Heqo3; rewrite map_e1 in Heqo; inversion Heqo; subst. pose proof (meps_0_deterministic _ eval_real_e1 H5); subst. clear H5. destruct (validIntervalbounds_sound _ (E:=E1) (Gamma:=defVars) R0 (fVars:= fVars) (dVars:=dVars)) as [iv2' [err2' [v2' [map_e2 [eval_real_e2 bounds_e2]]]]]; try auto; set_tac. rewrite map_e2 in Heqo2; inversion Heqo2; subst. pose proof (meps_0_deterministic _ eval_real_e2 H6); subst; clear H6. assert (b = Div -> ~ (vF2 = 0)%R) as no_div_zero. { intros; subst; simpl in *. andb_to_prop R2. apply le_neq_bool_to_lt_prop in L1. assert (contained vF1 (widenInterval (Q2R ivlo1, Q2R ivhi1) (Q2R err1))) as bounds_float_e1. { eapply distance_gives_iv; simpl; try eauto. } assert (contained vF2 (widenInterval (Q2R ivlo2, Q2R ivhi2) (Q2R err2))) as bounds_float_e2. { eapply distance_gives_iv; simpl; try eauto. } simpl in *. canonize_hyps. intro; subst. rewrite <- Q2R0_is_0 in bounds_float_e2. destruct L1 as [nodivzero | nodivzero]; apply Qlt_Rlt in nodivzero; try rewrite Q2R_plus in *; try rewrite Q2R_minus in *; lra. } split. + repeat eexists; econstructor; eauto. instantiate (1 := 0%R). rewrite Rabs_R0. apply mTypeToR_pos_R. + intros * eval_float. clear eval_float_e1 eval_float_e2. inversion eval_float; subst. eapply (binary_unfolding _ H10 H4 H5 H9) in eval_float; try auto. inversion Heqo1; subst. destruct b. * eapply (validErrorboundCorrectAddition (e1:=e1) A); eauto. { cbn. instantiate (1:=Gamma). Flover_compute. rewrite mTypeEq_refl, R3, R4; auto. } { cbn. instantiate (1:=dVars); Flover_compute. rewrite L, L2, R1; simpl; auto. } * eapply (validErrorboundCorrectSubtraction (e1:=e1) A); eauto. { cbn; instantiate (1:=Gamma); Flover_compute; auto. rewrite mTypeEq_refl, R3, R4; auto. } { cbn; instantiate (1:=dVars); Flover_compute. rewrite L, L2, R1; simpl; auto. } * eapply (validErrorboundCorrectMult (e1 := e1) A); eauto. { cbn; instantiate (1:=Gamma); Flover_compute; auto. rewrite mTypeEq_refl, R3, R4; auto. } { cbn; instantiate (1:=dVars); Flover_compute. rewrite L, L2, R1; simpl; auto. } * eapply (validErrorboundCorrectDiv (e1 := e1) A); eauto. { cbn; instantiate (1:=Gamma); Flover_compute; auto. rewrite mTypeEq_refl, R3, R4; auto. } { cbn; instantiate (1:=dVars); Flover_compute. rewrite L, L2,L4, R1; simpl; auto. } { andb_to_prop R; auto. } (*- simpl in valid_error. destruct (absenv e1) as [[ivlo1 ivhi1] err1] eqn:absenv_e1; destruct (absenv e2) as [[ivlo2 ivhi2] err2] eqn:absenv_e2; destruct (absenv e3) as [[ivlo3 ivhi3] err3] eqn:absenv_e3. subst; simpl in *. rewrite absenv_eq, absenv_e1, absenv_e2, absenv_e3 in *. case_eq (Gamma (Fma e1 e2 e3)); intros * type_fma; rewrite type_fma in *; [ | inversion valid_error ]. case_eq (Gamma e1); intros * type_e1; rewrite type_e1 in typing_ok; [ | inversion typing_ok ]. case_eq (Gamma e2); intros * type_e2; rewrite type_e2 in typing_ok; [ | inversion typing_ok ]. case_eq (Gamma e3); intros * type_e3; rewrite type_e3 in typing_ok; [ | inversion typing_ok ]. repeat match goal with | [H: _ = true |- _] => andb_to_prop H end. type_conv.*) - cbn in *. rewrite A_eq in *. Flover_compute; try congruence; type_conv; subst; simpl in *. inversion eval_real; subst. assert (m0 = REAL /\ m4 = REAL /\ m5 = REAL) as [? [? ?]] by (split; try split; eapply toRMap_eval_REAL; eauto); subst. destruct i as [ivlo1 ivhi1]; destruct i2 as [ivlo2 ivhi2]; destruct i1 as [ivlo3 ivhi3]; rename e into err1; rename e5 into err2; rename e4 into err3. destruct (IHe1 E1 E2 fVars dVars A v1 err1 P ivlo1 ivhi1 Gamma defVars) as [[vF1 [mF1 eval_float_e1]] bounded_e1]; try auto; set_tac. destruct (IHe2 E1 E2 fVars dVars A v2 err2 P ivlo2 ivhi2 Gamma defVars) as [[vF2 [mF2 eval_float_e2]] bounded_e2]; try auto; set_tac. destruct (IHe3 E1 E2 fVars dVars A v3 err3 P ivlo3 ivhi3 Gamma defVars) as [[vF3 [mF3 eval_float_e3]] bounded_e3]; try auto; set_tac. destruct (validIntervalbounds_sound _ (E:=E1) (Gamma:=defVars) L (fVars := fVars) (dVars:=dVars)) as [iv1' [ err1' [v1' [map_e1 [eval_real_e1 bounds_e1]]]]]; try auto; set_tac. rewrite map_e1 in Heqo; inversion Heqo; subst. pose proof (meps_0_deterministic _ eval_real_e1 H5); subst; clear H5. destruct (validIntervalbounds_sound _ (E:=E1) (Gamma:=defVars) R1 (fVars:= fVars) (dVars:=dVars)) as [iv2' [err2' [v2' [map_e2 [eval_real_e2 bounds_e2]]]]]; try auto; set_tac. rewrite map_e2 in Heqo2; inversion Heqo2; subst. pose proof (meps_0_deterministic _ eval_real_e2 H6); subst; clear H6. destruct (validIntervalbounds_sound _ (E:=E1) (Gamma:=defVars) R0 (fVars:= fVars) (dVars:=dVars)) as [iv3' [err3' [v3' [map_e3 [eval_real_e3 bounds_e3]]]]]; try auto; set_tac. rewrite map_e3 in Heqo5; inversion Heqo5; subst. pose proof (meps_0_deterministic _ eval_real_e3 H7); subst; clear H7. split. + repeat eexists; econstructor; eauto. rewrite Rabs_right; try lra. instantiate (1 := 0%R). apply mTypeToR_pos_R. apply Rle_ge. hnf; right; reflexivity. + intros * eval_float. clear eval_float_e1 eval_float_e2 eval_float_e3. inversion eval_float; subst. eapply (fma_unfolding _ H4 H5 H8 H9) in eval_float; try auto. eapply (validErrorboundCorrectFma (e1:=e1) (e2:=e2) (e3:=e3) A); eauto. { simpl. rewrite Heqo0. rewrite Heqo4. rewrite Heqo6. rewrite Heqo7. rewrite mTypeEq_refl, R5, R6, R7; auto. } { simpl. rewrite A_eq. rewrite Heqo0. rewrite R, L1, L2, R4; simpl. rewrite map_e1, map_e2, map_e3. inversion Heqo1. rewrite <- H0. auto. } - cbn in *; Flover_compute; try congruence; type_conv; subst. inversion eval_real; subst. apply REAL_least_precision in H1. subst. destruct i0 as [ivlo_e ivhi_e]; rename e1 into err_e. destruct (IHe E1 E2 fVars dVars A v1 err_e P ivlo_e ivhi_e Gamma defVars) as [[vF [mF eval_float_e]] bounded_e]; try auto; set_tac. pose proof (typingSoundnessExp _ _ R0 eval_float_e). rewrite H in Heqo2; inversion Heqo2; subst. destruct (validIntervalbounds_sound _ (E:=E1) (Gamma:=defVars) L (fVars := fVars) (dVars:=dVars)) as [iv1' [err1' [v1' [map_e [eval_real_e bounds_e]]]]]; try auto; set_tac. rewrite map_e in Heqo0; inversion Heqo0; subst. pose proof (meps_0_deterministic _ eval_real_e H4); subst. clear H4. split. + eexists; eexists. eapply Downcast_dist'; eauto. * rewrite isMorePrecise_morePrecise; auto. * instantiate (1 := 0%R); rewrite Rabs_R0; auto using mTypeToR_pos_R. + intros * eval_float. inversion eval_float; subst. eapply validErrorboundCorrectRounding; eauto. * simpl. eapply Downcast_dist'; eauto. constructor. unfold updDefVars. rewrite Nat.eqb_refl; auto. unfold updEnv; simpl; auto. * cbn; instantiate (1:=Gamma); Flover_compute. rewrite mTypeEq_refl, R3, R0; eauto. * cbn; instantiate (1:=dVars); Flover_compute. rewrite L2, L3; auto. Qed. Theorem validErrorboundCmd_gives_eval (f:cmd Q) : forall (A:analysisResult) E1 E2 outVars fVars dVars vR elo ehi err P Gamma defVars, typeCheckCmd f defVars Gamma = true -> approxEnv E1 defVars A fVars dVars E2 -> ssa f (NatSet.union fVars dVars) outVars -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL -> validErrorboundCmd f Gamma A dVars = true -> validIntervalboundsCmd f A P dVars = true -> dVars_range_valid dVars E1 A -> fVars_P_sound fVars E1 P -> vars_typed (NatSet.union fVars dVars) defVars -> FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) -> (exists vF m, bstep (toRCmd f) E2 defVars vF m). Proof. induction f; intros * type_f approxc1c2 ssa_f freeVars_subset eval_real valid_bounds valid_intv fVars_sound P_valid types_defined A_res; cbn in *; Flover_compute; try congruence; type_conv; subst. - (* let-binding *) inversion eval_real; subst. inversion ssa_f; subst. simpl in freeVars_subset. assert (NatSet.Subset (usedVars e -- dVars) fVars) as valid_varset. { set_tac. split; try auto. split; try set_tac. hnf; intros; subst; set_tac. } destruct i as [ivlo_e ivhi_e]; rename e2 into err_e. match goal with | [H : validErrorbound _ _ _ _ = true |- _] => eapply validErrorbound_sound with (err := err_e) (elo := ivlo_e) (ehi:= ivhi_e) in H; eauto; destruct H as [[vF [ mF eval_float_e]] bounded_e] end. canonize_hyps. assert (approxEnv (updEnv n v E1) (updDefVars n mF defVars) A fVars (NatSet.add n dVars) (updEnv n vF E2)). + eapply approxUpdBound; try eauto. simpl in *. apply Rle_trans with (r2:= Q2R err_e); try lra. eapply bounded_e; eauto. + rename R2 into valid_rec. rewrite (typingSoundnessExp _ _ L0 eval_float_e) in *; simpl in *. inversion Heqo1; subst. destruct (IHf A (updEnv n v E1) (updEnv n vF E2) outVars fVars (NatSet.add n dVars) vR elo ehi err P Gamma (updDefVars n m1 defVars)) as [vF_res [m_res step_res]]; eauto. { eapply ssa_equal_set; eauto. hnf. intros a; split; intros in_set. - rewrite NatSet.add_spec, NatSet.union_spec; rewrite NatSet.union_spec, NatSet.add_spec in in_set. destruct in_set as [P1 | [ P2 | P3]]; auto. - rewrite NatSet.add_spec, NatSet.union_spec in in_set; rewrite NatSet.union_spec, NatSet.add_spec. destruct in_set as [P1 | [ P2 | P3]]; auto. } { hnf. intros a in_diff. rewrite NatSet.diff_spec, NatSet.add_spec in in_diff. destruct in_diff as [ in_freeVars no_dVar]. apply freeVars_subset. simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. split; try auto. } { eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars)); eauto using Rmap_updVars_comm. } { intros v1 v1_mem. unfold updEnv. case_eq (v1 =? n); intros v1_eq. - apply Nat.eqb_eq in v1_eq; subst. exists v, (q1, q2), e1; split; try auto; split; try auto; simpl. destruct (validIntervalbounds_sound e (E:=E1) (Gamma:=defVars) L (fVars:=fVars)) as [iv_e' [ err_e' [vR_e [map_e [eval_real_e bounded_real_e]]]]]; eauto. rewrite map_e in *; inversion Heqo; subst. pose proof (meps_0_deterministic _ eval_real_e H7); subst. simpl in *. inversion Heqo0; subst; lra. - rewrite Nat.eqb_neq in v1_eq; set_tac. destruct v1_mem; subst; try congruence. apply fVars_sound ; try auto. destruct H0; auto. } { intros v1 mem_fVars. specialize (P_valid v1 mem_fVars). unfold updEnv. case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try auto. rewrite Nat.eqb_eq in case_v1; subst. assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by (rewrite NatSet.union_spec; auto). rewrite <- NatSet.mem_spec in in_union. rewrite in_union in *; congruence. } { intros v1 v1_mem; set_tac. unfold updDefVars. case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto. apply types_defined. clear H5; set_tac. destruct v1_mem as [v_fVar | v_dVar]; try set_tac. destruct v_dVar as [? | [? ?]]; try auto. rewrite Nat.eqb_neq in case_v1; congruence. } { exists vF_res; exists m_res; try auto. econstructor; eauto. } - inversion eval_real; subst. unfold updEnv; simpl. unfold validErrorboundCmd in valid_bounds. simpl in *. edestruct validErrorbound_sound as [[vF [mF eval_e]] bounded_e]; eauto. exists vF; exists mF; econstructor; eauto. Qed. Theorem validErrorboundCmd_sound (f:cmd Q): forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err P Gamma defVars, typeCheckCmd f defVars Gamma = true -> approxEnv E1 defVars A fVars dVars E2 -> ssa f (NatSet.union fVars dVars) outVars -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL -> bstep (toRCmd f) E2 defVars vF mF -> validErrorboundCmd f Gamma A dVars = true -> validIntervalboundsCmd f A P dVars = true -> dVars_range_valid dVars E1 A -> fVars_P_sound fVars E1 P -> vars_typed (NatSet.union fVars dVars) defVars -> FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) -> (Rabs (vR - vF) <= (Q2R err))%R. Proof. induction f; intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float valid_bounds valid_intv fVars_sound P_valid types_defined A_res; cbn in *; Flover_compute; try congruence; type_conv; subst. - inversion eval_real; inversion eval_float; subst. inversion ssa_f; subst. assert (NatSet.Subset (usedVars e -- dVars) fVars) as valid_varset. { set_tac. split; try auto. split; try set_tac. hnf; intros; subst; set_tac. } match goal with | [H : validErrorbound _ _ _ _ = true |- _] => eapply validErrorbound_sound with (err := e2) (elo := fst(i)) (ehi:= snd(i)) in H; edestruct i; eauto; destruct H as [[vFe [mFe eval_float_e]] bounded_e] end. canonize_hyps. rename R into valid_rec. rewrite (typingSoundnessExp _ _ L0 eval_float_e) in *; simpl in *. (* destruct (Gamma (Var Q n)); try congruence. *) (* match goal with *) (* | [ H: _ && _ = true |- _] => andb_to_prop H *) (* end. *) (* type_conv. *) apply (IHf A (updEnv n v E1) (updEnv n v0 E2) outVars fVars (NatSet.add n dVars) vR vF mF elo ehi err P Gamma (updDefVars n m1 defVars)); eauto. + eapply approxUpdBound; try eauto. simpl in *. apply Rle_trans with (r2:= Q2R e2); try lra. eapply bounded_e; eauto. + eapply ssa_equal_set; eauto. hnf. intros a; split; intros in_set. * rewrite NatSet.add_spec, NatSet.union_spec; rewrite NatSet.union_spec, NatSet.add_spec in in_set. destruct in_set as [P1 | [ P2 | P3]]; auto. * rewrite NatSet.add_spec, NatSet.union_spec in in_set; rewrite NatSet.union_spec, NatSet.add_spec. destruct in_set as [P1 | [ P2 | P3]]; auto. + hnf. intros a in_diff. rewrite NatSet.diff_spec, NatSet.add_spec in in_diff. destruct in_diff as [ in_freeVars no_dVar]. apply freeVars_subset. simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. split; try auto. + eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars)); eauto using Rmap_updVars_comm. + intros v1 v1_mem. unfold updEnv. case_eq (v1 =? n); intros v1_eq. * apply Nat.eqb_eq in v1_eq; subst. exists v, (q1,q2), e1; split; try auto; split; try auto. simpl. rewrite <- R1, <- R0. destruct (validIntervalbounds_sound e L (E:=E1) (Gamma:=defVars) (fVars:=fVars)) as [iv_e [ err_e [ vR_e [ map_e [eval_real_e bounded_real_e]]]]]; eauto. repeat destr_factorize. pose proof (meps_0_deterministic _ eval_real_e H7); subst. inversion Heqo0; subst. simpl in *; auto. * rewrite Nat.eqb_neq in v1_eq. set_tac. destruct v1_mem as [? | [? ?]]. { exfalso; apply v1_eq; auto. } { apply fVars_sound ; auto. } + intros v1 mem_fVars. specialize (P_valid v1 mem_fVars). unfold updEnv. case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try auto. rewrite Nat.eqb_eq in case_v1; subst. assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by (rewrite NatSet.union_spec; auto). rewrite <- NatSet.mem_spec in in_union. rewrite in_union in *; congruence. + intros v1 v1_mem; set_tac. unfold updDefVars. case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto. apply types_defined. rewrite NatSet.union_spec. destruct v1_mem as [v_fVar | v_dVar]; try auto. rewrite NatSet.add_spec in v_dVar. destruct v_dVar; try auto. subst; rewrite Nat.eqb_refl in case_v1; congruence. - inversion eval_real; subst. inversion eval_float; subst. unfold updEnv; simpl. unfold validErrorboundCmd in valid_bounds. simpl in *. edestruct validErrorbound_sound as [[* [* eval_e]] bounded_e]; eauto. Qed.