Commit e320513e authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix soundness proof for roundoff error valdator

parent c056a2d9
......@@ -18,22 +18,24 @@ exprression may yield different values for different machine epsilons
**)
Inductive approxEnv : env -> (expr R -> option mType) -> analysisResult -> NatSet.t
-> NatSet.t -> env -> Prop :=
|approxRefl defVars A:
approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
approxEnv E1 defVars A fVars dVars E2 ->
|approxRefl Gamma A:
approxEnv emptyEnv Gamma A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 Gamma A v1 v2 x fVars dVars m:
approxEnv E1 Gamma A fVars dVars E2 ->
Gamma (Var R x) = Some m ->
(Rabs (v1 - v2) <= computeErrorR v1 m)%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1)
(updDefVars (Var R x) m defVars) A (NatSet.add x fVars) dVars
(updDefVars (Var R x) m Gamma) A (NatSet.add x fVars) dVars
(updEnv x v2 E2)
|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m iv err:
approxEnv E1 defVars A fVars dVars E2 ->
|approxUpdBound E1 E2 Gamma A v1 v2 x fVars dVars m iv err:
approxEnv E1 Gamma A fVars dVars E2 ->
Gamma (Var R x) = Some m ->
FloverMap.find (Var Q x) A = Some (iv, err) ->
(Rabs (v1 - v2) <= Q2R err)%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1)
(updDefVars (Var R x) m defVars) A fVars (NatSet.add x dVars)
Gamma A fVars (NatSet.add x dVars)
(updEnv x v2 E2).
Section RelationProperties.
......@@ -58,7 +60,7 @@ Section RelationProperties.
+ eapply IHa; eauto.
set_tac.
destruct x_valid; set_tac.
destruct H1 as [? | [? ?]]; subst; try auto.
destruct H2 as [? | [? ?]]; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
- unfold updEnv in *.
case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
......@@ -66,7 +68,7 @@ Section RelationProperties.
+ eapply IHa; auto.
set_tac.
destruct x_valid; set_tac.
destruct H2 as [? | [ ? ?]]; subst; try auto.
destruct H3 as [? | [ ? ?]]; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
Qed.
......@@ -104,7 +106,7 @@ Section RelationProperties.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H1.
apply H2.
set_tac. }
unfold updEnv in *; rewrite x_x0_neq in *.
unfold updDefVars in x_typed.
......@@ -130,7 +132,7 @@ Section RelationProperties.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H0; set_tac.
apply H1; set_tac.
}
unfold updEnv in *; rewrite x_x0_neq in *.
unfold updDefVars in x_typed; cbn in x_typed.
......@@ -144,7 +146,7 @@ Section RelationProperties.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
inversion E1_def; inversion E2_def; subst.
rewrite A_e in *; inversion H; auto.
rewrite A_e in *; inversion H0; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
......
......@@ -362,7 +362,8 @@ Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
eval_expr E1 (toRTMap defVars) (toREval e) nR REAL ->
eval_expr E2 defVars e nF1 m ->
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars (Var R 1) m defVars)
(updDefVars (Downcast mEps (Var R 1)) mEps
(updDefVars (Var R 1) m defVars))
(toRExp (Downcast mEps (Var Q 1))) nF mEps->
(Rabs (nR - nF1) <= err)%R ->
(Rabs (nR - nF) <= err + computeErrorR nF1 mEps)%R.
......
......@@ -149,22 +149,34 @@ Proof.
auto.
Qed.
Section soundnessProofs.
Definition eval_Real E1 Gamma (e:expr Q) nR :=
eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) nR REAL.
Arguments eval_Real _ _ _ _/.
Definition eval_Fin E2 Gamma (e:expr Q) nF m :=
eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m.
Arguments eval_Fin _ _ _ _ _/.
Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi fVars
dVars Gamma exprTypes:
eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp (Var Q v))) nR REAL ->
eval_Real E1 Gamma (Var Q v) nR ->
validTypes (Var Q v) Gamma ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
validRanges (Var Q v) A E1 (toRExpMap Gamma) ->
validRanges (Var Q v) A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorbound (Var Q v) exprTypes A dVars = true ->
NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
exists nF m,
eval_expr E2 (toRExpMap Gamma) (toRExp (Var Q v)) nF m.
eval_Fin E2 Gamma (Var Q v) nF m.
Proof.
intros eval_real typing_ok approxCEnv bounds_valid error_valid v_sound A_var.
apply validRanges_single in bounds_valid.
destruct_smart [find_v [eval_real2 bounds_valid]] bounds_valid.
pose proof (meps_0_deterministic _ eval_real eval_real2). subst.
pose proof (meps_0_deterministic _ eval_real eval_real2); subst.
cbn in *.
inversion eval_real; subst.
Flover_compute; type_conv.
......@@ -175,17 +187,17 @@ Proof.
apply NatSetProps.FM.diff_3; set_tac.
- destruct typing_ok as [? [tdef ?]].
exists x, x0. eapply Var_load; eauto.
admit.
Admitted.
eapply toRExpMap_some; eauto; simpl; auto.
Qed.
Lemma validErrorboundCorrectVariable:
forall E1 E2 A (v:nat) e nR nF mF nlo nhi fVars dVars exprTypes,
eval_expr E1 (toRMap (toRExpMap exprTypes)) (toREval (toRExp (Var Q v))) nR REAL ->
eval_expr E2 (toRExpMap exprTypes) (toRExp (Var Q v)) nF mF ->
approxEnv E1 (toRExpMap exprTypes) A fVars dVars E2 ->
validTypes (Var Q v) (exprTypes) ->
validRanges (Var Q v) A E1 (toRExpMap exprTypes) ->
validErrorbound (Var Q v) exprTypes A dVars = true ->
forall E1 E2 A (v:nat) e nR nF mF nlo nhi fVars dVars Gamma,
eval_Real E1 Gamma (Var Q v) nR ->
eval_Fin E2 Gamma (Var Q v) nF mF ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
validTypes (Var Q v) (Gamma) ->
validRanges (Var Q v) A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorbound (Var Q v) Gamma A dVars = true ->
NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
......@@ -215,40 +227,40 @@ Proof.
repeat destr_factorize.
rewrite computeErrorQ_computeErrorR in error_valid.
eapply Rle_trans; eauto.
assert (m = mF) by admit; subst. (* comes from toRExpMap... *)
eapply toRExpMap_some in Heqo; eauto; simpl in *.
assert (m = mF) by congruence; subst.
rewrite <- maxAbs_impl_RmaxAbs.
apply computeErrorR_up.
apply contained_leq_maxAbs.
simpl in *; auto.
Admitted.
Qed.
Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR Gamma:
eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp (Const m n))) nR REAL ->
Lemma validErrorboundCorrectConstant_eval E2 m n Gamma:
validTypes (Const m n) Gamma ->
exists nF m',
eval_expr E2 (toRExpMap Gamma) (toRExp (Const m n)) nF m'.
eval_Fin E2 Gamma (Const m n) nF m'.
Proof.
intros eval_real typing_ok.
intros typing_ok.
simpl in *.
destruct typing_ok as [? [type_def [? ?]]]; subst.
repeat eexists.
eapply Const_dist'; eauto.
- instantiate (1:= 0%R).
rewrite Rabs_R0. auto using mTypeToR_pos_R.
- admit.
Admitted.
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 exprTypes
defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR REAL ->
eval_expr E2 defVars (toRExp (Const m n)) nF m ->
validTypes (Const m n) exprTypes ->
Gamma:
eval_Real E1 Gamma (Const m n) nR ->
eval_Fin E2 Gamma (Const m n) nF m ->
validTypes (Const m n) Gamma ->
validErrorbound (Const m n) exprTypes 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.
unfold eval_Real in *.
cbn in *; Flover_compute; type_conv.
eapply Rle_trans.
eapply const_abs_err_bounded; eauto.
......@@ -288,31 +300,30 @@ 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:
eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp (Binop Plus e1 e2))) nR REAL ->
eval_expr E2 (toRExpMap Gamma) (toRExp e1) nF1 m1 ->
eval_expr E2 (toRExpMap Gamma) (toRExp e2) nF2 m2 ->
eval_Real E1 Gamma e1 nR1 ->
eval_Real E1 Gamma e2 nR2 ->
eval_Real E1 Gamma (Binop Plus e1 e2) nR ->
eval_Fin E2 Gamma e1 nF1 m1 ->
eval_Fin E2 Gamma e2 nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 (toRExpMap Gamma)))
(updDefVars (Binop Plus (Var R 1) (Var R 2)) m
(updDefVars (Var Rdefinitions.R 2) m2
(updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
(toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
validTypes (Binop Plus e1 e2) Gamma ->
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)->
FloverMap.find (Binop Plus e1 e2) Gamma = Some m ->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros e1_real e2_real eval_real e1_float e2_float eval_float
subexpr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add
err1_bounded err2_bounded.
cbn in subexpr_ok.
destruct subexpr_ok
as [mBin [type_def [[? [? [me1 [me2 [type_e1 [type_e2 join_def]]]]]] ?]]].
valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add
Gamma_Plus err1_bounded err2_bounded.
cbn in *; Flover_compute; type_conv.
eapply Rle_trans.
eapply
......@@ -332,7 +343,6 @@ Proof.
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).
assert (mBin = m) by admit (* inversion lemma for semantics s*).
subst.
rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
apply computeErrorR_up.
......@@ -344,56 +354,35 @@ Proof.
- rewrite Q2R_max4.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; lra.
Admitted.
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 fBits fBit:
(isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find (Binop Sub e1 e2) fBits = Some fBit) ->
Some m = join m1 m2 fBit ->
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (Binop Sub e1 e2))) nR REAL ->
eval_expr E2 defVars (toRBMap fBits) (toRExp e1) nF1 m1->
eval_expr E2 defVars (toRBMap fBits) (toRExp e2) nF2 m2 ->
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma :
eval_Real E1 Gamma e1 nR1 ->
eval_Real E1 Gamma e2 nR2 ->
eval_Real E1 Gamma (Binop Sub e1 e2) nR ->
eval_Fin E2 Gamma e1 nF1 m1->
eval_Fin E2 Gamma e2 nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(fun e =>
match e with
| Binop b (Var _ 1) (Var _ 2) => toRBMap fBits (toRExp (Binop b e1 e2))
| _ => toRBMap fBits e
end)
(updDefVars (Binop Sub (Var R 1) (Var R 2)) m
(updDefVars (Var Rdefinitions.R 2) m2
(updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
(toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Sub e1 e2) defVars Gamma fBits = 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)->
FloverMap.find (Binop Sub e1 e2) Gamma = Some m ->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros validFBit mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
subexpr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub Gamma_sub
err1_bounded err2_bounded.
assert (FloverMap.find e1 Gamma = Some m1) as type_e1.
{ eapply typingSoundnessExp; eauto.
cbn in subexpr_ok; Flover_compute; auto. }
assert (FloverMap.find e2 Gamma = Some m2) as type_e2.
{ eapply typingSoundnessExp; eauto.
cbn in subexpr_ok; Flover_compute; auto. }
assert (FloverMap.find (Binop Sub e1 e2) Gamma = Some m).
{ eapply typingSoundnessExp with (E:=E2) (v:=perturb (nF1 - nF2) m 0%R); eauto.
eapply Binop_dist' with (delta:=0%R) (fBit:=fBit); eauto; try congruence.
- rewrite Rabs_R0. apply mTypeToR_pos_R; auto.
- intros fixed_m1 fixed_m2.
specialize (validFBit fixed_m1 fixed_m2).
apply toRBMap_some in validFBit.
simpl in *; auto. }
clear subexpr_ok.
cbn in *; Flover_compute; type_conv.
eapply Rle_trans.
eapply (subtract_abs_err_bounded e1 e2); try eauto.
......@@ -898,52 +887,32 @@ 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 fBits fBit:
(isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find (Binop Mult e1 e2) fBits = Some fBit) ->
Some m = join m1 m2 fBit ->
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (Binop Mult e1 e2))) nR REAL ->
eval_expr E2 defVars (toRBMap fBits) (toRExp e1) nF1 m1->
eval_expr E2 defVars (toRBMap fBits) (toRExp e2) nF2 m2 ->
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma :
eval_Real E1 Gamma e1 nR1 ->
eval_Real E1 Gamma e2 nR2 ->
eval_Real E1 Gamma (Binop Mult e1 e2) nR ->
eval_Fin E2 Gamma e1 nF1 m1->
eval_Fin E2 Gamma e2 nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(fun e =>
match e with
| Binop b (Var _ 1) (Var _ 2) => toRBMap fBits (toRExp (Binop b e1 e2))
| _ => toRBMap fBits e
end)
(updDefVars (Binop Mult (Var R 1) (Var R 2)) m
(updDefVars (Var Rdefinitions.R 2) m2
(updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
(toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Mult e1 e2) defVars Gamma fBits = 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)->
FloverMap.find (Binop Mult e1 e2) Gamma = Some m ->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros validFBit mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
subexpr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_mult
intros e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub Gamma_sub
err1_bounded err2_bounded.
assert (FloverMap.find e1 Gamma = Some m1) as type_e1.
{ eapply typingSoundnessExp; eauto.
cbn in subexpr_ok; Flover_compute; auto. }
assert (FloverMap.find e2 Gamma = Some m2) as type_e2.
{ eapply typingSoundnessExp; eauto.
cbn in subexpr_ok; Flover_compute; auto. }
assert (FloverMap.find (Binop Mult e1 e2) Gamma = Some m).
{ eapply typingSoundnessExp with (E:=E2) (v:=perturb (nF1 * nF2) m 0%R); eauto.
eapply Binop_dist' with (delta:=0%R) (fBit:=fBit); eauto; try congruence.
- rewrite Rabs_R0. apply mTypeToR_pos_R; auto.
- intros fixed_m1 fixed_m2.
specialize (validFBit fixed_m1 fixed_m2).
apply toRBMap_some in validFBit.
simpl in *; auto. }
clear subexpr_ok.
cbn in *; Flover_compute; type_conv; subst.
cbn in *; Flover_compute; type_conv.
canonize_hyps.
eapply Rle_trans.
eapply (mult_abs_err_bounded e1 e2); eauto.
......@@ -983,23 +952,17 @@ 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 fBits fBit:
(isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find (Binop Div e1 e2) fBits = Some fBit) ->
Some m = join m1 m2 fBit ->
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e1)) nR1 REAL ->
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e2)) nR2 REAL ->
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (Binop Div e1 e2))) nR REAL ->
eval_expr E2 defVars (toRBMap fBits) (toRExp e1) nF1 m1->
eval_expr E2 defVars (toRBMap fBits) (toRExp e2) nF2 m2 ->
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma :
eval_Real E1 Gamma e1 nR1 ->
eval_Real E1 Gamma e2 nR2 ->
eval_Real E1 Gamma (Binop Div e1 e2) nR ->
eval_Fin E2 Gamma e1 nF1 m1->
eval_Fin E2 Gamma e2 nF2 m2 ->
eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(fun e =>
match e with
| Binop b (Var _ 1) (Var _ 2) => toRBMap fBits (toRExp (Binop b e1 e2))
| _ => toRBMap fBits e
end)
(updDefVars (Binop Div (Var R 1) (Var R 2)) m
(updDefVars (Var Rdefinitions.R 2) m2
(updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
(toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Div e1 e2) defVars Gamma fBits = true ->
validErrorbound (Binop Div e1 e2) Gamma A dVars = true ->
(Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
(Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
......@@ -1007,31 +970,16 @@ Lemma validErrorboundCorrectDiv E1 E2 A
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)->
FloverMap.find (Binop Div e1 e2) Gamma = Some m ->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros validFBit mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
subexpr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real A_e1 A_e2 A_div
intros e1_real e2_real eval_real e1_float e2_float eval_float valid_error
valid_intv1 valid_intv2 no_div_zero_real A_e1 A_e2 A_sub Gamma_sub
err1_bounded err2_bounded.
assert (FloverMap.find e1 Gamma = Some m1) as type_e1.
{ eapply typingSoundnessExp; eauto.
cbn in subexpr_ok; Flover_compute; auto. }
assert (FloverMap.find e2 Gamma = Some m2) as type_e2.
{ eapply typingSoundnessExp; eauto.
cbn in subexpr_ok; Flover_compute; auto. }
assert (FloverMap.find (Binop Div e1 e2) Gamma = Some m).
{ eapply typingSoundnessExp with (E:=E2) (v:=perturb (nF1 / nF2) m 0%R); eauto.
eapply Binop_dist' with (delta:=0%R) (fBit:=fBit); eauto; try congruence.
- rewrite Rabs_R0. apply mTypeToR_pos_R; auto.
- intros; subst. inversion eval_float; subst.
inversion H5; cbn in *; hnf; intros subst. apply H6; subst; congruence.
- intros fixed_m1 fixed_m2.
specialize (validFBit fixed_m1 fixed_m2).
apply toRBMap_some in validFBit.
simpl in *; auto. }
clear subexpr_ok.
cbn in *; Flover_compute; type_conv; subst.
cbn in *; Flover_compute; type_conv.
canonize_hyps.
eapply Rle_trans.
eapply (div_abs_err_bounded e1 e2); eauto.
rename L0 into no_div_zero_float.
......@@ -1063,14 +1011,13 @@ Proof.
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.
e1_real e2_float e2_real A_sub 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.
pose proof (interval_inversion_valid (Q2R e2lo,Q2R e2hi) no_div_zero_real_R valid_intv2) 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
......@@ -1101,7 +1048,7 @@ Proof.
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 H1 err2_pos) as err_prop_inv.
pose proof (err_prop_inversion_neg float_iv_neg real_iv_neg err2_bounded valid_intv2 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.
......@@ -1540,7 +1487,7 @@ Proof.
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 H1 err2_pos) as err_prop_inv.
pose proof (err_prop_inversion_pos float_iv_pos real_iv_pos err2_bounded valid_intv2 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.
......@@ -1855,20 +1802,20 @@ Proof.
+ 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 H0 H1) as valid_div_float.
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 H5.
apply Rle_Qle in H5. 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 H6.
apply Rle_Qle in H6. 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.
......@@ -1889,53 +1836,47 @@ Proof.
+ 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.
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 H4.
apply Rle_Qle in H4. 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 H5. inversion H5. rewrite Zmult_1_r in *.
rewrite Z.abs_0_iff in H7.
rewrite H7. rewrite Z.abs_0. hnf. simpl; auto. }
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 H7; rewrite H6; auto.
+ intros. apply H2. rewrite (H5 (e2lo-err2) H7). hnf. auto.
+ intros. apply H3. rewrite H5; auto. hnf; auto.
- rewrite <- (Qmult_0_l (minAbs (e2lo - err2, e2hi + err2))) in H4.
rewrite (Qmult_inj_r) in H4; auto. }
+ 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 fBits fBit:
(isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 ->
FloverMap.find (Fma e1 e2 e3) fBit