Commit 8ac618e5 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Prove RealRangeValidator sound

parent 1c933ce8
...@@ -29,24 +29,34 @@ Proof. ...@@ -29,24 +29,34 @@ Proof.
+ unfold dVars_range_valid; intros; set_tac. + unfold dVars_range_valid; intros; set_tac.
+ set_tac. + set_tac.
+ unfold vars_typed. intros v in_set; set_tac. destruct in_set; set_tac. + unfold vars_typed. intros v in_set; set_tac. destruct in_set; set_tac.
- destruct (validAffineBounds f A P NatSet.empty (FloverMap.empty (affine_form Q)) 1) eqn: Hafcheck; - pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
fold iexpmap inoise imap in H.
destruct (validAffineBounds f A P NatSet.empty iexpmap inoise) eqn: Hafcheck;
try congruence. try congruence.
clear H. clear H.
destruct p as [exprAfs noise]. destruct p as [exprAfs noise].
pose proof (validAffineBounds_sound) as sound_affine. pose proof (validAffineBounds_sound) as sound_affine.
assert ((forall e : FloverMap.key,
(exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e iexpmap = Some af) ->
checked_expressions A E Gamma e iexpmap inoise imap)) as Hchecked
by (intros e Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
rewrite FloverMapFacts.P.F.empty_o in Hein;
congruence).
assert (1 > 0)%nat as Hinoise by omega. assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> (fun _ : nat => None) n = None) as Himap by trivial. eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
assert (affine_dVars_range_valid NatSet.empty E A) as HdVarsValid assert (affine_dVars_range_valid NatSet.empty E A inoise iexpmap imap) as HdVarsValid
by (unfold affine_dVars_range_valid; intros * H; set_tac). 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 (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 exact H0. assert (affine_fVars_P_sound (usedVars f) E P) as HfVars by exact H0.
assert (affine_vars_typed (usedVars f NatSet.empty) Gamma) as Hvarstyped 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). 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 specialize (sound_affine f A P (usedVars f) NatSet.empty E Gamma
exprAfs noise (FloverMap.empty (affine_form Q)) 1%nat (fun _ => None) exprAfs noise iexpmap inoise imap
Hinoise Himap Hafcheck HdVarsValid Hsubset HfVars Hvarstyped) Hchecked Hinoise Himap Hafcheck HdVarsValid Hsubset HfVars Hvarstyped)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]. as [map2 [af [vR [aiv [aerr sound_affine]]]]].
destruct sound_affine as [_ [Haiv [Hsup [_ [_ [_ [_ [Hee Heval]]]]]]]]. destruct sound_affine as [_ [_ [Haiv [Hsup [_ [_ [_ [_ [Hee [Heval _]]]]]]]]]].
exists aiv, aerr, vR. exists aiv, aerr, vR.
split; try split; try auto. split; try split; try auto.
apply AffineArith.to_interval_containment in Heval. apply AffineArith.to_interval_containment in Heval.
......
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