Commit b93f1500 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'affine_arithmetic' into 'affine_arithmetic'

Affine arithmetic

See merge request AVA/FloVer!6
parents 2f5806c3 c5a76189
(*
Formalization of Affine Arithmetic for FloVer. Original author: Raphael Monat.
*)
Require Import Coq.Reals.Reals Coq.QArith.Qreals Coq.Lists.List Coq.micromega.Psatz.
Require Import Recdef.
Require Import Flover.AffineForm Flover.Infra.Abbrevs Flover.Infra.RealSimps Flover.Infra.Ltacs Flover.IntervalArith.
Open Scope R.
Ltac Rrewrite H := assert H as tmp by (try field; try lra); rewrite tmp; clear tmp.
Fixpoint radius (a: affine_form R): R := match a with
| Const v => 0
| Noise _ v a' => (Rabs v) + radius a'
end.
Lemma radius_nonneg (a: affine_form R):
0 <= radius a.
Proof.
induction a; simpl in *; try lra.
assert (0 = 0 + 0) as tmp by lra; rewrite tmp; clear tmp.
eapply Rplus_le_compat; try assumption.
apply Rabs_pos.
Qed.
Definition toInterval (a: affine_form R): interval := mkInterval (get_const a - radius a) (get_const a + radius a).
Lemma valid_to_interval (af: affine_form R):
valid (toInterval af).
Proof.
unfold valid.
unfold toInterval.
simpl.
pose proof (radius_nonneg af).
apply Rplus_le_compat; try lra.
Qed.
Definition fromInterval (iv: interval) (noise: nat): affine_form R :=
let ivMid := (IVhi iv / 2) + (IVlo iv / 2) in
let ivRad := Rmax (ivMid - (IVlo iv)) ((IVhi iv) - ivMid) in
if Req_dec_sum (IVlo iv) (IVhi iv) then Const ivMid
else Noise noise ivRad (Const (ivMid)).
Lemma to_from_interval_eq (iv: interval) (n: nat):
valid iv ->
(toInterval (fromInterval iv n)) = iv.
Proof.
intros vld.
unfold valid, fromInterval, toInterval in *.
unfold IVlo, IVhi in vld.
destruct iv as (l, r).
simpl in *.
destruct (Req_dec_sum l r) as [H | H]; simpl in *.
- subst; f_equal; lra.
- apply Rmax_case_strong; intros; rewrite Rabs_pos_eq; try lra; f_equal; lra.
Qed.
Lemma to_interval_functional a x1 x2:
toInterval a = x1 -> toInterval a = x2 -> x1 = x2.
Proof.
congruence.
Qed.
Definition above_zero a := 0 < (IVlo (toInterval a)).
Definition below_zero a := (IVhi (toInterval a)) < 0.
Lemma above_zero_monotone a n v :
above_zero (Noise n v a) -> above_zero a.
Proof.
unfold above_zero.
simpl.
intros noise.
unfold Qminus in *.
pose proof (Rabs_pos v) as nnabs.
pose proof (radius_nonneg a) as nnrad.
lra.
Qed.
Lemma above_IVhi a:
above_zero a -> IVhi (toInterval a) > 0.
Proof.
unfold above_zero.
pose proof (valid_to_interval a) as validiv.
unfold valid in validiv.
lra.
Qed.
Lemma below_zero_monotone a n v :
below_zero (Noise n v a) -> below_zero a.
Proof.
unfold below_zero.
simpl.
intros noise.
pose proof (Rabs_pos v) as nnabs.
pose proof (radius_nonneg a) as nnrad.
lra.
Qed.
Lemma below_IVlo a:
below_zero a -> IVlo (toInterval a) < 0.
Proof.
unfold below_zero.
pose proof (valid_to_interval a) as validiv.
unfold valid in validiv.
lra.
Qed.
Definition noise_type := {q: R | -(1) <= q /\ q <= 1}.
Definition noise_val (q: noise_type): R := proj1_sig q.
Coercion noise_val : noise_type >-> R.
Lemma zero_is_valid_noise:
-1 <= 0 <= 1.
Proof.
lra.
Qed.
Lemma one_is_valid_noise:
-1 <= 1 <= 1.
Proof.
lra.
Qed.
Definition noise_zero := exist (fun (x: R) => -1 <= x /\ x <= 1) 0 zero_is_valid_noise.
Definition noise_one := exist (fun (x: R) => -1 <= x /\ x <= 1) 1 one_is_valid_noise.
Definition noise_mapping := nat -> option noise_type.
Definition contained_map (map1 map2: noise_mapping) := forall k v, map1 k = Some v -> map2 k = Some v.
Instance contained_map_preorder : PreOrder contained_map.
Proof.
constructor.
- unfold Reflexive, contained_map; auto.
- unfold Transitive, contained_map; auto.
Qed.
Lemma contained_map_refl map:
contained_map map map.
Proof.
intros k v; auto.
Qed.
Lemma contained_map_trans map1 map2 map3:
contained_map map1 map2 -> contained_map map2 map3 -> contained_map map1 map3.
Proof.
unfold contained_map; auto.
Qed.
Definition updMap (m: noise_mapping) (n: nat) (q: noise_type): noise_mapping :=
fun x => if x =? n then Some q else m x.
Lemma upd_sound map n q:
updMap map n q n = Some q.
Proof.
unfold updMap.
assert (n =? n = true) as H by apply Nat.eqb_refl.
now rewrite H.
Qed.
Lemma contained_map_extension map n q:
map n = None -> contained_map map (updMap map n q).
Proof.
intros A.
intros k v B.
unfold updMap.
destruct (k =? n) eqn: Heq; try assumption.
apply beq_nat_true in Heq.
congruence.
Qed.
Lemma contained_map_extension2 map n1 q1 n2 q2:
map n1 = None -> map n2 = None -> contained_map map (updMap (updMap map n2 q2) n1 q1).
Proof.
intros A B.
intros k v C.
unfold updMap.
destruct (k =? n1) eqn: Heq.
- apply beq_nat_true in Heq; congruence.
- destruct (k =? n2) eqn: Heq'; try assumption.
apply beq_nat_true in Heq'; congruence.
Qed.
Fixpoint eval_aff (a: affine_form R) (map: noise_mapping): option R :=
match a with
| Const v => Some v
| Noise n v a' => match (map n), eval_aff a' map with
| None, _ => None
| _, None => None
| Some res, Some res_a' =>
Some ((res * v) + res_a')
end
end.
Definition Ropt_eq (q1: option R) (q2: option R) : Prop :=
match q1, q2 with
| Some r1, Some r2 => r1 = r2
| None, None => True
| _, _ => False
end.
Lemma Ropt_eq_refl q:
Ropt_eq q q.
Proof.
now destruct q.
Qed.
Lemma Ropt_eq_sym x y:
Ropt_eq x y -> Ropt_eq y x.
Proof.
intros A.
destruct x, y; simpl in *; try auto using Qeq_sym.
Qed.
Lemma Ropt_eq_trans x y z:
Ropt_eq x y -> Ropt_eq y z -> Ropt_eq x z.
Proof.
intros A B.
destruct x, y, z; simpl in *; try contradiction; eauto using Req_trans.
Qed.
Instance Qoption_Equivalence : Equivalence Ropt_eq.
Proof.
constructor; eauto using Ropt_eq_refl, Ropt_eq_sym, Ropt_eq_trans.
Qed.
Lemma Ropt_eq_dec x y:
{Ropt_eq x y} + {~ (Ropt_eq x y)}.
Proof.
destruct x, y; simpl; eauto using Req_dec_sum.
Qed.
Definition af_evals (a: affine_form R) (v: R) (map: noise_mapping): Prop :=
Ropt_eq (eval_aff a map) (Some v).
Lemma constant_evals_unchanged v1 v2 map:
af_evals (Const v1) v2 map -> v1 = v2.
Proof.
intros A.
unfold af_evals, Ropt_eq in A.
now simpl in A.
Qed.
Lemma af_evals_noise_compat a v1 v2 n map:
af_evals (Noise n v1 a) v2 map ->
exists q, map n = Some q /\ af_evals a (v2 - q * v1) map.
Proof.
intros A.
unfold af_evals, Ropt_eq in *.
simpl in A.
destruct (map n); try contradiction.
destruct (eval_aff a map); try contradiction.
exists n0.
rewrite <- A.
split; auto; ring.
Qed.
Lemma af_evals_map_extension a v map1 map2:
contained_map map1 map2 ->
af_evals a v map1 ->
af_evals a v map2.
Proof.
unfold contained_map.
intros cont.
revert v.
induction a.
- now simpl in *.
- intros v__eval eval1.
apply af_evals_noise_compat in eval1 as [q1 [Hmap1 eval1]].
specialize (IHa _ eval1).
specialize (cont _ _ Hmap1).
clear eval1 Hmap1.
unfold af_evals in *.
simpl in *.
rewrite cont.
unfold Ropt_eq in *.
destruct (eval_aff a map2); try contradiction.
rewrite IHa; lra.
Qed.
Lemma bounded_by_abs_pos v (q: noise_type):
0 < v -> - Rabs v <= q * v <= Rabs v.
Proof.
intros v_pos % Rlt_le; destruct q as [q [q_l q_h]]; simpl; rewrite Rabs_pos_eq; try lra; split.
- Rrewrite (q * v = - (- q * v)).
apply Ropp_le_contravar.
pose proof (Rmult_le_compat_r _ _ _ v_pos q_l); lra.
- pose proof (Rmult_le_compat_r _ _ _ v_pos q_h); lra.
Qed.
Lemma Rabs_bounded (x y: R):
-1 <= x <= 1 ->
Rabs(x*y) <= Rabs y.
Proof.
intros.
rewrite Rabs_mult.
assert (Rabs y = 1 * Rabs y) as tmp by lra; rewrite tmp at 2; clear tmp.
eapply Rmult_le_compat_r; eauto using Rabs_pos, Rabs_le.
Qed.
Lemma bounded_by_abs v (q: noise_type):
- Rabs v <= q * v <= Rabs v.
Proof.
destruct (Req_dec_sum v 0) as [H | H].
- subst.
rewrite Rabs_pos_eq; lra.
- destruct (Rlt_dec v 0) as [H' | H'].
+ destruct (bounded_by_abs_pos (v:=-v) q) as [v_l v_h]; try lra.
rewrite Rabs_Ropp in v_h, v_l.
assert (q * v = - (q * -v)) as H0 by lra.
assert (Rabs v = - - Rabs v) as H1 by lra.
rewrite H0.
rewrite H1 at 2.
split; apply Ropp_le_contravar; auto.
+ apply bounded_by_abs_pos; lra.
Qed.
(* Interval containment property *)
Lemma bounded_aff a map v:
(eval_aff a map) = (Some v) ->
(get_const a) - (radius a) <= v /\ v <= (get_const a) + (radius a).
Proof.
revert v; induction a; intros v0 eval; simpl in *; subst.
- inversion eval; subst; lra.
- case_eq (map n); intros; rewrite H in eval; try congruence.
case_eq (eval_aff a map); intros; rewrite H0 in eval; inversion eval.
subst.
specialize (IHa _ H0); destruct IHa as [IHal IHar].
assert (- Rabs v <= n0 * v <= Rabs v) as [v_l v_h] by eauto using bounded_by_abs.
split.
+ pose proof (Rplus_le_compat _ _ _ _ IHal v_l); lra.
+ pose proof (Rplus_le_compat _ _ _ _ IHar v_h); lra.
Qed.
Lemma bounded_aff_abs a map v:
(eval_aff a map) = Some v ->
Rabs (v - get_const a) <= radius a.
Proof.
intros.
apply Rabs_le.
pose proof (bounded_aff a map H).
lra.
Qed.
Lemma bounded_af_evals_abs a map v:
af_evals a v map ->
Rabs (v - get_const a) <= radius a.
Proof.
unfold af_evals.
destruct (eval_aff a map) eqn: Hv.
- intros A.
simpl in A.
rewrite <- A.
eauto using bounded_aff_abs.
- simpl; intros; contradiction.
Qed.
Lemma to_interval_containment a v map:
af_evals a v map ->
IVlo (toInterval a) <= v <= IVhi (toInterval a).
Proof.
intros evals.
simpl.
unfold af_evals in evals.
destruct (eval_aff a map) eqn: Hq; simpl in evals; try contradiction.
rewrite <- evals.
now apply bounded_aff with (map := map).
Qed.
Lemma radius_0_const (a: affine_form R) v map:
af_evals a v map ->
radius a = 0 ->
v = get_const a.
Proof.
unfold af_evals, Ropt_eq.
intros evals rad.
destruct (eval_aff a map) eqn: Hev; try contradiction.
apply bounded_aff in Hev.
rewrite evals in *.
rewrite rad in Hev.
lra.
Qed.
(***********************************************)
(******** Addition of two affine forms *********)
(***********************************************)
Function plus_aff_tuple (a: affine_form R * affine_form R) { measure aff_length_tuple a }: affine_form R :=
let (a1, a2) := a in
match a1, a2 with
| Const v1, Const v2 => Const (v1 + v2)
| Const v1, Noise n2 v2 a2' => Noise n2 v2 (plus_aff_tuple (a1, a2'))
| Noise n1 v1 a1', Const v2 => Noise n1 v1 (plus_aff_tuple (a1', a2))
| Noise n1 v1 a1', Noise n2 v2 a2' =>
if (n1 =? n2)%nat then
Noise n1 (v1+v2) (plus_aff_tuple (a1', a2'))
else if n1 <? n2%nat then
Noise n2 v2 (plus_aff_tuple (a1, a2'))
else
Noise n1 v1 (plus_aff_tuple (a1', a2))
end.
Proof.
- intros. unfold aff_length_tuple; simpl; auto; lia.
- intros; unfold aff_length_tuple; simpl; auto; lia.
- intros; unfold aff_length_tuple; simpl; auto; lia.
- intros; unfold aff_length_tuple; simpl; auto; lia.
- intros; unfold aff_length_tuple; simpl; auto; lia.
Defined.
Definition plus_aff (a1 a2: affine_form R): affine_form R := plus_aff_tuple (a1, a2).
Lemma plus_aff_tuple_sound (a: affine_form R * affine_form R) (v1 v2: R) map:
af_evals (fst a) v1 map ->
af_evals (snd a) v2 map ->
af_evals (plus_aff_tuple a) (v1 + v2) map.
Proof.
revert v1 v2; unfold af_evals.
functional induction (plus_aff_tuple a); simpl in *; intros v3 v4 G1 G2.
- lra.
- case_eq (map n2); intros; rewrite H in *; [ | inversion G2 ].
destruct (eval_aff a2' map); unfold Ropt_eq in *; [ | inversion G2].
specialize (IHa0 _ _ G1 (Ropt_eq_refl (Some r))).
case_eq (eval_aff (plus_aff_tuple (Const v1, a2')) map); intros; rewrite H0 in *; [ | inversion IHa0 ].
lra.
- case_eq (map n1); intros; rewrite H in *; [ | inversion G1 ].
destruct (eval_aff a1' map); unfold Ropt_eq in *; [ | inversion G1 ].
specialize (IHa0 _ _ (Ropt_eq_refl (Some r)) G2).
case_eq (eval_aff (plus_aff_tuple (a1', Const v2)) map); intros; rewrite H0 in *; [ | inversion IHa0 ].
lra.
- apply beq_nat_true in e2; subst.
case_eq (map n2); intros; rewrite H in *; [ | inversion G1 ].
destruct (eval_aff a1' map); unfold Ropt_eq in *; [ | inversion G1 ].
destruct (eval_aff a2' map); unfold Ropt_eq in *; [ | inversion G2 ].
specialize (IHa0 _ _ (eq_refl r) (eq_refl r0)).
case_eq (eval_aff (plus_aff_tuple (a1', a2')) map); intros; rewrite H0 in *; [ | inversion IHa0 ].
lra.
- case_eq (map n1); intros; rewrite H in *; [ | inversion G1 ].
case_eq (map n2); intros; rewrite H0 in *; [ | inversion G2 ].
destruct (eval_aff a1' map); unfold Ropt_eq in *; [ | inversion G1 ].
destruct (eval_aff a2' map); unfold Ropt_eq in *; [ | inversion G2 ].
specialize (IHa0 _ _ (eq_refl (n * v1 + r)) (eq_refl r0)).
case_eq (eval_aff (plus_aff_tuple (Noise n1 v1 a1', a2')) map); intros; rewrite H1 in *; [ | inversion IHa0 ].
lra.
- case_eq (map n1); intros; rewrite H in *; [ | inversion G1 ].
case_eq (map n2); intros; rewrite H0 in *; [ | inversion G2 ].
destruct (eval_aff a1' map); unfold Ropt_eq in *; [ | inversion G1 ].
destruct (eval_aff a2' map); unfold Ropt_eq in *; [ | inversion G2 ].
specialize (IHa0 _ _ (eq_refl r) (eq_refl (n0 * v2 + r0))).
case_eq (eval_aff (plus_aff_tuple (a1', Noise n2 v2 a2')) map); intros; rewrite H1 in *; [ | inversion IHa0 ].
lra.
Qed.
Lemma plus_aff_sound (a1: affine_form R) (a2: affine_form R) (v1 v2: R) map:
af_evals a1 v1 map ->
af_evals a2 v2 map ->
af_evals (plus_aff a1 a2) (v1 + v2) map.
Proof.
eauto using plus_aff_tuple_sound.
Qed.
Lemma plus_aff_comm (a1 a2: affine_form R) v1 v2 map:
af_evals a1 v1 map ->
af_evals a2 v2 map ->
af_evals (plus_aff a1 a2) (v1 + v2) map <-> af_evals (plus_aff a2 a1) (v2 + v1) map.
Proof.
intros evals1 evals2.
pose proof (plus_aff_sound _ _ _ _ _ evals1 evals2) as evalspl.
pose proof (plus_aff_sound _ _ _ _ _ evals2 evals1) as evalspr.
unfold af_evals in *.
rewrite evalspl, evalspr.
simpl; lra.
Qed.
Lemma plus_aff_preserves_fresh a1 a2 n:
fresh n a1 ->
fresh n a2 ->
fresh n (plus_aff a1 a2).
Proof.
unfold plus_aff.
remember (a1, a2) as a12.
assert (fst a12 = a1 /\ snd a12 = a2) as Havals by now rewrite Heqa12.
destruct Havals as [Heqa1 Heqa2].
rewrite <- Heqa1, <- Heqa2.
clear Heqa1 Heqa2 Heqa12 a1 a2.
intros fresh1 fresh2.
functional induction (plus_aff_tuple a12); simpl in *; eauto using fresh_noise_gt, fresh_noise_compat, fresh_noise.
pose proof (fresh_noise_gt fresh1) as freshn1.
apply fresh_noise_compat in fresh1.
pose proof (fresh_noise_gt fresh2) as freshn2.
apply fresh_noise_compat in fresh2.
specialize (IHa fresh1 fresh2).
now apply (fresh_noise _ freshn1).
Qed.
(***********************************************)
(***** Multiplication of two affine forms ******)
(***********************************************)
Function mult_aff_aux (a: affine_form R * affine_form R) { measure aff_length_tuple a }: affine_form R :=
let (a1, a2) := a in
let c_a1 := get_const a1 in
let c_a2 := get_const a2 in
match a1, a2 with
| Const v1, Const v2 => Const (v1 * v2)
| Const v1, Noise n2 v2 a2' => Noise n2 (v2 * v1) (mult_aff_aux (a1, a2'))
| Noise n1 v1 a1', Const v2 => Noise n1 (v1 * v2) (mult_aff_aux (a1', a2))
| Noise n1 v1 a1', Noise n2 v2 a2' =>
if (n1 =? n2) then
Noise n1 (v1 * c_a2 + v2 * c_a1) (mult_aff_aux (a1', a2'))
else if (n1 <? n2) then
Noise n2 (v2 * c_a1) (mult_aff_aux (a1, a2'))
else
Noise n1 (v1 * c_a2) (mult_aff_aux (a1', a2))
end.
Proof.
- intros; unfold aff_length_tuple; simpl; auto; lia.
- intros; unfold aff_length_tuple; simpl; auto; lia.
- intros; unfold aff_length_tuple; simpl; auto; lia.
- intros; unfold aff_length_tuple; simpl; auto; lia.
- intros; unfold aff_length_tuple; simpl; auto; lia.
Defined.
Definition mult_aff (a1 a2: affine_form R) (next_noise: nat): affine_form R :=
if (Req_dec_sum (radius a1 * radius a2) 0) then
mult_aff_aux (a1, a2)
else
Noise next_noise (radius a1 * radius a2) (mult_aff_aux (a1, a2)).
Lemma mult_aff_aux_sound_helper1 (a1 a2: affine_form R) (val1 val2 v1 v2 q: R) (q1 qIHa: noise_type):
q = (val1 - q1 * v1) * (val2 - q1 * v2) - qIHa * radius a1 * radius a2 ->
Rabs (val1 - q1 * v1 - get_const a1) <= radius a1 ->
Rabs (val2 - get_const a2) <= Rabs v2 + radius a2 ->
Rabs (val1 * val2 - q1 * (v1 * get_const a2 + v2 * get_const a1) - q) <=
(Rabs v1 + radius a1) * (Rabs v2 + radius a2).
Proof.
intros Hq bounds1 bounds2.
rewrite Hq.
Rrewrite (val1 * val2 - q1 * (v1 * get_const a2 + v2 * get_const a1) - ((val1 - q1 * v1) * (val2 - q1 * v2) - qIHa * radius a1 * radius a2) = - q1 * v1 * q1 * v2 + q1 * v2 * (val1 - get_const a1) + q1 * v1 * (val2 - get_const a2) + qIHa * (radius a1 * radius a2)).
Rrewrite ((Rabs v1 + radius a1) * (Rabs v2 + radius a2) = Rabs v1 * Rabs v2 + radius a1 * Rabs v2 + Rabs v1 * radius a2 + radius a1 * radius a2).
eapply Rle_trans; try eapply Rabs_triang.
eapply Rplus_le_compat.
- Rrewrite (- q1 * v1 * q1 * v2 + q1 * v2 * (val1 - get_const a1) + q1 * v1 * (val2 - get_const a2) = q1 * v2 * (val1 - q1 * v1 - get_const a1) + q1 * v1 * (val2 - get_const a2)).
Rrewrite (Rabs v1 * Rabs v2 + radius a1 * Rabs v2 + Rabs v1 * radius a2 = Rabs v2 * radius a1 + Rabs v1 * (Rabs v2 + radius a2)).
eapply Rle_trans; try eapply Rabs_triang.
pose proof (Rabs_bounded (v2 * (val1 - q1 * v1 - get_const a1)) (proj2_sig q1)) as H.
pose proof (Rabs_bounded (v1 * (val2 - get_const a2)) (proj2_sig q1)) as H'.
eapply Rplus_le_compat; eapply Rle_trans; try (rewrite Rmult_assoc; eauto);
rewrite Rabs_mult; eauto using Rabs_pos, Rmult_le_compat_l.
- eapply Rle_trans; try apply (Rabs_bounded (radius a1 * radius a2) (proj2_sig qIHa)).
rewrite Rabs_mult.
pose proof (radius_nonneg a1) as H1.
pose proof (radius_nonneg a2) as H2.
repeat rewrite Rabs_pos_eq; try lra.
Qed.
Lemma mult_aff_aux_sound_helper2 (a1 a2: affine_form R) (val1 val2 v1 v2 q: R) (q1 qIHa: noise_type):
q = val1 * (val2 - q1 * v2) - qIHa * (Rabs v1 + radius a1) * radius a2 ->
Rabs (val1 - get_const a1) <= Rabs v1 + radius a1 ->
Rabs (val1 * val2 - q1 * (v2 * get_const a1) - q) <=
(Rabs v1 + radius a1) * (Rabs v2 + radius a2).
Proof.
intros Hq bounds1.
rewrite Hq.
Rrewrite (val1 * val2 - q1 * (v2 * get_const a1) - (val1 * (val2 - q1 * v2) - qIHa * (Rabs v1 + radius a1) * radius a2) = q1 * v2 * (val1 - get_const a1) + qIHa * (Rabs v1 * radius a2) + qIHa * (radius a1 * radius a2)).
Rrewrite ((Rabs v1 + radius a1) * (Rabs v2 + radius a2) = Rabs v2 * (Rabs v1 + radius a1) + Rabs v1 * radius a2 + radius a1 * radius a2).
eapply Rle_trans; try eapply Rabs_triang.
pose proof (Rabs_bounded (v2 * (val1 - get_const a1)) (proj2_sig q1)) as H.
epose proof (Rabs_bounded _ (proj2_sig qIHa)).
eapply Rplus_le_compat.
- eapply Rle_trans; try eapply Rabs_triang.
eapply Rplus_le_compat.
+ eapply Rle_trans.
* rewrite Rmult_assoc.
eauto.
* rewrite Rabs_mult.
apply Rmult_le_compat_l; eauto using Rabs_pos.
+ eapply Rle_trans; try eauto.
rewrite Rabs_mult.
rewrite (Rabs_pos_eq (radius a2) (radius_nonneg a2)).
rewrite (Rabs_pos_eq (Rabs v1) (Rabs_pos v1)).
lra.
- eapply Rle_trans.
apply (Rabs_bounded (x := qIHa) (radius a1 * radius a2) (proj2_sig qIHa)).
rewrite Rabs_mult.
pose proof (radius_nonneg a1) as H1.
pose proof (radius_nonneg a2) as H2.
repeat rewrite Rabs_pos_eq; lra.
Qed.
Lemma mult_aff_aux_sound_helper3 (a1 a2: affine_form R) (val1 val2 v1 v2 q: R) (q1 qIHa: noise_type):
q = (val1 - q1 * v1) * val2 - qIHa * radius a1 * (Rabs v2 + radius a2) ->
Rabs (val2 - get_const a2) <= Rabs v2 + radius a2 ->
Rabs (val1 * val2 - q1 * (v1 * get_const a2) - q) <=
(Rabs v1 + radius a1) * (Rabs v2 + radius a2).
Proof.
Rrewrite ((val1 - q1 * v1) * val2 - qIHa * radius a1 * (Rabs v2 + radius a2) = val2 * (val1 - q1 * v1) - qIHa * (Rabs v2 + radius a2) * radius a1).
Rrewrite (val1 * val2 - q1 * (v1 * get_const a2) - q = val2 * val1 - q1 * (v1 * get_const a2) - q).
Rrewrite ((Rabs v1 + radius a1) * (Rabs v2 + radius a2) = (Rabs v2 + radius a2) * (Rabs v1 + radius a1)).
eauto using mult_aff_aux_sound_helper2.
Qed.
Lemma mult_aff_aux_sound (a1: affine_form R) (a2: affine_form R) (v1 v2: R) map:
af_evals a1 v1 map ->
af_evals a2 v2 map ->
exists (q: noise_type), af_evals (mult_aff_aux (a1, a2)) (v1 * v2 - q * (radius a1) * (radius a2)) map.
Proof.
revert v1 v2.
remember (a1, a2) as a12.
assert (fst a12 = a1 /\ snd a12 = a2) as Havals by now rewrite Heqa12.