Commit 41b255c9 authored by Heiko Becker's avatar Heiko Becker

Port interval validation to finite maps, simplify proofs on the way

parent 6350c89b
......@@ -21,11 +21,13 @@ Ltac canonize_Q_prop :=
match goal with
| [ H: Qle_bool ?a ?b = true |- _] => rewrite Qle_bool_iff in H
| [ H: Qleb ?a ?b = true |- _ ] => rewrite Qle_bool_iff in H
| [ H: Qeq_bool ?a ?b = true |- _] => rewrite Qeq_bool_iff in H
end.
Ltac canonize_Q_to_R :=
match goal with
| [ H: (?a <= ?b)%Q |- _ ] => apply Qle_Rle in H
| [ H: (?a == ?b)%Q |- _ ] => apply Qeq_eqR in H
| [ H: context [Q2R 0] |- _ ] => rewrite Q2R0_is_0 in H
| [ |- context [Q2R 0] ] => rewrite Q2R0_is_0
end.
......@@ -44,51 +46,72 @@ Ltac Q2R_to_head_step :=
Ltac Q2R_to_head := repeat Q2R_to_head_step.
Ltac NatSet_simp hyp :=
try rewrite NatSet.mem_spec in hyp;
try rewrite NatSet.equal_spec in hyp;
try rewrite NatSet.subset_spec in hyp;
try rewrite NatSet.empty_spec in hyp;
try rewrite NatSet.is_empty_spec in hyp;
try rewrite NatSet.add_spec in hyp;
try rewrite NatSet.remove_spec in hyp;
try rewrite NatSet.singleton_spec in hyp;
try rewrite NatSet.union_spec in hyp;
try rewrite NatSet.inter_spec in hyp;
try rewrite NatSet.diff_spec in hyp.
Ltac NatSet_prop :=
match goal with
| [ H : true = true |- _ ] => clear H; NatSet_prop
| [ H: ?T = true |- _ ] => NatSet_simp H;
(apply Is_true_eq_left in H; NatSet_prop; apply Is_true_eq_true in H) || NatSet_prop
| _ => try auto
Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
match v with
|Some val => f val
| None => e
end.
Ltac match_simpl :=
Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
match v with |Some val => f val | None => e end = optionLift X Y v f e.
Proof.
cbv; auto.
Qed.
Lemma optionLift_cond X (a:bool) (b c :X):
(if a then b else c) = match a with |true => b |false => c end.
Proof.
cbv; auto.
Qed.
Ltac remove_matches := rewrite optionLift_eq in *.
Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *.
Ltac match_factorize :=
match goal with
| [ H: ?t = ?u |- context [match ?t with _ => _ end]] => rewrite H; simpl
| [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]]
=> rewrite H; cbn
| [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ]
=> rewrite H1 in H2; cbn in H2
| [ H: context [optionLift _ _ ?t _ _] |- _ ]
=> destruct t eqn:?; cbn in H; try congruence
| [ |- context [optionLift _ _ ?t _ _] ]
=> destruct t eqn:?; cbn; try congruence
end.
Ltac destruct_if :=
Ltac pair_factorize :=
match goal with
| [H: if ?c then ?a else ?b = _ |- _ ] =>
case_eq ?c;
let name := fresh "cond" in
intros name;
rewrite name in *;
try congruence
| [H: _ |- if ?c then ?a else ?b = _] =>
case_eq ?c;
let name := fresh "cond" in
intros name;
rewrite name in *;
try congruence
end.
(* HOL4 Style patter matching tactics *)
Tactic Notation "lift " tactic(t) :=
fun H => t H.
| [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H
end.
Ltac match_simpl :=
try remove_conds;
try remove_matches;
repeat match_factorize;
try pair_factorize.
(* Ltac destruct_if := *)
(* match goal with *)
(* | [H: if ?c then ?a else ?b = _ |- _ ] => *)
(* case_eq ?c; *)
(* let name := fresh "cond" in *)
(* intros name; *)
(* rewrite name in *; *)
(* try congruence *)
(* | [H: _ |- if ?c then ?a else ?b = _] => *)
(* case_eq ?c; *)
(* let name := fresh "cond" in *)
(* intros name; *)
(* rewrite name in *; *)
(* try congruence *)
(* end. *)
(* Ltac match_destr t:= *)
(* match goal with *)
(* | H: context [optionLift (DaisyMap.find ?k ?M) _ _] |- _ => *)
(* destruct (DaisyMap.find (elt:=intv * error) k M); idtac H *)
(* end. *)
Tactic Notation "match_pat" open_constr(pat) tactic(t) :=
match goal with
......
......@@ -72,24 +72,39 @@ Proof.
destruct x_in_add as [ x_eq | [x_neq x_in_S]]; auto.
Qed.
(** TODO: Merge with NatSet_prop tactic in Ltacs file **)
Ltac set_hnf_tac :=
Ltac set_bool_to_prop :=
match goal with
| [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H
| [ H: NatSet.mem ?x _ = false |- _] => apply not_in_not_mem in H
| [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec
end.
Ltac solve_simple_sets :=
match goal with
| [ H: NatSet.In ?x ?S1 |- NatSet.In ?x (NatSet.union ?S1 ?S2)]
=> rewrite NatSet.union_spec; auto
end.
Ltac set_hnf_tac :=
match goal with
| [ H: context [NatSet.In ?x (NatSet.diff ?A ?B)] |- _] => rewrite NatSet.diff_spec in H; destruct H
| [ H: NatSet.Subset ?SA ?SB |- NatSet.In ?v ?SB] => apply H
| [ H: NatSet.In ?x (NatSet.singleton ?y) |- _] => apply NatSetProps.Dec.F.singleton_1 in H
| [ H: NatSet.In ?x NatSet.empty |- _ ] => inversion H
| [ H: NatSet.In ?x (NatSet.union ?S1 ?S2) |- _ ] => rewrite NatSet.union_spec in H
| [ H: NatSet.In ?x (NatSet.add ?y ?S) |- _ ] => rewrite NatSet.add_spec_strong in H
| [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec
| [ H: NatSet.In ?x (NatSet.add ?y ?S) |- _ ] => rewrite add_spec_strong in H
| [ |- context [NatSet.In ?x (NatSet.union ?SA ?SB)]] => rewrite NatSet.union_spec
| [ |- context [NatSet.In ?x (NatSet.diff ?A ?B)]] => rewrite NatSet.diff_spec
| [ |- context [NatSet.In ?x (NatSet.singleton ?y)]] => rewrite NatSet.singleton_spec
| [ |- context [NatSet.In ?x (NatSet.remove ?y ?S)]] => rewrite NatSet.remove_spec
| [ |- context [NatSet.In ?x (NatSet.add ?y ?S)]] => rewrite NatSet.add_spec
| [ |- context [NatSet.Subset ?SA ?SB]] => hnf; intros
end.
Ltac set_tac :=
repeat set_hnf_tac;
simpl in *; try auto.
repeat set_bool_to_prop;
repeat solve_simple_sets;
repeat set_hnf_tac;
simpl in *;
repeat solve_simple_sets;
try auto.
......@@ -105,24 +105,21 @@ Theorem ivbounds_approximatesPrecond_sound f A P dVars iv err:
Proof.
induction f; cbn; intros approx_true var var_in_fV find_A; set_tac.
- subst.
rewrite find_A in *.
match_simpl.
destruct (var mem dVars) eqn:?; set_tac; try congruence.
andb_to_prop approx_true; unfold isSupersetIntv.
apply andb_prop_intro; split;
apply Is_true_eq_left; auto.
- destruct (DaisyMap.find (Unop u f) A) as [[iv_u err_u] | ] eqn:?;
try congruence.
- match_simpl.
andb_to_prop approx_true.
apply IHf; try auto.
set_tac.
- destruct (DaisyMap.find (Binop b f1 f2) A) as [[iv_b err_b] | ] eqn:?;
try congruence.
- match_simpl.
andb_to_prop approx_true.
destruct H.
+ apply IHf1; try auto; set_tac.
+ apply IHf2; try auto; set_tac.
- destruct (DaisyMap.find (Downcast m f) A) as [[iv_m err_m] | ] eqn:?;
try congruence.
- match_simpl.
andb_to_prop approx_true.
apply IHf; try auto; set_tac.
Qed.
......@@ -139,113 +136,116 @@ Proof.
unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto.
Qed.
Ltac env_assert A e name :=
assert (exists iv err, A e = (iv,err)) as name by (destruct (A e); repeat eexists; auto).
Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
A e2 = ((ivlo_e2,ivhi_e2), err) ->
DaisyMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) ->
validIntervalbounds (Binop Div e1 e2) A P V = true ->
(ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
intros A_eq validBounds.
unfold validIntervalbounds in validBounds.
env_assert A (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]].
env_assert A e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]].
rewrite abs_div, abs_e1, A_eq in validBounds.
repeat (rewrite <- andb_lazy_alt in validBounds).
apply Is_true_eq_left in validBounds.
apply andb_prop_elim in validBounds.
destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds.
destruct validBounds as [nodiv0 _].
apply Is_true_eq_true in nodiv0.
intros A_eq validBounds; cbn in *.
match_simpl.
andb_to_prop validBounds.
repeat match_simpl.
andb_to_prop R.
unfold isSupersetIntv in *; simpl in *.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
forall v, NatSet.In v dVars ->
exists vR ivlo ivhi err,
E v = Some vR /\
DaisyMap.find (Var Q v) A = Some ((ivlo, ivhi), err) /\
(Q2R ivlo <= vR <= Q2R ivhi)%R.
Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
forall v,
NatSet.In v fVars ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.
Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m :mType, Gamma v = Some m.
Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
fVars dVars (E:env) Gamma:
validIntervalbounds f A P dVars = true ->
(forall v, NatSet.mem v dVars = true ->
exists vR, E v = Some vR /\
(Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R) ->
dVars_range_valid dVars E A ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v, NatSet.mem v (NatSet.union fVars dVars) = true ->
exists m :mType, Gamma v = Some m) ->
exists vR, eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\
(Q2R (fst (fst (A f))) <= vR <= Q2R (snd (fst (A f))))%R.
fVars_P_sound fVars E P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
exists ivlo ivhi err vR,
DaisyMap.find f A = Some ((ivlo, ivhi), err) /\
eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\
(Q2R ivlo <= vR <= Q2R ivhi)%R.
Proof.
induction f;
intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
simpl in *.
- env_assert A (Var Q n) A_var.
destruct A_var as [iv_n [err_n A_var]].
case_eq (NatSet.mem n dVars); intros dVars_case;
rewrite dVars_case, A_var in valid_bounds; simpl in *.
+ destruct (valid_definedVars n) as [vR [env_valid bounds_valid]]; try auto.
eexists; split; simpl; try eauto.
cbn in *.
- match_simpl.
destruct (NatSet.mem n dVars) eqn:?; simpl in *.
+ destruct (valid_definedVars n)
as [vR [ivlo_n [ivhi_n [err_n [env_valid [map_n bounds_valid]]]]]];
try set_tac.
rewrite map_n in *.
inversion Heqo; subst.
exists ivlo_n, ivhi_n, e; eexists; split; [auto| split; try eauto ].
eapply Var_load; simpl; try auto.
destruct (types_defined n) as [m type_m];
set_tac.
match_simpl; auto.
+ destruct (valid_freeVars n) as [vR [env_valid bounds_valid]]; set_tac; try auto.
+ destruct (valid_freeVars n) as [vR [env_valid bounds_valid]];
set_tac; try auto.
assert (NatSet.In n fVars) by set_tac.
eexists; split; [econstructor | ]; eauto.
* destruct (types_defined n) as [m type_m]; set_tac.
andb_to_prop valid_bounds.
canonize_hyps; simpl in *.
exists (fst i), (snd i), e; eexists; split;
[destruct i; auto | split].
* econstructor; try eauto.
destruct (types_defined n) as [m type_m]; set_tac.
match_simpl; auto.
* andb_to_prop valid_bounds.
unfold Qleb in *.
canonize_hyps.
rewrite A_var.
simpl in *.
lra.
- exists (perturb (Q2R v) 0).
split; [econstructor; eauto; apply Rabs_0_equiv | ].
env_assert A (Const m v) A_const;
destruct A_const as [iv_v [err_v A_const]].
rewrite A_const in *; simpl in *.
* lra.
- match_simpl.
andb_to_prop valid_bounds.
canonize_hyps.
simpl in *; unfold perturb; lra.
- env_assert A (Unop u f) A_unop;
destruct A_unop as [iv_u [err_u A_unop]].
rewrite A_unop in *; simpl in *.
case_eq (validIntervalbounds f A P dVars);
intros case_bounds; rewrite case_bounds in *; try congruence.
env_assert A f A_f;
destruct A_f as [iv_f [ err_f A_f]]; rewrite A_f in *; simpl in *.
destruct IHf as [vF [eval_f valid_bounds_f]]; try auto.
destruct u.
+ exists (evalUnop Neg vF); split; [econstructor; auto | ].
(* TODO: Make lemma *)
unfold isSupersetIntv in valid_bounds;
andb_to_prop valid_bounds.
canonize_hyps.
simpl in *.
canonize_hyps; simpl in *.
exists (fst i), (snd i), e, (perturb (Q2R v) 0).
split; [destruct i; auto| split].
+ econstructor; try eauto. apply Rabs_0_equiv.
+ unfold perturb; simpl; lra.
- match_simpl.
andb_to_prop valid_bounds.
match_simpl.
destruct IHf as [ivlo_f [ivhi_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]]];
try auto.
destruct u; try andb_to_prop R.
+ exists (fst i), (snd i), e, (evalUnop Neg vF); split;
[destruct i; auto | split ;
[econstructor; eauto | ]].
canonize_hyps; simpl in *.
rewrite Q2R_opp in *.
lra.
+ andb_to_prop valid_bounds.
rename L into nodiv0.
destruct valid_bounds_f.
inversion iveq_f; subst; simpl in *; lra.
+ inversion iveq_f; subst; simpl in *.
rename L0 into nodiv0.
apply le_neq_bool_to_lt_prop in nodiv0.
exists (perturb (evalUnop Inv vF) 0); split; [econstructor; eauto; try apply Rabs_0_equiv | ].
* (* Absence of division by zero *)
exists (fst i), (snd i), e, (perturb (evalUnop Inv vF) 0); split;
[destruct i; auto | split].
* econstructor; eauto; try apply Rabs_0_equiv.
(* Absence of division by zero *)
hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
rewrite Q2R0_is_0 in nodiv0; lra.
* canonize_hyps.
pose proof (interval_inversion_valid (Q2R (fst iv_f),(Q2R (snd iv_f))) (a :=vF)) as inv_valid.
pose proof (interval_inversion_valid ((Q2R ivlo_f),(Q2R ivhi_f)) (a :=vF)) as inv_valid.
unfold invertInterval in inv_valid; simpl in *.
rewrite delta_0_deterministic; [| rewrite Rbasic_fun.Rabs_R0; lra].
destruct inv_valid; try auto.
{ destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
{ split; eapply Rle_trans.
- apply L0.
- apply L1.
- rewrite Q2R_inv; try auto.
destruct nodiv0; try lra.
hnf; intros.
assert (0 < Q2R (snd iv_f))%R.
assert (0 < Q2R (ivhi_f))%R.
{ eapply Rlt_le_trans.
apply Qlt_Rlt in H1.
rewrite <- Q2R0_is_0.
......@@ -258,7 +258,7 @@ Proof.
- rewrite <- Q2R_inv; try auto.
hnf; intros.
destruct nodiv0; try lra.
assert (Q2R (fst iv_f) < 0)%R.
assert (Q2R ivlo_f < 0)%R.
{ eapply Rle_lt_trans.
Focus 2.
rewrite <- Q2R0_is_0;
......@@ -267,58 +267,55 @@ Proof.
}
rewrite <- Q2R0_is_0 in H3.
apply Rlt_Qlt in H3. lra. }
- env_assert A (Binop b f1 f2) A_b;
destruct A_b as [iv_b [err_b A_b]].
env_assert A f1 A_f1;
destruct A_f1 as [iv_f1 [err_f1 A_f1]].
env_assert A f2 A_f2;
destruct A_f2 as [iv_f2 [err_f2 A_f2]].
rewrite A_b in *; simpl in *.
- match_simpl.
andb_to_prop valid_bounds.
destruct IHf1 as [vF1 [eval_f1 valid_f1]]; try auto; set_tac.
destruct IHf2 as [vF2 [eval_f2 valid_f2]]; try auto; set_tac.
rewrite A_f1, A_f2 in *; simpl in *.
repeat match_simpl.
destruct IHf1 as [ivlo_f1 [ivhi_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]];
try auto; set_tac.
destruct IHf2 as [ivlo_f2 [ivhi_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]];
try auto; set_tac.
assert (M0 = join M0 M0) as M0_join by (cbv; auto);
rewrite M0_join.
exists (perturb (evalBinop b vF1 vF2) 0);
exists (fst i), (snd i), e, (perturb (evalBinop b vF1 vF2) 0);
split; [destruct i; auto | ].
inversion env1; inversion env2; subst.
destruct b; simpl in *.
* split;
[econstructor; try congruence; apply Rabs_0_equiv | ].
pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_add.
pose proof (interval_addition_valid ((Q2R ivlo_f1), Q2R ivhi_f1)
(Q2R ivlo_f2, Q2R ivhi_f2)) as valid_add.
specialize (valid_add vF1 vF2 valid_f1 valid_f2).
unfold isSupersetIntv in R.
andb_to_prop R.
canonize_hyps.
simpl in *.
canonize_hyps; simpl in *.
repeat rewrite <- Q2R_plus in *;
rewrite <- Q2R_min4, <- Q2R_max4 in *.
unfold perturb.
lra.
unfold perturb. lra.
* split;
[econstructor; try congruence; apply Rabs_0_equiv |].
pose proof (interval_subtraction_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_sub.
pose proof (interval_subtraction_valid (Q2R ivlo_f1, Q2R ivhi_f1)
(Q2R ivlo_f2, Q2R ivhi_f2))
as valid_sub.
specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
unfold isSupersetIntv in R.
andb_to_prop R.
canonize_hyps.
simpl in *.
canonize_hyps; simpl in *.
repeat rewrite <- Q2R_opp in *;
repeat rewrite <- Q2R_plus in *;
rewrite <- Q2R_min4, <- Q2R_max4 in *.
unfold perturb.
lra.
unfold perturb; lra.
* split;
[ econstructor; try congruence; apply Rabs_0_equiv |].
pose proof (interval_multiplication_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_mul.
pose proof (interval_multiplication_valid (Q2R ivlo_f1, Q2R ivhi_f1)
(Q2R ivlo_f2, Q2R ivhi_f2))
as valid_mul.
specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
unfold isSupersetIntv in R.
andb_to_prop R.
canonize_hyps.
simpl in *.
canonize_hyps; simpl in *.
repeat rewrite <- Q2R_mult in *;
rewrite <- Q2R_min4, <- Q2R_max4 in *.
unfold perturb.
lra.
unfold perturb; lra.
* andb_to_prop R.
canonize_hyps.
apply le_neq_bool_to_lt_prop in L.
......@@ -327,17 +324,20 @@ Proof.
(* No division by zero proof *)
{ hnf; intros.
destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. }
{ pose proof (interval_division_valid (a:=vF1) (b:=vF2) (Q2R (fst iv_f1), Q2R (snd iv_f1)) (Q2R (fst iv_f2),Q2R (snd iv_f2))) as valid_div.
{ pose proof (interval_division_valid (a:=vF1) (b:=vF2)
(Q2R ivlo_f1, Q2R ivhi_f1)
(Q2R ivlo_f2, Q2R ivhi_f2))
as valid_div.
simpl in *.
destruct valid_div; try auto.
- destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
- assert (~ snd iv_f2 == 0).
- assert (~ ivhi_f2 == 0).
{ hnf; intros. destruct L; try lra.
assert (0 < snd iv_f2) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra).
assert (0 < ivhi_f2) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra).
lra. }
assert (~ fst iv_f2 == 0).
assert (~ ivlo_f2 == 0).
{ hnf; intros; destruct L; try lra.
assert (fst iv_f2 < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra).
assert (ivlo_f2 < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra).
lra. }
repeat (rewrite <- Q2R_inv in *; try auto).
repeat rewrite <- Q2R_mult in *.
......@@ -345,18 +345,18 @@ Proof.
unfold perturb.
lra.
}
- env_assert A (Downcast m f) A_d;
destruct A_d as [iv_d [err_d A_d]];
env_assert A f A_f;
destruct A_f as [iv_f [err_f A_f]];
rewrite A_d, A_f in *; simpl in *.
- match_simpl.
andb_to_prop valid_bounds.
destruct IHf as [vF [eval_f valid_f]]; try auto.
exists (perturb vF 0).
match_simpl.
destruct IHf as [ivlo_f [ivhi_f [err_f [vF [env_f [eval_f valid_f]]]]]];
try auto.
inversion env_f; subst.
exists (fst i), (snd i), e, (perturb vF 0).
split; [destruct i; try auto |].
split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |].
canonize_hyps.
unfold perturb; simpl in *.
lra.
unfold isSupersetIntv in *; andb_to_prop R.
canonize_hyps; simpl in *.
unfold perturb; lra.
Qed.
Lemma Rmap_updVars_comm Gamma n m:
......@@ -367,24 +367,6 @@ Proof.
intros x; destruct (x =? n); try auto.
Qed.
(* Lemma eval_exp_Rmap_updVars_comm e n Gamma E v: *)
(* eval_exp E (toRMap (updDefVars n M0 Gamma)) (toREval (toRExp e)) v M0 -> *)
(* eval_exp E (updDefVars n M0 (toRMap Gamma)) (toREval (toRExp e)) v M0. *)
(* Proof. *)
(* revert v; *)
(* induction e; intros * eval_e; inversion eval_e; subst; simpl in *; *)
(* auto. *)
(* - constructor; try auto. *)
(* erewrite test3; eauto. *)
(* - rewrite H2 in *. *)
(* apply M0_join_is_M0 in H2. *)
(* destruct H2; subst. *)
(* eauto. *)
(* - apply M0_least_precision in H1; subst. *)
(* econstructor; try eauto. *)
(* apply isMorePrecise_refl. *)
(* Qed. *)
Lemma swap_Gamma_eval_exp e E vR m Gamma1 Gamma2:
(forall n, Gamma1 n = Gamma2 n) ->
eval_exp E Gamma1 e vR m ->
......@@ -418,95 +400,78 @@ Proof.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma:
forall E fVars dVars outVars elo ehi err P,
forall E fVars dVars outVars P,
ssa f (NatSet.union fVars dVars) outVars ->
(forall v, NatSet.mem v dVars = true ->
exists vR, E v = Some vR /\
(Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R) ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v, NatSet.mem v (NatSet.union fVars dVars) = true ->
exists m :mType, Gamma v = Some m) ->
dVars_range_valid dVars E A ->
fVars_P_sound fVars E P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd f A P dVars = true ->
A (getRetExp f) = ((elo, ehi), err) ->
exists vR,
exists elo ehi err vR,
DaisyMap.find (getRetExp f) A = Some ((elo, ehi), err) /\
bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\