Commit 3c902fe7 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Start reworking conclusion of validAffineBounds_sound

parent 7256c32f
......@@ -1830,6 +1830,28 @@ Proof.
apply visitedSubexpr; eauto.
Lemma validAffineBounds_sound_validRanges e A P fVars dVars E Gamma exprmap2 noise2
exprmap1 noise1 map1:
(forall e, (exists af, FloverMap.find e exprmap1 = Some af) ->
checked_expressions A E Gamma fVars dVars e exprmap1 noise1 map1) ->
(noise1 > 0)%nat ->
(forall n, (n >= noise1)%nat -> map1 n = None) ->
validAffineBounds e A P dVars exprmap1 noise1 = Some (exprmap2, noise2) ->
affine_dVars_range_valid dVars E A noise1 exprmap1 map1 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
affine_fVars_P_sound fVars E P ->
affine_vars_typed (NatSet.union fVars dVars) Gamma ->
validRanges e A E Gamma.
induction e; intros * checked_expressions1 Hnoisepose1 Hvalidmap1 Hvalidbounds1 Hdvars1
Hsubset1 Hfvars1 Htypes1;
edestruct validAffineBounds_sound as [map2 [af [vR [iv [err valid_bounds_sound]]]]]; eauto.
- simpl; split; eauto.
exists iv, err, vR.
split; try split.
1-2: intuition.
Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
(exprsAf: expressionsAffine) (currentMaxNoise: nat): option (expressionsAffine * nat) :=
match c with
......@@ -2104,7 +2126,7 @@ Proof.
exists ihmap, ihaf, ihvR, ihaiv, ihaerr.
repeat split; try auto.
+ econstructor; try eauto.
eapply IntervalValidation.swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n REAL Gamma)) ; try eauto.
eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n REAL Gamma)) ; try eauto.
intros n1; erewrite Rmap_updVars_comm; eauto.
+ intros e' Hnone Hsome.
specialize (ihchecked e').
......@@ -138,7 +138,7 @@ Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P:precond)
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
fVars_P_sound fVars E P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
validRanges f A E.
validRanges f A E Gamma.
(* exists iv err vR, *)
(* FloverMap.find f A = Some (iv, err) /\ *)
(* eval_expr E (toRMap Gamma) (toREval (toRExp f)) vR REAL /\ *)
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment