Commit be900b25 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'affine_arithmetic' into 'master'

Affine arithmetic

See merge request AVA/FloVer!10
parents 93095593 a80a2a77
......@@ -4,6 +4,6 @@
url = https://github.com/CakeML/cakeml.git
[submodule "daisy"]
branch = certificates
branch = certified
path = daisy
url = ../../AVA/daisy.git
This diff is collapsed.
This diff is collapsed.
Require Import Coq.ZArith.ZArith Coq.ZArith.Zbool Coq.micromega.Psatz Recdef.
Require Import Flover.Infra.Abbrevs.
Inductive affine_form (V: Type): Type :=
| Const: V -> affine_form V
| Noise: nat -> V -> affine_form V -> affine_form V.
Fixpoint get_const V (a: affine_form V): V := match a with
| Const v => v
| Noise n c a' => get_const a'
end.
(* Helper function to serve as a measure for fixpoint termination *)
Fixpoint aff_length (V: Type) (a: affine_form V): nat := match a with
| Const _ => 0
| Noise _ _ a' => 1 + aff_length a'
end.
Definition aff_length_tuple V (a: affine_form V * affine_form V) :=
(aff_length (fst a) + aff_length (snd a))%nat.
Definition aff_tuple_order V (a b:affine_form V * affine_form V):=
(aff_length_tuple a < aff_length_tuple b)%nat.
Fixpoint get_max_index_aux V (current_max: nat) (a: affine_form V): nat := match a with
| Const _ => current_max
| Noise n v a' => if (Nat.leb current_max n) then
get_max_index_aux n a'
else
get_max_index_aux current_max a'
end.
Functional Scheme get_max_index_aux_ind := Induction for get_max_index_aux Sort Prop.
Definition get_max_index V (a: affine_form V) := get_max_index_aux 0 a.
Definition fresh V (n: nat) (a: affine_form V) :=
(n > get_max_index a)%nat.
Lemma get_mia_monotonic V (a: affine_form V) (n: nat):
(get_max_index_aux n a >= n)%nat.
Proof.
functional induction get_max_index_aux V n a.
- lia.
- apply Nat.leb_le in e0.
unfold Peano.ge; auto.
eapply Nat.le_trans; eauto.
- lia.
Qed.
Lemma get_mia_monotonic2 V (a: affine_form V) (p q: nat):
(p >= q)%nat ->
(get_max_index_aux p a >= get_max_index_aux q a)%nat.
Proof.
revert p q; induction a; intros p q pgeqq; simpl in *.
- auto.
- case_eq (p <=? n)%nat; intros pleqn.
+ assert ((q <=? n)%nat = true) as qleqn by (apply Nat.leb_le; apply Nat.leb_le in pleqn; lia).
rewrite qleqn.
lia.
+ case_eq (q <=? n)%nat; intros qleqn.
* apply leb_complete_conv in pleqn.
assert (p >= n)%nat by lia.
specialize (IHa p n H); auto.
* specialize (IHa p q pgeqq); auto.
Qed.
Lemma fresh_noise_compat V (a: affine_form V) m n v:
fresh m (Noise n v a) -> fresh m a.
Proof.
unfold fresh, get_max_index in *; destruct a; intros.
rewrite get_max_index_aux_equation.
- simpl in H. lia.
- simpl in H.
case_eq (n <=? n0); intros; rewrite H0 in H.
+ apply Nat.leb_le in H0.
simpl.
auto.
+ simpl.
apply leb_complete_conv in H0.
assert (get_max_index_aux n a >= get_max_index_aux n0 a)%nat
by (apply get_mia_monotonic2; lia).
lia.
Qed.
Lemma fresh_noise_gt V (a: affine_form V) m n v:
fresh m (Noise n v a) -> (m > n)%nat.
Proof.
intros A.
unfold fresh, get_max_index in *; induction a.
- rewrite get_max_index_aux_equation in A.
now simpl in A.
- simpl in A.
destruct (n <=? n0) eqn: Hn.
+ apply Nat.leb_le in Hn.
pose proof (get_mia_monotonic a n0) as mono.
apply (le_lt_trans _ _ _ mono) in A.
lia.
+ apply leb_complete_conv in Hn.
auto.
Qed.
Lemma fresh_noise V (a: affine_form V) m n v:
(m > n)%nat -> fresh m a -> fresh m (Noise n v a).
Proof.
intros A B.
unfold fresh, get_max_index in *; induction a.
- trivial.
- simpl in *.
destruct (n <=? n0) eqn: Hn.
+ assumption.
+ apply leb_complete_conv in Hn.
apply IHa.
clear IHa A Hn n v v0.
assert ((get_max_index_aux n0 a >= get_max_index_aux 0 a)%nat)
by (eapply get_mia_monotonic2; omega).
apply (le_lt_trans _ _ _ H B).
Qed.
Lemma fresh_monotonic V (a: affine_form V) m n:
(m >= n)%nat -> fresh n a -> fresh m a.
Proof.
unfold fresh; lia.
Qed.
Lemma fresh_inc V (a: affine_form V) n:
fresh n a ->
fresh (n + 1) a.
Proof.
unfold fresh.
lia.
Qed.
Lemma fresh_n_gt_O V (a: affine_form V) n:
fresh n a ->
(n > 0)%nat.
Proof.
destruct a.
- unfold fresh, get_max_index; rewrite get_max_index_aux_equation; auto.
- intros ? % fresh_noise_gt; lia.
Qed.
This diff is collapsed.
......@@ -4,19 +4,20 @@
Running this function on the encoded analysis result gives the desired theorem
as shown in the soundness theorem.
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
Require Import Flover.RealRangeValidator Flover.RoundoffErrorValidator Flover.Environments Flover.Typing Flover.FPRangeValidator.
From Flover
Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
Environments Typing FPRangeValidator ExpressionAbbrevs Commands.
Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
Require Export Infra.ExpressionAbbrevs Flover.Commands Coq.QArith.QArith.
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
let tMap := (typeMap defVars e (FloverMap.empty mType)) in
if (typeCheck e defVars tMap)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
(P:precond) (defVars:nat -> option mType) (fBits:FloverMap.t N):=
let tMap := (typeMap defVars e (FloverMap.empty mType) fBits) in
if (typeCheck e defVars tMap fBits)
then
if RangeValidator e absenv P && FPRangeValidator e absenv tMap NatSet.empty
if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
then RoundoffErrorValidator e tMap absenv NatSet.empty
else false
else false.
......@@ -26,7 +27,8 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (de
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
**)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P
defVars fBits:
forall (E1 E2:env),
approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
(forall v, NatSet.In v (Expressions.usedVars e) ->
......@@ -35,13 +37,13 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa
(forall v, NatSet.In v (usedVars e) ->
exists m : mType,
defVars v = Some m) ->
CertificateChecker e absenv P defVars = true ->
CertificateChecker e absenv P defVars fBits = true ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR REAL /\
eval_expr E2 defVars (toRExp e) vF m /\
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) vR REAL /\
eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m /\
(forall vF m,
eval_expr E2 defVars (toRExp e) vF m ->
eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
......@@ -57,6 +59,10 @@ Proof.
assert (dVars_range_valid NatSet.empty E1 absenv).
{ unfold dVars_range_valid.
intros; set_tac. }
assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None))
as affine_dvars_valid.
{ unfold affine_dVars_range_valid.
intros; set_tac. }
assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
{ hnf; intros a in_empty.
set_tac. }
......@@ -64,24 +70,29 @@ Proof.
{ unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
split; try auto. hnf; intros; set_tac. }
rename R into validFPRanges.
edestruct (RangeValidator_sound e absenv (P:=P) (Gamma:=defVars) (E:=E1))
as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]; eauto.
assert (validRanges e absenv E1 defVars (toRBMap fBits)) as valid_e.
{ eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1));
auto. }
pose proof (validRanges_single _ _ _ _ _ valid_e) as valid_single;
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType) fBits) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; split; auto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
let tMap := typeMapCmd defVars f (FloverMap.empty mType) in
if (typeCheckCmd f defVars tMap && validSSA f (freeVars f))
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
defVars fBits:=
let tMap := typeMapCmd defVars f (FloverMap.empty mType) fBits in
if (typeCheckCmd f defVars tMap fBits && validSSA f (freeVars f))
then
if (validIntervalboundsCmd f absenv P NatSet.empty) &&
if (RangeValidatorCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv tMap NatSet.empty
then (validErrorboundCmd f tMap absenv NatSet.empty)
then (RoundoffErrorValidatorCmd f tMap absenv NatSet.empty)
else false
else false.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
defVars fBits:
forall (E1 E2:env),
approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
(forall v, NatSet.In v (freeVars f) ->
......@@ -90,13 +101,13 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
(forall v, NatSet.In v (freeVars f) ->
exists m : mType,
defVars v = Some m) ->
CertificateCheckerCmd f absenv P defVars = true ->
CertificateCheckerCmd f absenv P defVars fBits = true ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL /\
bstep (toRCmd f) E2 defVars vF m /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\
bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m /\
(forall vF m,
bstep (toRCmd f) E2 defVars vF m ->
bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m ->
(Rabs (vR - vF) <= Q2R (err))%R).
(**
The proofs is a simple composition of the soundness proofs for the range
......@@ -122,12 +133,13 @@ Proof.
destruct H0; set_tac. }
assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
as freeVars_contained by set_tac.
edestruct (validIntervalboundsCmd_sound)
as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]]; eauto.
assert (validRangesCmd f absenv E1 defVars (toRBMap fBits)) as valid_f.
{ eapply RangeValidatorCmd_sound; eauto.
unfold affine_dVars_range_valid; intros.
set_tac. }
pose proof (validRangesCmd_single _ _ _ _ _ valid_f) as valid_single.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
edestruct validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
exists (f_lo, f_hi), err, vR, vF, mF; split; try auto.
split; try auto; split; try auto.
intros.
eapply validErrorboundCmd_sound; eauto.
Qed.
\ No newline at end of file
Qed.
......@@ -49,14 +49,14 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Define big step semantics for the Flover language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars:
eval_expr E defVars e v m ->
bstep s (updEnv x v E) (updDefVars x m defVars) res m' ->
bstep (Let m x e s) E defVars res m'
|ret_b m e E v defVars:
eval_expr E defVars e v m ->
bstep (Ret e) E defVars v m.
Inductive bstep : cmd R -> env -> (nat -> option mType) -> (expr R -> option N) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars fBits:
eval_expr E defVars fBits e v m ->
bstep s (updEnv x v E) (updDefVars x m defVars) fBits res m' ->
bstep (Let m x e s) E defVars fBits res m'
|ret_b m e E v defVars fBits:
eval_expr E defVars fBits e v m ->
bstep (Ret e) E defVars fBits v m.
(**
The free variables of a command are all used variables of exprressions
......@@ -88,14 +88,14 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
end.
Lemma bstep_eq_env f:
forall E1 E2 Gamma v m,
forall E1 E2 Gamma fBits v m,
(forall x, E1 x = E2 x) ->
bstep f E1 Gamma v m ->
bstep f E2 Gamma v m.
bstep f E1 Gamma fBits v m ->
bstep f E2 Gamma fBits v m.
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
- eapply eval_eq_env in H8; eauto. eapply let_b; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
......
......@@ -7,9 +7,9 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealSimps Flover.Infra.RealRationalProps.
Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
eval_expr E1 (toRMap defVars) (Const REAL n) nR REAL ->
eval_expr E2 defVars (Const m n) nF m ->
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars fBits:
eval_expr E1 (toRMap defVars) fBits (Const REAL n) nR REAL ->
eval_expr E2 defVars fBits (Const m n) nF m ->
(Rabs (nR - nF) <= computeErrorR n m)%R.
Proof.
intros eval_real eval_float.
......@@ -30,14 +30,19 @@ Proof.
Qed.
Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars fBits:
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars fBits (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) fBits (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(fun e =>
match e with
| Binop b (Var _ 1) (Var _ 2) => fBits (toRExp (Binop b e1 e2))
| _ => fBits e
end)
(Binop Plus (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
......@@ -50,22 +55,20 @@ Proof.
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in plus_real; auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) (join REAL REAL) delta); auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) REAL delta); auto.
unfold evalBinop in *; simpl in *.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in plus_real.
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in plus_real.
clear H5 H6 H7 v1 v2.
clear delta H2.
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in plus_real.
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in plus_real.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion plus_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H7; subst.
unfold updEnv; simpl.
unfold updEnv in H1,H6; simpl in *.
symmetry in H1,H6.
inversion H1; inversion H6; subst.
inversion H6; subst; inversion H7; subst.
unfold updEnv in H1,H12; simpl in *.
symmetry in H1,H12.
inversion H1; inversion H12; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H1.
repeat rewrite Rmult_plus_distr_l.
......@@ -73,7 +76,7 @@ Proof.
rewrite Rsub_eq_Ropp_Rplus.
unfold computeErrorR.
pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta))).
destruct (join m0 m3);
destruct m;
repeat rewrite Ropp_plus_distr; try rewrite plus_bounds_simplify; try rewrite Rplus_assoc.
{ repeat rewrite <- Rplus_assoc.
assert (e1R + e2R + - e1F + - e2F = e1R + - e1F + e2R + - e2F)%R by lra.
......@@ -84,12 +87,12 @@ Proof.
rewrite Rplus_0_r.
apply Rplus_le_compat; try auto. }
Focus 4.
eapply Rle_trans.
apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
apply Rplus_le_compat; try auto.
eapply Rle_trans.
apply Rabs_triang.
rewrite Rabs_Ropp. apply Rplus_le_compat; auto.
eapply Rle_trans; [ apply Rabs_triang | rewrite (Rplus_assoc (Q2R err1)) ].
apply Rplus_le_compat; try auto.
eapply Rle_trans; [ apply Rabs_triang |].
apply Rplus_le_compat; try auto.
rewrite Rabs_Ropp; simpl. auto.
all: eapply Rle_trans; try eapply H.
all: setoid_rewrite Rplus_assoc at 2.
all: eapply Rplus_le_compat; try auto.
......@@ -103,14 +106,19 @@ Qed.
Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars fBits:
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars fBits (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) fBits (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(fun e =>
match e with
| Binop b (Var _ 1) (Var _ 2) => fBits (toRExp (Binop b e1 e2))
| _ => fBits e
end)
(Binop Sub (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
......@@ -118,42 +126,38 @@ Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
Proof.
intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion sub_real; subst;
inversion sub_real; subst.
assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in sub_real; auto.
rewrite delta_0_deterministic; auto.
rewrite (delta_0_deterministic (evalBinop Sub v1 v2) REAL delta); auto.
unfold evalBinop in *; simpl in *.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in sub_real.
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in sub_real.
clear H5 H6 H7 v1 v2.
clear delta H2.
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in sub_real.
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in sub_real.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion sub_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H7; subst.
unfold updEnv; simpl.
simpl in H0; simpl in H5; inversion H0; inversion H5; subst; clear H0 H5.
symmetry in H6, H1.
unfold updEnv in H6, H1; simpl in H6, H1.
inversion H6; inversion H1; subst.
inversion H6; subst; inversion H7; subst.
unfold updEnv in H1,H12; simpl in *.
symmetry in H1,H12.
inversion H1; inversion H12; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H8 H1 H6.
clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H8 H6 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
repeat rewrite Rsub_eq_Ropp_Rplus.
repeat rewrite Ropp_plus_distr.
unfold computeErrorR.
pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta))).
destruct (join m0 m3);
destruct m;
repeat rewrite Ropp_plus_distr; try rewrite Ropp_involutive;
try rewrite plus_bounds_simplify; try rewrite Rplus_assoc.
{ repeat rewrite <- Rplus_assoc.
assert (e1R + - e2R + - e1F + e2F = e1R + - e1F + - e2R + e2F)%R by lra.
rewrite H0; clear H0.
rewrite H1; clear H1.
rewrite Rplus_assoc.
eapply Rle_trans.
apply Rabs_triang; apply Rplus_le_compat; try auto.
......@@ -170,6 +174,7 @@ Proof.
rewrite Rabs_Ropp. apply Rplus_le_compat; try auto.
rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
auto.
all: eapply Rle_trans; try eapply Rabs_triang.
all: setoid_rewrite Rplus_assoc at 2.
all: eapply Rplus_le_compat; try auto.
......@@ -181,14 +186,19 @@ Proof.
Qed.
Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
(vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars fBits:
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars fBits (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) fBits (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(fun e =>
match e with
| Binop b (Var _ 1) (Var _ 2) => fBits (toRExp (Binop b e1 e2))
| _ => fBits e
end)
(Binop Mult (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
Proof.
......@@ -201,26 +211,25 @@ Proof.
rewrite delta_0_deterministic in mult_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in mult_real.
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in mult_real.
clear H5 H6 v1 v2 H7 H2.
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in mult_real.
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in mult_real.
clear H3 H4.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)