Commit fe9c5000 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Rename variables in ErrorAnalysis

parent fe530b1c
......@@ -14,46 +14,46 @@ Definition eval_Fin E2 Gamma (e:expr Q) nF m :=
Arguments eval_Fin _ _ _ _ _/.
Fixpoint validErrorBounds (e:expr Q) A Gamma dVars :Prop :=
Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma fVars dVars :Prop :=
(match e with
| Unop u e => validErrorBounds e A Gamma dVars
| Downcast m e => validErrorBounds e A Gamma dVars
| Unop u e => validErrorBounds e E1 E2 A Gamma fVars dVars
| Downcast m e => validErrorBounds e E1 E2 A Gamma fVars dVars
| Binop b e1 e2 =>
validErrorBounds e1 A Gamma dVars /\
validErrorBounds e2 A Gamma dVars
validErrorBounds e1 E1 E2 A Gamma fVars dVars /\
validErrorBounds e2 E1 E2 A Gamma fVars dVars
| Fma e1 e2 e3 =>
validErrorBounds e1 A Gamma dVars /\
validErrorBounds e2 A Gamma dVars /\
validErrorBounds e3 A Gamma dVars
validErrorBounds e1 E1 E2 A Gamma fVars dVars /\
validErrorBounds e2 E1 E2 A Gamma fVars dVars /\
validErrorBounds e3 E1 E2 A Gamma fVars dVars
| _ => True
end) /\
forall E1 E2 fVars nR err elo ehi,
forall v__R iv err,
validTypes e Gamma ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_Real E1 Gamma e nR ->
eval_Real E1 Gamma e v__R ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
FloverMap.find e A = Some ((elo,ehi),err) ->
(exists nF m,
eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m) /\
(forall nF m,
eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m ->
(Rabs (nR - nF) <= (Q2R err))%R).
FloverMap.find e A = Some (iv, err) ->
(exists v__FP m__FP,
eval_expr E2 (toRExpMap Gamma) (toRExp e) v__FP m__FP) /\
(forall v__FP m__FP,
eval_expr E2 (toRExpMap Gamma) (toRExp e) v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Lemma validErrorBounds_single e A Gamma dVars:
validErrorBounds e A Gamma dVars ->
forall E1 E2 fVars nR err elo ehi,
Lemma validErrorBounds_single e E1 E2 A Gamma fVars dVars:
validErrorBounds e E1 E2 A Gamma fVars dVars ->
forall v__R iv err,
validTypes e Gamma ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_Real E1 Gamma e nR ->
eval_Real E1 Gamma e v__R ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
FloverMap.find e A = Some ((elo,ehi),err) ->
(exists nF m,
eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m) /\
(forall nF m,
eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m ->
(Rabs (nR - nF) <= (Q2R err))%R).
FloverMap.find e A = Some (iv, err) ->
(exists v__FP m__FP,
eval_expr E2 (toRExpMap Gamma) (toRExp e) v__FP m__FP) /\
(forall v__FP m__FP,
eval_expr E2 (toRExpMap Gamma) (toRExp e) v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Proof.
intros validError_e;
intros; destruct e; cbn in *; split;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment