Commit 6d5987a6 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Remove redundant parameters from checked_error_expressions

parent 6f73f2ed
......@@ -1789,17 +1789,12 @@ Proof.
symmetry; now apply expr_compare_eq_eval_compat.
Qed.
Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap fVars dVars
Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap
noise_map noise expr_map :=
forall v__R v__FP m__FP iv__A err__A,
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
forall v__R v__FP m__FP (iv__A: intv) (err__A: error),
eval_expr_det E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) v__R REAL ->
eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
FloverMap.find e A = Some (iv__A, err__A) ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
(* affine_dVars_range_valid dVars E1 A noise1 expr_map1 noise_map1 -> *)
validTypes e Gamma ->
exists af err__af,
fresh noise (afQ2R af) /\
(forall n, (n >= noise)%nat -> noise_map n = None) /\
......@@ -1809,14 +1804,14 @@ Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap fVars dV
(err__af <= Q2R err__A)%R /\
af_evals (afQ2R af) (v__R - v__FP)%R noise_map.
Lemma checked_error_expressions_extension e E1 E2 A Gamma DeltaMap fVars dVars
Lemma checked_error_expressions_extension e E1 E2 A Gamma DeltaMap
noise_map1 noise_map2 noise1 noise2 expr_map1 expr_map2:
contained_map noise_map1 noise_map2 ->
(noise1 <= noise2)%nat ->
contained_flover_map expr_map1 expr_map2 ->
(forall n, (n >= noise2)%nat -> noise_map2 n = None) ->
checked_error_expressions e E1 E2 A Gamma DeltaMap fVars dVars noise_map1 noise1 expr_map1 ->
checked_error_expressions e E1 E2 A Gamma DeltaMap fVars dVars noise_map2 noise2 expr_map2.
checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1 ->
checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2.
Proof.
intros cont contf Hnoise Hvalidmap checked1.
unfold checked_error_expressions in checked1 |-*.
......@@ -1826,11 +1821,11 @@ Proof.
intuition; eauto using fresh_monotonic, af_evals_map_extension.
Qed.
Lemma checked_error_expressions_flover_map_add_compat e e' af E1 E2 A Gamma DeltaMap fVars dVars
Lemma checked_error_expressions_flover_map_add_compat e e' af E1 E2 A Gamma DeltaMap
noise_map noise expr_map:
Q_orderedExps.exprCompare e' e <> Eq ->
checked_error_expressions e E1 E2 A Gamma DeltaMap fVars dVars noise_map noise expr_map ->
checked_error_expressions e E1 E2 A Gamma DeltaMap fVars dVars noise_map noise
checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map noise expr_map ->
checked_error_expressions e E1 E2 A Gamma DeltaMap noise_map noise
(FloverMap.add e' af expr_map).
Proof.
intros Hneq checked1.
......@@ -1842,20 +1837,18 @@ Proof.
rewrite FloverMapFacts.P.F.add_neq_o; auto.
Qed.
Definition affine_dVars_error_valid E1 E2 A Gamma DeltaMap fVars dVars
noise_map noise expr_map: Prop :=
Definition affine_dVars_error_valid E1 E2 A Gamma DeltaMap dVars noise_map noise expr_map: Prop :=
forall v, NatSet.In v dVars ->
checked_error_expressions (Var Q v) E1 E2 A Gamma DeltaMap fVars dVars
noise_map noise expr_map.
checked_error_expressions (Var Q v) E1 E2 A Gamma DeltaMap noise_map noise expr_map.
Lemma affine_dVars_error_valid_extension E1 E2 A Gamma DeltaMap fVars dVars
Lemma affine_dVars_error_valid_extension E1 E2 A Gamma DeltaMap dVars
noise_map1 noise_map2 noise1 noise2 expr_map1 expr_map2:
contained_map noise_map1 noise_map2 ->
(noise1 <= noise2)%nat ->
contained_flover_map expr_map1 expr_map2 ->
(forall n, (n >= noise2)%nat -> noise_map2 n = None) ->
affine_dVars_error_valid E1 E2 A Gamma DeltaMap fVars dVars noise_map1 noise1 expr_map1 ->
affine_dVars_error_valid E1 E2 A Gamma DeltaMap fVars dVars noise_map2 noise2 expr_map2.
affine_dVars_error_valid E1 E2 A Gamma DeltaMap dVars noise_map1 noise1 expr_map1 ->
affine_dVars_error_valid E1 E2 A Gamma DeltaMap dVars noise_map2 noise2 expr_map2.
Proof.
intros ? ? ? ? Hdvars.
unfold affine_dVars_error_valid in Hdvars |-*.
......@@ -1883,14 +1876,14 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar
FloverMap.find (elt:=intv * error) e A = Some (iv__A, err__A) ->
(0 < noise1)%nat ->
(forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
affine_dVars_error_valid E1 E2 A Gamma DeltaMap fVars dVars noise_map1 noise1 expr_map1 ->
affine_dVars_error_valid E1 E2 A Gamma DeltaMap dVars noise_map1 noise1 expr_map1 ->
(forall e' : FloverMap.key,
FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
exists (v__FP' : R) (m__FP' : mType),
eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') ->
(forall e' : FloverMap.key,
FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
checked_error_expressions e' E1 E2 A Gamma DeltaMap fVars dVars noise_map1 noise1 expr_map1) ->
checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
((exists (v__FP : R) (m__FP : mType),
eval_expr_det E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
(forall e' : FloverMap.key,
......@@ -1914,8 +1907,7 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar
(forall e' : FloverMap.key,
~ FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
FloverMap.In (elt:=affine_form Q) e' expr_map2 ->
checked_error_expressions e' E1 E2 A Gamma DeltaMap fVars dVars noise_map2 noise2
expr_map2)).
checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2)).
Lemma validErrorboundAA_sound_var n E1 E2 A Gamma DeltaMap fVars dVars:
validErrorboundAA_sound_statement (Var Q n) E1 E2 A Gamma DeltaMap fVars dVars.
......
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