Commit 9489c9c8 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Fix merge errors in IntervalValidation

parent 81e8172d
......@@ -68,15 +68,16 @@ Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars
end
else false
| Fma f1 f2 f3 =>
if ((validIntervalbounds f1 absenv P validVars) &&
(validIntervalbounds f2 absenv P validVars) &&
(validIntervalbounds f3 absenv P validVars))
if ((validIntervalbounds f1 A P validVars) &&
(validIntervalbounds f2 A P validVars) &&
(validIntervalbounds f3 A P validVars))
then
let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in
let (iv3,_) := absenv f3 in
let new_iv := addIntv iv1 (multIntv iv2 iv3) in
isSupersetIntv new_iv intv
match DaisyMap.find f1 A, DaisyMap.find f2 A, DaisyMap.find f3 A with
| Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
let new_iv := addIntv iv1 (multIntv iv2 iv3) in
isSupersetIntv new_iv intv
| _, _, _ => false
end
else false
| Downcast _ f1 =>
if (validIntervalbounds f1 A P validVars)
......@@ -129,31 +130,13 @@ Proof.
destruct H.
+ apply IHf1; try auto; set_tac.
+ apply IHf2; try auto; set_tac.
- intros approx_fma_true v v_in_fV.
simpl in v_in_fV.
rewrite NatSet.diff_spec in v_in_fV.
destruct v_in_fV as [ v_in_fV v_not_in_V].
repeat rewrite NatSet.union_spec in v_in_fV.
apply Is_true_eq_left in approx_fma_true.
destruct (absenv (Fma f1 f2 f3)); destruct (absenv f1);
destruct (absenv f2); destruct (absenv f3); simpl in *.
apply andb_prop_elim in approx_fma_true.
destruct approx_fma_true.
apply andb_prop_elim in H.
destruct H.
apply andb_prop_elim in H.
- Daisy_compute; try congruence.
destruct H.
destruct v_in_fV.
+ apply IHf1; try auto.
* apply Is_true_eq_true; auto.
* rewrite NatSet.diff_spec; split; auto.
+ destruct H3.
* apply IHf2; try auto.
++ apply Is_true_eq_true; auto.
++ rewrite NatSet.diff_spec; split; auto.
* apply IHf3; try auto.
++ apply Is_true_eq_true; auto.
++ rewrite NatSet.diff_spec; split; auto.
+ apply IHf1; try auto; set_tac.
+ set_tac.
destruct H.
* apply IHf2; try auto; set_tac.
* apply IHf3; try auto; set_tac.
- Daisy_compute; try congruence.
apply IHf; try auto; set_tac.
Qed.
......@@ -381,32 +364,23 @@ Proof.
unfold perturb.
lra.
}
- env_assert absenv (Fma f1 f2 f3) absenv_fma;
destruct absenv_fma as [iv_fma [err_fma absenv_fma]].
env_assert absenv f1 absenv_f1;
destruct absenv_f1 as [iv_f1 [err_f1 absenv_f1]].
env_assert absenv f2 absenv_f2;
destruct absenv_f2 as [iv_f2 [err_f2 absenv_f2]].
env_assert absenv f3 absenv_f3;
destruct absenv_f3 as [iv_f3 [err_f3 absenv_f3]].
rewrite absenv_fma in *; simpl in *.
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.
destruct IHf3 as [vF3 [eval_f3 valid_f3]]; try auto; set_tac.
rewrite absenv_f1, absenv_f2, absenv_f3 in *; simpl in *.
- Daisy_compute; try congruence.
destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]; try auto; set_tac.
destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]; try auto; set_tac.
destruct IHf3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]]; try auto; set_tac.
assert (M0 = join3 M0 M0 M0) as M0_join by (cbv; auto);
rewrite M0_join.
exists (perturb (evalFma vF1 vF2 vF3) 0); split.
* econstructor; try congruence. apply Rabs_0_equiv.
kill_trivial_exists.
exists (perturb (evalFma vF1 vF2 vF3) 0); split; try auto.
inversion env1; inversion env2; inversion env3; subst.
split; [auto | ].
* econstructor; try congruence; apply Rabs_0_equiv.
* pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
rewrite Heqiv_f23prod in valid_add, valid_mul.
unfold multIntv in valid_add.
unfold isSupersetIntv in R.
andb_to_prop R.
canonize_hyps.
simpl in *.
repeat rewrite <- Q2R_mult in *;
......@@ -414,9 +388,7 @@ Proof.
repeat rewrite <- Q2R_plus in *;
repeat rewrite <- Q2R_min4, <- Q2R_max4 in *.
specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
unfold evalFma.
unfold evalBinop.
unfold perturb.
unfold evalFma, evalBinop, perturb.
lra.
- match_simpl.
andb_to_prop valid_bounds.
......
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