Commit e98bf643 authored by Joachim Bard's avatar Joachim Bard

fixing evalFma

parent 9a055ff5
......@@ -100,7 +100,7 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) P (validVars: NatSet.
olet valid3 := validAffineBounds e3 A P validVars exprsAf2 n2 in
let (exprsAf3, n3) := valid3 in
olet af3 := FloverMap.find e3 exprsAf3 in
updateExpMapSucc e (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 n3)) n3 exprsAf3 intv
updateExpMapSucc e (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 n3) af3) n3 exprsAf3 intv
| Downcast _ e' =>
olet valid' := validAffineBounds e' A P validVars exprsAf currentMaxNoise in
let (exprsAf', n') := valid' in
......@@ -1902,7 +1902,7 @@ Proof.
}
{ repeat set_tac. }
assert (af3' = af3) by congruence; subst.
destruct (isSupersetIntv (toIntv (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3))) aiv) eqn: Hsup; try congruence.
destruct (isSupersetIntv (toIntv (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3)) aiv) eqn: Hsup; try congruence.
inversion validBounds; subst; clear validBounds.
pose proof mult_aff_sound as multsound.
assert (fresh subnoise3 (afQ2R af1)) as fresh1 by now apply afQ2R_fresh;
......@@ -1913,7 +1913,7 @@ Proof.
assert (af_evals (afQ2R af1) vR1 ihmap3) as subaff1' by eauto using af_evals_map_extension.
assert (af_evals (afQ2R af2) vR2 ihmap3) as subaff2' by eauto using af_evals_map_extension.
assert (af_evals (afQ2R af3) vR3 ihmap3) as subaff3' by eauto using af_evals_map_extension.
specialize (multsound (afQ2R af2) (afQ2R af3) vR2 vR3 ihmap3 subnoise3 fresh2 fresh3 subaff2' subaff3') as [qMult multsound].
specialize (multsound (afQ2R af1) (afQ2R af2) vR1 vR2 ihmap3 subnoise3 fresh1 fresh2 subaff1' subaff2') as [qMult multsound].
assert (contained_map map1 (updMap ihmap3 subnoise3 qMult)).
{
etransitivity; try exact ihcont1.
......@@ -1922,39 +1922,37 @@ Proof.
apply contained_map_extension.
apply Hsubmapvalid3; lia.
}
assert (contained_flover_map iexpmap (FloverMap.add (Fma e1 e2 e3) (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)) subexprAff3)).
assert (contained_flover_map iexpmap (FloverMap.add (Fma e1 e2 e3) (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3) subexprAff3)).
{
pose proof contained_flover_map_extension as H'.
specialize (H' _ iexpmap _ (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)) Hvisited).
specialize (H' _ iexpmap _ (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3) Hvisited).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
clear H'.
etransitivity; try eassumption.
etransitivity; try eassumption.
}
assert (FloverMap.find (elt:=affine_form Q) (Fma e1 e2 e3) (FloverMap.add (Fma e1 e2 e3) (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)) subexprAff3) = Some (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)))
assert (FloverMap.find (elt:=affine_form Q) (Fma e1 e2 e3) (FloverMap.add (Fma e1 e2 e3) (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3) subexprAff3) = Some (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3))
by (rewrite FloverMapFacts.P.F.add_eq_o; try auto;
apply Q_orderedExps.exprCompare_refl).
assert (fresh (subnoise3 + 1) (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3))).
assert (fresh (subnoise3 + 1) (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3)).
{
rewrite <- afQ2R_fresh in fresh1.
rewrite <- afQ2R_fresh in fresh3.
apply AffineArithQ.plus_aff_fresh_compat.
{
apply fresh_monotonic with (n := subnoise3); try lia; auto.
}
unfold AffineArithQ.mult_aff.
destruct Qeq_bool.
- rewrite orb_true_l.
apply AffineArithQ.mult_aff_aux_fresh_compat;
apply fresh_inc; now rewrite afQ2R_fresh.
- destruct Qeq_bool.
+ rewrite orb_true_r.
apply AffineArithQ.mult_aff_aux_fresh_compat;
apply fresh_inc; now rewrite afQ2R_fresh.
+ simpl.
apply fresh_noise; try lia.
- unfold AffineArithQ.mult_aff.
destruct Qeq_bool.
+ rewrite orb_true_l.
apply AffineArithQ.mult_aff_aux_fresh_compat;
apply fresh_inc; now rewrite afQ2R_fresh.
+ destruct Qeq_bool.
* rewrite orb_true_r.
apply AffineArithQ.mult_aff_aux_fresh_compat;
apply fresh_inc; now rewrite afQ2R_fresh.
* simpl.
apply fresh_noise; try lia.
apply AffineArithQ.mult_aff_aux_fresh_compat;
apply fresh_inc; now rewrite afQ2R_fresh.
- apply fresh_monotonic with (n := subnoise3); try lia; auto.
}
assert (forall n : nat, (n >= subnoise3 + 1)%nat -> updMap ihmap3 subnoise3 qMult n = None).
{
......@@ -1974,7 +1972,7 @@ Proof.
- auto.
- auto.
- auto. }
assert (af_evals (afQ2R (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3))) (perturb (evalFma vR1 vR2 vR3) REAL 0) (updMap ihmap3 subnoise3 qMult)).
assert (af_evals (afQ2R (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3)) (perturb (evalFma vR1 vR2 vR3) REAL 0) (updMap ihmap3 subnoise3 qMult)).
{
unfold perturb.
unfold evalFma.
......@@ -1985,13 +1983,13 @@ Proof.
eapply af_evals_map_extension; try apply contained_map_extension; auto.
}
exists (updMap ihmap3 subnoise3 qMult),
(AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)),
(AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3),
(perturb (evalFma vR1 vR2 vR3) REAL 0)%R, aiv, aerr.
repeat split; auto.
+ lia.
+ apply validAffineBounds_validRanges.
exists (updMap ihmap3 subnoise3 qMult),
(AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)),
(AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3),
(perturb (evalFma vR1 vR2 vR3) REAL 0)%R, aiv, aerr.
repeat split; auto.
+ intros e Hnone Hsome.
......@@ -2002,7 +2000,7 @@ Proof.
destruct (FloverMapFacts.O.MO.eq_dec (Fma e1 e2 e3) e).
- assert (Q_orderedExps.exprCompare e (Fma e1 e2 e3) = Eq)
by (now rewrite Q_orderedExps.exprCompare_eq_sym).
exists (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)),
exists (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3),
(perturb (evalFma vR1 vR2 vR3) REAL 0)%R, aiv, aerr.
repeat split; eauto using fresh_monotonic, af_evals_map_extension.
+ rewrite usedVars_eq_compat; eauto; simpl.
......@@ -2014,7 +2012,7 @@ Proof.
repeat split; auto.
eapply validAffineBounds_validRanges.
exists (updMap ihmap3 subnoise3 qMult),
(AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)),
(AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3),
(perturb (evalFma vR1 vR2 vR3) REAL 0)%R, aiv, aerr.
repeat split; auto.
- destruct (FloverMap.find e subexprAff1).
......@@ -2034,7 +2032,7 @@ Proof.
}
* {
pose proof contained_flover_map_extension as H'.
specialize (H' _ subexprAff1 _ (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)) Hecont).
specialize (H' _ subexprAff1 _ (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3) Hecont).
eapply checked_expressions_contained with (map1 := ihmap1)
(expmap1 := subexprAff1)
(noise1 := subnoise1); eauto.
......@@ -2060,7 +2058,7 @@ Proof.
etransitivity; try exact ihcont3.
apply contained_map_extension; auto.
- pose proof contained_flover_map_extension as H'.
specialize (H' _ subexprAff2 _ (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)) Hecont).
specialize (H' _ subexprAff2 _ (AffineArithQ.plus_aff (AffineArithQ.mult_aff af1 af2 subnoise3) af3) Hecont).
eapply checked_expressions_contained with (map1 := ihmap2)
(expmap1 := subexprAff2)
(noise1 := subnoise2); eauto.
......
......@@ -305,7 +305,7 @@ Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
then DeltaMap (Fma (toRExp e1) (toRExp e2) (toRExp e3)) m
else None)
(Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
(Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + computeErrorR (e1F + e2F * e3F ) m)%R.
(Rabs (vR - vF) <= Rabs ((e1R * e2R - e1F * e2F) + (e3R - e3F)) + computeErrorR (e1F * e2F + e3F ) m)%R.
Proof.
intros e1_real e1_float e2_real e2_float e3_real e3_float fma_real fma_float.
inversion fma_real; subst;
......
......@@ -89,10 +89,10 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let upperBoundE3 := maxAbs ive3 in
let errIntv_prod := multIntv errIve2 errIve3 in
let mult_error_bound := (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in
let mAbs := (maxAbs (addIntv errIve1 errIntv_prod)) in
Qleb (err1 + mult_error_bound + computeErrorQ mAbs m) err
let errIntv_prod := multIntv errIve1 errIve2 in
let mult_error_bound := (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) in
let mAbs := (maxAbs (addIntv errIntv_prod errIve3)) in
Qleb (mult_error_bound + err3 + computeErrorQ mAbs m) err
| _, _, _ => false
end
else false
......@@ -1901,7 +1901,7 @@ Proof.
repeat rewrite <- Rabs_eq_Qabs in valid_error.
repeat rewrite Q2R_plus in valid_error.
repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
eapply Rle_trans; eauto.
eapply Rle_trans. 2: eauto.
apply Rplus_le_compat.
- eauto using Rle_trans, Rabs_triang, Rplus_le_compat, multiplicationErrorBounded.
- assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
......@@ -1913,9 +1913,9 @@ Proof.
assert (contained nR3 (Q2R e3lo, Q2R e3hi)) as contained_intv3 by auto.
pose proof (distance_gives_iv (a:=nR3) _ _ contained_intv3 err3_bounded)
as valid_err3.
pose proof (IntervalArith.interval_multiplication_valid _ _ valid_err2 valid_err3)
pose proof (IntervalArith.interval_multiplication_valid _ _ valid_err1 valid_err2)
as valid_err_mult.
pose proof (IntervalArith.interval_addition_valid _ _ valid_err1 valid_err_mult).
pose proof (IntervalArith.interval_addition_valid _ _ valid_err_mult valid_err3).
rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
apply computeErrorR_up.
apply contained_leq_maxAbs.
......
This diff is collapsed.
......@@ -1437,50 +1437,50 @@ Lemma fma_error_af_evals
contained_map noise_map noise_map' /\
(forall n, (noise + 6) <= n -> noise_map' n = None)%nat /\
fresh (noise + 6) (plus_aff
(plus_aff (afQ2R af1)
(subtract_aff
(plus_aff (subtract_aff
(plus_aff
(mult_aff (afQ2R (fromIntv iv2 noise)) (afQ2R af3) (noise + 2))
(mult_aff (afQ2R (fromIntv iv3 (noise + 1))) (afQ2R af2) (noise + 3)))
(mult_aff (afQ2R af2) (afQ2R af3) (noise + 4))))
(mult_aff (afQ2R (fromIntv iv1 noise)) (afQ2R af2) (noise + 2))
(mult_aff (afQ2R (fromIntv iv2 (noise + 1))) (afQ2R af1) (noise + 3)))
(mult_aff (afQ2R af1) (afQ2R af2) (noise + 4)))
(afQ2R af3))
(mkErrorPolyR
(computeErrorR (Q2R (maxAbs
(addIntv (widenIntv iv1 err1)
(multIntv (widenIntv iv2 err2)
(widenIntv iv3 err3))))) m)
(addIntv (multIntv (widenIntv iv1 err1)
(widenIntv iv2 err2))
(widenIntv iv3 err3)))) m)
(noise + 5))) /\
af_evals
(plus_aff
(plus_aff (afQ2R af1)
(subtract_aff
(plus_aff (subtract_aff
(plus_aff
(mult_aff (afQ2R (fromIntv iv2 noise)) (afQ2R af3) (noise + 2))
(mult_aff (afQ2R (fromIntv iv3 (noise + 1))) (afQ2R af2) (noise + 3)))
(mult_aff (afQ2R af2) (afQ2R af3) (noise + 4))))
(mult_aff (afQ2R (fromIntv iv1 noise)) (afQ2R af2) (noise + 2))
(mult_aff (afQ2R (fromIntv iv2 (noise + 1))) (afQ2R af1) (noise + 3)))
(mult_aff (afQ2R af1) (afQ2R af2) (noise + 4)))
(afQ2R af3))
(mkErrorPolyR
(computeErrorR (Q2R (maxAbs
(addIntv (widenIntv iv1 err1)
(multIntv (widenIntv iv2 err2)
(widenIntv iv3 err3))))) m)
(addIntv (multIntv (widenIntv iv1 err1)
(widenIntv iv2 err2))
(widenIntv iv3 err3)))) m)
(noise + 5)))
(v__R1 + v__R2 * v__R3 - perturb (v__FP1 + v__FP2 * v__FP3) m delta) noise_map'.
(v__R1 * v__R2 + v__R3 - perturb (v__FP1 * v__FP2 + v__FP3) m delta) noise_map'.
Proof.
intros Hevals1 Hevals2 Hevals3 Hfresh1 Hfresh2 Hfresh3; intros.
destruct (@af_evals_afQ2R_from_intv_updMap iv2 noise noise_map v__R2) as [q1 Hevalsiv1]; auto.
destruct (@af_evals_afQ2R_from_intv_updMap iv1 noise noise_map v__R1) as [q1 Hevalsiv1]; auto.
pose (noise_map1 := updMap noise_map noise q1).
assert (contained_map noise_map noise_map1)
by (apply contained_map_extension; auto).
assert (forall n', (noise + 1 <= n')%nat -> noise_map1 n' = None)
by (apply updMap_noise_incr; auto).
destruct (@af_evals_afQ2R_from_intv_updMap iv3 (noise + 1)%nat noise_map1 v__R3) as [q2 Hevalsiv2]; auto.
destruct (@af_evals_afQ2R_from_intv_updMap iv2 (noise + 1)%nat noise_map1 v__R2) as [q2 Hevalsiv2]; auto.
pose (noise_map2 := updMap noise_map1 (noise + 1)%nat q2).
assert (contained_map noise_map1 noise_map2)
by (apply contained_map_extension; auto).
assert (forall n', (noise + 1 + 1 <= n')%nat -> noise_map2 n' = None)
by (apply updMap_noise_incr; auto).
replace (noise + 1 + 1)%nat with (noise + 2)%nat in * by lia.
destruct (@mult_aff_sound (afQ2R (fromIntv iv2 noise)) (afQ2R af3) v__R2
(v__R3 - v__FP3) noise_map2 (noise + 2)%nat)%R as [q3 Hevalsmult1];
destruct (@mult_aff_sound (afQ2R (fromIntv iv1 noise)) (afQ2R af2) v__R1
(v__R2 - v__FP2) noise_map2 (noise + 2)%nat)%R as [q3 Hevalsmult1];
eauto using fresh_monotonic, af_evals_map_extension.
1: (rewrite <- afQ2R_fresh; apply fresh_from_intv; lia).
1: (eapply fresh_monotonic with (n := noise); eauto; lia).
......@@ -1490,8 +1490,8 @@ Proof.
assert (forall n', (noise + 2 + 1 <= n')%nat -> noise_map3 n' = None)
by (apply updMap_noise_incr; auto).
replace (noise + 2 + 1)%nat with (noise + 3)%nat in * by lia.
destruct (@mult_aff_sound (afQ2R (fromIntv iv3 (noise + 1))) (afQ2R af2) v__R3
(v__R2 - v__FP2) noise_map3 (noise + 3)%nat)%R as [q4 Hevalsmult2];
destruct (@mult_aff_sound (afQ2R (fromIntv iv2 (noise + 1))) (afQ2R af1) v__R2
(v__R1 - v__FP1) noise_map3 (noise + 3)%nat)%R as [q4 Hevalsmult2];
eauto using fresh_monotonic, af_evals_map_extension.
1: (rewrite <- afQ2R_fresh; apply fresh_from_intv; lia).
1: (eapply fresh_monotonic with (n := noise); eauto; lia).
......@@ -1501,7 +1501,7 @@ Proof.
assert (forall n', (noise + 3 + 1 <= n')%nat -> noise_map4 n' = None)
by (apply updMap_noise_incr; auto).
replace (noise + 3 + 1)%nat with (noise + 4)%nat in * by lia.
destruct (@mult_aff_sound (afQ2R af2) (afQ2R af3) (v__R2 - v__FP2) (v__R3 - v__FP3)
destruct (@mult_aff_sound (afQ2R af1) (afQ2R af2) (v__R1 - v__FP1) (v__R2 - v__FP2)
noise_map4 (noise + 4)%nat)%R as [q5 Hevalsmult3];
eauto using fresh_monotonic, af_evals_map_extension.
1-2: (eapply fresh_monotonic with (n := noise); eauto; lia).
......@@ -1515,16 +1515,16 @@ Proof.
replace (noise + 4 + 1)%nat with (noise + 5)%nat in * by lia.
apply af_evals_map_extension with (map2 := noise_map5) in Hevalsplus1; auto.
pose proof (subtract_aff_sound _ _ _ _ _ Hevalsplus1 Hevalsmult3) as Hevalsplus2.
apply af_evals_map_extension with (map2 := noise_map5) in Hevals1;
apply af_evals_map_extension with (map2 := noise_map5) in Hevals3;
eauto using contained_map_trans.
pose proof (plus_aff_sound _ _ _ _ _ Hevals1 Hevalsplus2) as Hevalsplus3.
pose proof (plus_aff_sound _ _ _ _ _ Hevalsplus2 Hevals3) as Hevalsplus3.
replace (noise + 6)%nat with (noise + 5 + 1)%nat by lia.
eapply plus_error_aff_af_evals with (noise_map' := noise_map5) (noise' := (noise + 5)%nat); eauto.
- field_rewrite ((v__R1 + v__R2 * v__R3) - (v__FP1 + v__FP2 * v__FP3) =
((v__R1 - v__FP1) + ((v__R2 * (v__R3 - v__FP3)) + (v__R3 * (v__R2 - v__FP2))
- ((v__R2 - v__FP2) * (v__R3 - v__FP3)))))%R; auto.
- field_rewrite ((v__R1 * v__R2 + v__R3) - (v__FP1 * v__FP2 + v__FP3) =
(((v__R1 * (v__R2 - v__FP2)) + (v__R2 * (v__R1 - v__FP1))
- ((v__R1 - v__FP1) * (v__R2 - v__FP2))) + (v__R3 - v__FP3)))%R; auto.
- apply plus_aff_fresh_compat;
[apply fresh_monotonic with (n := noise); eauto; lia|].
[|apply fresh_monotonic with (n := noise); eauto; lia].
apply plus_aff_fresh_compat.
+ apply plus_aff_fresh_compat;
apply mult_aff_fresh_compat; try lia.
......
......@@ -100,7 +100,7 @@ Definition evalUnop (o:unop) (v:R):=
end .
Definition evalFma (v1:R) (v2:R) (v3:R):=
evalBinop Plus v1 (evalBinop Mult v2 v3).
evalBinop Plus (evalBinop Mult v1 v2) v3.
(**
Define exprressions parametric over some value type V.
......
......@@ -86,7 +86,7 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P: FloverMap.t intv)
then
match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
| Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
let new_iv := addIntv iv1 (multIntv iv2 iv3) in
let new_iv := addIntv (multIntv iv1 iv2) iv3 in
isSupersetIntv new_iv intv
| _, _, _ => false
end
......@@ -355,11 +355,12 @@ Proof.
split; [auto | ].
* eapply Fma_dist' with (delta := 0%R); eauto; try congruence; cbn;
try rewrite Rabs_R0; try auto; lra.
* 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.
* pose proof (interval_multiplication_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_mul.
specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
remember (multInterval (Q2R (fst iv_f1), Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as iv_f12prod.
pose proof (interval_addition_valid (fst iv_f12prod, snd iv_f12prod)) (Q2R (fst iv_f3),Q2R (snd iv_f3)) as valid_add.
specialize (valid_add (vF1 * vF2)%R vF3 valid_mul valid_f3).
rewrite Heqiv_f12prod in valid_add, valid_mul.
unfold multIntv in valid_add.
canonize_hyps.
simpl in *.
......@@ -367,7 +368,6 @@ Proof.
repeat rewrite <- Q2R_min4, <- Q2R_max4 in *;
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, evalBinop, perturb.
lra.
- destruct types_defined
......
......@@ -193,7 +193,7 @@ Fixpoint smt_expr_eq (e: SMTArith) (e': expr Q) : bool :=
| Binop Sub e1' e2', MinusQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| Binop Mult e1' e2', TimesQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| Binop Div e1' e2', DivQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| Fma e1' e2' e3', PlusQ e1 (TimesQ e2 e3) =>
| Fma e1' e2' e3', PlusQ (TimesQ e1 e2) e3 =>
smt_expr_eq e1 e1' && smt_expr_eq e2 e2' && smt_expr_eq e3 e3'
| Downcast _ e', _ => smt_expr_eq e e'
| _, _ => false
......@@ -227,16 +227,17 @@ Proof.
destruct e, b; cbn; try discriminate; andb_to_prop Heq.
all: eapply (Binop_dist' (v1:=v1) (v2:=v2)); eauto.
- destruct e; try discriminate.
destruct e2; try discriminate.
destruct e1; try discriminate.
intros Heq H. andb_to_prop Heq.
fold smt_expr_eq in *.
inversion H; subst.
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
eapply (Binop_dist' (m1:=REAL) (m2:=REAL) (v1:=v1) (v2:= v2 * v3)); eauto.
2: discriminate.
eapply (Binop_dist' (m1:=REAL) (m2:=REAL) (v1:=v2) (v2:=v3)); eauto.
subst. unfold evalFma. cbn.
eapply (Binop_dist' (m1:=REAL) (m2:=REAL) (v1:=v1 * v2) (v2:= v3));
try discriminate; eauto.
eapply (Binop_dist' (m1:=REAL) (m2:=REAL) (v1:=v1) (v2:=v2)); eauto.
discriminate.
- cbn. intros Heq H.
inversion H; subst.
......
......@@ -237,8 +237,8 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
then
match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
| Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
let mult_iv := tightenBounds (Binop Mult f2 f3) (multIntv iv2 iv3) Q P L in
let new_iv := tightenBounds e (addIntv iv1 mult_iv) Q P L in
let mult_iv := tightenBounds (Binop Mult f1 f2) (multIntv iv1 iv2) Q P L in
let new_iv := tightenBounds e (addIntv mult_iv iv3) Q P L in
isSupersetIntv new_iv intv
| _, _, _ => false
end
......@@ -464,12 +464,12 @@ Proof.
try rewrite Rabs_R0; try auto; try lra; eauto. }
inversion env1; inversion env2; inversion env3; subst.
split; [auto | ].
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).
pose (mult_interval := tightenBounds (Binop Mult f2 f3) (multIntv iv_f2 iv_f3) Q P L).
pose proof (@interval_addition_valid (Q2R (fst iv_f1), Q2R (snd iv_f1))
(Q2R (fst mult_interval), Q2R (snd mult_interval))
vF1 (vF2 * vF3)) as valid_add.
pose proof (interval_multiplication_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_mul.
specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
pose (mult_interval := tightenBounds (Binop Mult f1 f2) (multIntv iv_f1 iv_f2) Q P L).
pose proof (@interval_addition_valid (Q2R (fst mult_interval), Q2R (snd mult_interval))
(Q2R (fst iv_f3), Q2R (snd iv_f3))
(vF1 * vF2) vF3) as valid_add.
unfold mult_interval in valid_add.
canonize_hyps.
eapply Rle_trans2; eauto.
......@@ -477,8 +477,8 @@ Proof.
cbn in *. rewrite ?Q2R_min4, ?Q2R_max4, ?Q2R_plus.
apply valid_add; auto.
assert (Heval_mult: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
(Binop Mult (toREval (toRExp f2)) (toREval (toRExp f3)))
(vF2 * vF3) REAL).
(Binop Mult (toREval (toRExp f1)) (toREval (toRExp f2)))
(vF1 * vF2) REAL).
{ eapply Binop_dist' with (delta := 0%R); try congruence;
try rewrite Rabs_R0; cbn; try lra; try reflexivity; eauto. }
eapply tightenBounds_sound; eauto using inlineLets_sound.
......
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