Commit 72e60f72 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Correct points raised in the discussion of #154

parent ef225811
......@@ -160,11 +160,11 @@ Proof.
* 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 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 Is_true_eq_true; auto.
++ rewrite NatSet.diff_spec; split; auto.
- intros approx_rnd_true v v_in_fV.
simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f).
apply Is_true_eq_left in approx_rnd_true.
......@@ -186,21 +186,6 @@ Proof.
unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto.
Qed.
(**
Technical definition to help prove soundess for FMA
**)
Definition multIntv (iv1:intv) (iv2:intv) :=
(
min4 (Q2R ((fst iv1) * (fst iv2)))
(Q2R ((fst iv1) * (snd iv2)))
(Q2R ((snd iv1) * (fst iv2)))
(Q2R ((snd iv1) * (snd iv2))),
max4 (Q2R ((fst iv1) * (fst iv2)))
(Q2R ((fst iv1) * (snd iv2)))
(Q2R ((snd iv1) * (fst iv2)))
(Q2R ((snd iv1) * (snd iv2)))
).
Ltac env_assert absenv e name :=
assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
......@@ -426,9 +411,9 @@ Proof.
* 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 (multIntv iv_f2 iv_f3) as iv_f23prod.
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.
rewrite Heqiv_f23prod in valid_add, valid_mul.
unfold multIntv in valid_add.
unfold isSupersetIntv in R.
andb_to_prop R.
......
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