Commit 9e2ebfc6 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Remove assumption on already checked expressions;

Progress RealRangeValidator proof
parent af40a32d
This diff is collapsed.
......@@ -34,6 +34,30 @@ Proof.
clear H.
destruct p as [exprAfs noise].
pose proof (validAffineBounds_sound) as sound_affine.
specialize (sound_affine f A P NatSet.empty NatSet.empty E Gamma
exprAfs noise (FloverMap.empty (affine_form Q)) 1%nat (fun _ => None)).
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> (fun _ : nat => None) n = None) as Himap by trivial.
assert (affine_dVars_range_valid NatSet.empty E A) as HdVarsValid
by (unfold affine_dVars_range_valid; intros * H; set_tac).
assert (NatSet.Subset (usedVars f -- NatSet.empty) (usedVars f)) as Hsubset by set_tac.
assert (affine_fVars_P_sound (usedVars f) E P) as HfVars by admit.
assert (affine_vars_typed (usedVars f NatSet.empty) Gamma) as Hvarstyped
by (unfold affine_vars_typed; intros v in_set; set_tac; destruct in_set; set_tac).
specialize (sound_affine f A P (usedVars f) NatSet.empty E Gamma
exprAfs noise (FloverMap.empty (affine_form Q)) 1%nat (fun _ => None)
Hinoise Himap Hafcheck HdVarsValid Hsubset HfVars Hvarstyped)
as [map2 [af [vR [aiv [aerr sound_affine]]]]].
destruct sound_affine as [_ [Haiv [Hsup [_ [_ [_ [_ [Hee Heval]]]]]]]].
exists aiv, aerr, vR.
split; try split; try auto.
apply AffineArith.to_interval_containment in Heval.
unfold isSupersetIntv in Hsup.
apply andb_prop in Hsup as [Hsupl Hsupr].
apply Qle_bool_iff in Hsupl.
apply Qle_bool_iff in Hsupr.
apply Qle_Rle in Hsupl.
apply Qle_Rle in Hsupr.
rewrite <- to_interval_to_intv in Heval.
simpl in Heval.
destruct Heval as [Heval1 Heval2].
split; eauto using Rle_trans.
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