Commit fc30b638 authored by ='s avatar =
Browse files

Cleaning a few Coq files

parent ef97348d
...@@ -13,9 +13,8 @@ expression may yield different values for different machine epsilons ...@@ -13,9 +13,8 @@ expression may yield different values for different machine epsilons
(or environments that already only approximate each other) (or environments that already only approximate each other)
**) **)
Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop := Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
|approxRefl A: |approxRefl defVars A:
(* TODO: this is weird. why not start with defVars?*) approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv
approxEnv emptyEnv (fun n => None) A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m: |approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
approxEnv E1 defVars A fVars dVars E2 -> approxEnv E1 defVars A fVars dVars E2 ->
defVars x = Some m -> defVars x = Some m ->
......
...@@ -7,8 +7,8 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith. ...@@ -7,8 +7,8 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs. Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
(* TODO: absenv not used *)
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType) defVars: Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
eval_exp E1 (toREvalVars defVars) (Const M0 n) nR M0 -> eval_exp E1 (toREvalVars defVars) (Const M0 n) nR M0 ->
eval_exp E2 defVars (Const m n) nF m -> eval_exp E2 defVars (Const m n) nF m ->
(Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R. (Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R.
...@@ -51,7 +51,9 @@ Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) ...@@ -51,7 +51,9 @@ Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 -> eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toREvalVars defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 -> eval_exp E1 (toREvalVars defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Plus (Var R 1) (Var R 2)) vF m-> eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Plus (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%R. (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%R.
...@@ -116,7 +118,9 @@ Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) ...@@ -116,7 +118,9 @@ Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 -> eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toREvalVars defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 -> eval_exp E1 (toREvalVars defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Sub (Var R 1) (Var R 2)) vF m -> eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Sub (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R ->
(Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps m))))%R. (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps m))))%R.
...@@ -175,7 +179,9 @@ Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) ...@@ -175,7 +179,9 @@ Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 -> eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toREvalVars defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 -> eval_exp E1 (toREvalVars defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Mult (Var R 1) (Var R 2)) vF m-> eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Mult (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%R. (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%R.
Proof. Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float. intros e1_real e1_float e2_real e2_float mult_real mult_float.
...@@ -224,7 +230,9 @@ Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) ...@@ -224,7 +230,9 @@ Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
eval_exp E2 defVars (toRExp e2) e2F m2 -> eval_exp E2 defVars (toRExp e2) e2F m2 ->
eval_exp E1 (toREvalVars defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 -> eval_exp E1 (toREvalVars defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Div (Var R 1) (Var R 2)) vF m -> eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Div (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R. (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R.
Proof. Proof.
intros e1_real e1_float e2_real e2_float div_real div_float. intros e1_real e1_float e2_real e2_float div_real div_float.
...@@ -446,7 +454,9 @@ Qed. ...@@ -446,7 +454,9 @@ Qed.
Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars: Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
eval_exp E1 (toREvalVars defVars) (toREval e) nR M0 -> eval_exp E1 (toREvalVars defVars) (toREval e) nR M0 ->
eval_exp E2 defVars e nF1 m -> eval_exp E2 defVars e nF1 m ->
eval_exp (updEnv 1 nF1 emptyEnv) (fun n => if n =? 1 then Some m else defVars n) (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon-> eval_exp (updEnv 1 nF1 emptyEnv)
(updDefVars 1 m defVars)
(toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon->
(Rabs (nR - nF1) <= err)%R -> (Rabs (nR - nF1) <= err)%R ->
(Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R. (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R.
Proof. Proof.
......
...@@ -27,11 +27,11 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy ...@@ -27,11 +27,11 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy
else (Qleb (maxAbs intv * (meps m)) err) else (Qleb (maxAbs intv * (meps m)) err)
|Const _ n => |Const _ n =>
Qleb (maxAbs intv * (meps m)) err Qleb (maxAbs intv * (meps m)) err
|Unop Neg e => |Unop Neg e1 =>
if (validErrorbound e typeMap absenv dVars) if (validErrorbound e1 typeMap absenv dVars)
then Qeq_bool err (snd (absenv e)) then Qeq_bool err (snd (absenv e1))
else false else false
|Unop Inv e => false |Unop Inv e1 => false
|Binop b e1 e2 => |Binop b e1 e2 =>
if ((validErrorbound e1 typeMap absenv dVars) && (validErrorbound e2 typeMap absenv dVars)) if ((validErrorbound e1 typeMap absenv dVars) && (validErrorbound e2 typeMap absenv dVars))
then then
...@@ -112,7 +112,7 @@ Qed. ...@@ -112,7 +112,7 @@ Qed.
Lemma validErrorboundCorrectVariable: Lemma validErrorboundCorrectVariable:
forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma defVars, forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma defVars,
typeCheck (Var Q v) defVars Gamma = true -> typeCheck (Var Q v) defVars Gamma = true ->
approxEnv E1 defVars absenv fVars dVars E2 -> approxEnv E1 defVars absenv fVars dVars E2 ->
eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Var Q v))) nR M0 -> eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Var Q v))) nR M0 ->
eval_exp E2 defVars (toRExp (Var Q v)) nF m -> eval_exp E2 defVars (toRExp (Var Q v)) nF m ->
...@@ -120,7 +120,7 @@ Lemma validErrorboundCorrectVariable: ...@@ -120,7 +120,7 @@ Lemma validErrorboundCorrectVariable:
validErrorbound (Var Q v) Gamma absenv dVars = true -> validErrorbound (Var Q v) Gamma absenv dVars = true ->
(forall v1, (forall v1,
NatSet.mem v1 dVars = true -> NatSet.mem v1 dVars = true ->
exists r, E1 v1 = Some r /\ exists r, E1 v1 = Some r /\
(Q2R (fst (fst (absenv (Var Q v1)))) <= r <= Q2R (snd (fst (absenv (Var Q v1)))))%R) -> (Q2R (fst (fst (absenv (Var Q v1)))) <= r <= Q2R (snd (fst (absenv (Var Q v1)))))%R) ->
(forall v1, NatSet.mem v1 fVars= true -> (forall v1, NatSet.mem v1 fVars= true ->
exists r, E1 v1 = Some r /\ exists r, E1 v1 = Some r /\
...@@ -167,7 +167,7 @@ Proof. ...@@ -167,7 +167,7 @@ Proof.
rewrite H,H5 in typing_ok; apply EquivEqBoolEq in typing_ok; subst. rewrite H,H5 in typing_ok; apply EquivEqBoolEq in typing_ok; subst.
clear H5 H3. clear H5 H3.
apply Rmult_le_compat_r. apply Rmult_le_compat_r.
{ apply inj_eps_posR. } { apply meps_posR. }
{ rewrite <- maxAbs_impl_RmaxAbs. { rewrite <- maxAbs_impl_RmaxAbs.
apply contained_leq_maxAbs. apply contained_leq_maxAbs.
unfold contained; simpl. unfold contained; simpl.
...@@ -275,7 +275,7 @@ Lemma validErrorboundCorrectConstant: ...@@ -275,7 +275,7 @@ Lemma validErrorboundCorrectConstant:
forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars m Gamma defVars, forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars m Gamma defVars,
eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Const m n))) nR M0 -> eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Const m n))) nR M0 ->
eval_exp E2 defVars (toRExp (Const m n)) nF m -> eval_exp E2 defVars (toRExp (Const m n)) nF m ->
typeCheck (Const m n) defVars Gamma = true -> typeCheck (Const m n) defVars Gamma = true ->
validErrorbound (Const m n) Gamma absenv dVars = true -> validErrorbound (Const m n) Gamma absenv dVars = true ->
(Q2R nlo <= nR <= Q2R nhi)%R -> (Q2R nlo <= nR <= Q2R nhi)%R ->
absenv (Const m n) = ((nlo,nhi),e) -> absenv (Const m n) = ((nlo,nhi),e) ->
...@@ -298,12 +298,12 @@ Proof. ...@@ -298,12 +298,12 @@ Proof.
destruct intv_valid. destruct intv_valid.
eapply Rle_trans. eapply Rle_trans.
- eapply Rmult_le_compat_r. - eapply Rmult_le_compat_r.
apply inj_eps_posR. apply meps_posR.
apply RmaxAbs; eauto. apply RmaxAbs; eauto.
- rewrite Q2R_mult in error_valid. - rewrite Q2R_mult in error_valid.
rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto. rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto.
inversion subexpr_ok; subst. inversion subexpr_ok; subst.
rewrite H in H4. apply EquivEqBoolEq in H4; subst; auto. rewrite H in H4. apply EquivEqBoolEq in H4; subst; auto.
Qed. Qed.
Lemma validErrorboundCorrectAddition E1 E2 absenv Lemma validErrorboundCorrectAddition E1 E2 absenv
...@@ -316,9 +316,9 @@ Lemma validErrorboundCorrectAddition E1 E2 absenv ...@@ -316,9 +316,9 @@ Lemma validErrorboundCorrectAddition E1 E2 absenv
eval_exp E2 defVars (toRExp e1) nF1 m1 -> eval_exp E2 defVars (toRExp e1) nF1 m1 ->
eval_exp E2 defVars (toRExp e2) nF2 m2 -> eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (updDefVars 2 m2 (updDefVars 1 m1 defVars))
(toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m -> (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Plus e1 e2) defVars Gamma = true -> typeCheck (Binop Plus e1 e2) defVars Gamma = true ->
validErrorbound (Binop Plus e1 e2) Gamma absenv dVars = true -> validErrorbound (Binop Plus e1 e2) Gamma absenv dVars = true ->
(Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
(Q2R e2lo <= nR2 <= Q2R e2hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
...@@ -353,7 +353,7 @@ Proof. ...@@ -353,7 +353,7 @@ Proof.
eapply Rle_trans. eapply Rle_trans.
apply Rplus_le_compat_l. apply Rplus_le_compat_l.
eapply Rmult_le_compat_r. eapply Rmult_le_compat_r.
apply inj_eps_posR. apply meps_posR.
Focus 2. Focus 2.
rewrite Qle_bool_iff in valid_error. rewrite Qle_bool_iff in valid_error.
apply Qle_Rle in valid_error. apply Qle_Rle in valid_error.
...@@ -400,9 +400,9 @@ Lemma validErrorboundCorrectSubtraction E1 E2 absenv ...@@ -400,9 +400,9 @@ Lemma validErrorboundCorrectSubtraction E1 E2 absenv
eval_exp E2 defVars (toRExp e1) nF1 m1-> eval_exp E2 defVars (toRExp e1) nF1 m1->
eval_exp E2 defVars (toRExp e2) nF2 m2 -> eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (updDefVars 2 m2 (updDefVars 1 m1 defVars))
(toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m -> (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Sub e1 e2) defVars Gamma = true -> typeCheck (Binop Sub e1 e2) defVars Gamma = true ->
validErrorbound (Binop Sub e1 e2) Gamma absenv dVars = true -> validErrorbound (Binop Sub e1 e2) Gamma absenv dVars = true ->
(Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
(Q2R e2lo <= nR2 <= Q2R e2hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
...@@ -443,7 +443,7 @@ Proof. ...@@ -443,7 +443,7 @@ Proof.
eapply Rle_trans. eapply Rle_trans.
apply Rplus_le_compat_l. apply Rplus_le_compat_l.
eapply Rmult_le_compat_r. eapply Rmult_le_compat_r.
apply inj_eps_posR. apply meps_posR.
Focus 2. Focus 2.
apply valid_error. apply valid_error.
remember (subtractIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv. remember (subtractIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
...@@ -487,9 +487,9 @@ Lemma validErrorboundCorrectMult E1 E2 absenv ...@@ -487,9 +487,9 @@ Lemma validErrorboundCorrectMult E1 E2 absenv
eval_exp E2 defVars (toRExp e1) nF1 m1 -> eval_exp E2 defVars (toRExp e1) nF1 m1 ->
eval_exp E2 defVars (toRExp e2) nF2 m2 -> eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (updDefVars 2 m2 (updDefVars 1 m1 defVars))
(toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m -> (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Mult e1 e2) defVars Gamma = true -> typeCheck (Binop Mult e1 e2) defVars Gamma = true ->
validErrorbound (Binop Mult e1 e2) Gamma absenv dVars = true -> validErrorbound (Binop Mult e1 e2) Gamma absenv dVars = true ->
(Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
(Q2R e2lo <= nR2 <= Q2R e2hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
...@@ -1005,7 +1005,7 @@ Proof. ...@@ -1005,7 +1005,7 @@ Proof.
destruct H4. destruct H4.
unfold RmaxAbsFun. unfold RmaxAbsFun.
apply Rmult_le_compat_r. apply Rmult_le_compat_r.
apply inj_eps_posR. apply meps_posR.
apply RmaxAbs; subst; simpl in *. apply RmaxAbs; subst; simpl in *.
+ rewrite Q2R_min4. + rewrite Q2R_min4.
repeat rewrite Q2R_mult; repeat rewrite Q2R_mult;
...@@ -1027,9 +1027,9 @@ Lemma validErrorboundCorrectDiv E1 E2 absenv ...@@ -1027,9 +1027,9 @@ Lemma validErrorboundCorrectDiv E1 E2 absenv
eval_exp E2 defVars (toRExp e1) nF1 m1 -> eval_exp E2 defVars (toRExp e1) nF1 m1 ->
eval_exp E2 defVars (toRExp e2) nF2 m2 -> eval_exp E2 defVars (toRExp e2) nF2 m2 ->
eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
(fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (updDefVars 2 m2 (updDefVars 1 m1 defVars))
(toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m -> (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m ->
typeCheck (Binop Div e1 e2) defVars Gamma = true -> typeCheck (Binop Div e1 e2) defVars Gamma = true ->
validErrorbound (Binop Div e1 e2) Gamma absenv dVars = true -> validErrorbound (Binop Div e1 e2) Gamma absenv dVars = true ->
(Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
(Q2R e2lo <= nR2 <= Q2R e2hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
...@@ -1905,7 +1905,7 @@ Proof. ...@@ -1905,7 +1905,7 @@ Proof.
{ destruct valid_div_float. { destruct valid_div_float.
unfold RmaxAbsFun. unfold RmaxAbsFun.
apply Rmult_le_compat_r. apply Rmult_le_compat_r.
apply inj_eps_posR. apply meps_posR.
rewrite <- maxAbs_impl_RmaxAbs. rewrite <- maxAbs_impl_RmaxAbs.
unfold RmaxAbsFun. unfold RmaxAbsFun.
apply RmaxAbs; subst; simpl in *. apply RmaxAbs; subst; simpl in *.
...@@ -1952,7 +1952,9 @@ Qed. ...@@ -1952,7 +1952,9 @@ Qed.
Lemma validErrorboundCorrectRounding E1 E2 absenv (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars: Lemma validErrorboundCorrectRounding E1 E2 absenv (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars:
eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) nR M0 -> eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) nR M0 ->
eval_exp E2 defVars (toRExp e) nF1 m -> eval_exp E2 defVars (toRExp e) nF1 m ->
eval_exp (updEnv 1 nF1 emptyEnv) (fun n => if n =? 1 then Some m else defVars n) (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon -> eval_exp (updEnv 1 nF1 emptyEnv)
(updDefVars 1 m defVars)
(toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon ->
typeCheck (Downcast machineEpsilon e) defVars Gamma = true -> typeCheck (Downcast machineEpsilon e) defVars Gamma = true ->
validErrorbound (Downcast machineEpsilon e) Gamma absenv dVars = true -> validErrorbound (Downcast machineEpsilon e) Gamma absenv dVars = true ->
(Q2R elo <= nR <= Q2R ehi)%R -> (Q2R elo <= nR <= Q2R ehi)%R ->
...@@ -1970,11 +1972,11 @@ Proof. ...@@ -1970,11 +1972,11 @@ Proof.
case_eq (Gamma e); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. case_eq (Gamma e); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ].
andb_to_prop subexpr_ok. andb_to_prop subexpr_ok.
apply EquivEqBoolEq in L0; subst. apply EquivEqBoolEq in L0; subst.
andb_to_prop valid_error. andb_to_prop valid_error.
simpl in *. simpl in *.
eapply Rle_trans. eapply Rle_trans.
eapply round_abs_err_bounded; eauto. eapply round_abs_err_bounded; eauto.
assert (contained nR (Q2R elo, Q2R ehi)) as valid_intv_c by (unfold contained; auto). assert (contained nR (Q2R elo, Q2R ehi)) as valid_intv_c by (unfold contained; auto).
pose proof (distance_gives_iv _ valid_intv_c err_bounded) as dgi. pose proof (distance_gives_iv _ valid_intv_c err_bounded) as dgi.
unfold IntervalArith.contained in dgi. unfold IntervalArith.contained in dgi.
destruct dgi as [dgi1 dgi2]; simpl in dgi1; simpl in dgi2. destruct dgi as [dgi1 dgi2]; simpl in dgi1; simpl in dgi2.
...@@ -1983,7 +1985,7 @@ Proof. ...@@ -1983,7 +1985,7 @@ Proof.
apply Rmult_le_compat_r. apply Rmult_le_compat_r.
* rewrite <- Q2R0_is_0. * rewrite <- Q2R0_is_0.
apply Qle_Rle. apply Qle_Rle.
apply inj_eps_pos. apply meps_pos.
* remember (widenIntv (elo, ehi) err) as iv_widen. * remember (widenIntv (elo, ehi) err) as iv_widen.
destruct iv_widen as [eloR ehiR]. destruct iv_widen as [eloR ehiR].
rewrite <- maxAbs_impl_RmaxAbs. rewrite <- maxAbs_impl_RmaxAbs.
...@@ -1994,13 +1996,13 @@ Proof. ...@@ -1994,13 +1996,13 @@ Proof.
rewrite Q2R_minus. rewrite Q2R_minus.
rewrite Q2R_plus. rewrite Q2R_plus.
split; assumption. split; assumption.
+ apply Qle_bool_iff in R2. + apply Qle_bool_iff in R2.
rewrite <- Q2R_mult. rewrite <- Q2R_mult.
rewrite <- Q2R_plus. rewrite <- Q2R_plus.
apply Qle_Rle. apply Qle_Rle.
assumption. assumption.
Qed. Qed.
(** (**
Soundness theorem for the error bound validator. Soundness theorem for the error bound validator.
Proof is by induction on the expression e. Proof is by induction on the expression e.
...@@ -2008,7 +2010,7 @@ Qed. ...@@ -2008,7 +2010,7 @@ Qed.
**) **)
Theorem validErrorbound_sound (e:exp Q): Theorem validErrorbound_sound (e:exp Q):
forall E1 E2 fVars dVars absenv nR nF err P elo ehi m Gamma defVars, forall E1 E2 fVars dVars absenv nR nF err P elo ehi m Gamma defVars,
typeCheck e defVars Gamma = true -> typeCheck e defVars Gamma = true ->
approxEnv E1 defVars absenv fVars dVars E2 -> approxEnv E1 defVars absenv fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars -> NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) nR M0 -> eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) nR M0 ->
...@@ -2042,7 +2044,7 @@ Proof. ...@@ -2042,7 +2044,7 @@ Proof.
unfold isSupersetIntv in valid_intv; apply andb_true_iff in valid_intv; destruct valid_intv. unfold isSupersetIntv in valid_intv; apply andb_true_iff in valid_intv; destruct valid_intv.
simpl in H,H0. simpl in H,H0.
split; auto. split; auto.
* apply Qle_bool_iff in H1. apply (Qle_Rle _ _ H1). * apply Qle_bool_iff in H1. apply (Qle_Rle _ _ H1).
* apply Qle_bool_iff in H2. apply (Qle_Rle _ _ H2). * apply Qle_bool_iff in H2. apply (Qle_Rle _ _ H2).
- unfold validErrorbound in valid_error. - unfold validErrorbound in valid_error.
rewrite absenv_eq in valid_error. rewrite absenv_eq in valid_error.
...@@ -2176,7 +2178,7 @@ Proof. ...@@ -2176,7 +2178,7 @@ Proof.
simpl in eval_real. simpl in eval_real.
simpl in typing_ok. simpl in typing_ok.
simpl in fVars_subset. simpl in fVars_subset.
inversion typing_ok; subst. inversion typing_ok; subst.
pose proof (validIntervalbounds_sound e absenv P (fVars:=fVars) (dVars:=dVars) (E:=E1) defVars L1 (vR:=nR) valid_dVars fVars_subset P_valid eval_real) as vIB_e. pose proof (validIntervalbounds_sound e absenv P (fVars:=fVars) (dVars:=dVars) (E:=E1) defVars L1 (vR:=nR) valid_dVars fVars_subset P_valid eval_real) as vIB_e.
rewrite <- Heqabsenv_e in vIB_e. rewrite <- Heqabsenv_e in vIB_e.
simpl in vIB_e; auto. simpl in vIB_e; auto.
...@@ -2237,7 +2239,7 @@ Qed. ...@@ -2237,7 +2239,7 @@ Qed.
Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
forall E1 E2 outVars fVars dVars vR vF elo ehi err P m Gamma defVars, forall E1 E2 outVars fVars dVars vR vF elo ehi err P m Gamma defVars,
typeCheckCmd f defVars Gamma = true -> typeCheckCmd f defVars Gamma = true ->
approxEnv E1 defVars absenv fVars dVars E2 -> approxEnv E1 defVars absenv fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars -> ssa f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
...@@ -2246,7 +2248,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): ...@@ -2246,7 +2248,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
validErrorboundCmd f Gamma absenv dVars = true -> validErrorboundCmd f Gamma absenv dVars = true ->
validIntervalboundsCmd f absenv P dVars = true -> validIntervalboundsCmd f absenv P dVars = true ->
(forall v1, NatSet.mem v1 dVars = true -> (forall v1, NatSet.mem v1 dVars = true ->
exists vR, E1 v1 = Some vR /\ exists vR, E1 v1 = Some vR /\
(Q2R (fst (fst (absenv (Var Q v1)))) <= vR <= Q2R (snd (fst (absenv (Var Q v1)))))%R) -> (Q2R (fst (fst (absenv (Var Q v1)))) <= vR <= Q2R (snd (fst (absenv (Var Q v1)))))%R) ->
(forall v, NatSet.mem v fVars= true -> (forall v, NatSet.mem v fVars= true ->
exists vR, E1 v = Some vR /\ exists vR, E1 v = Some vR /\
...@@ -2257,7 +2259,7 @@ Proof. ...@@ -2257,7 +2259,7 @@ Proof.
induction f; induction f;
intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float valid_bounds valid_intv fVars_sound P_valid absenv_res. intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float valid_bounds valid_intv fVars_sound P_valid absenv_res.
- simpl in eval_real, eval_float. - simpl in eval_real, eval_float.
inversion eval_float; inversion eval_real; subst. inversion eval_float; inversion eval_real; subst.
inversion ssa_f; subst. inversion ssa_f; subst.
assert (approxEnv (updEnv n v0 E1) defVars absenv fVars (NatSet.add n dVars) (updEnv n v E2)). assert (approxEnv (updEnv n v0 E1) defVars absenv fVars (NatSet.add n dVars) (updEnv n v E2)).
+ eapply approxUpdBound; try auto. + eapply approxUpdBound; try auto.
...@@ -2333,7 +2335,7 @@ Proof. ...@@ -2333,7 +2335,7 @@ Proof.
simpl. simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto. split; try auto.
* intros v1 v1_mem. * intros v1 v1_mem.
unfold updEnv. unfold updEnv.
case_eq (v1 =? n); intros v1_eq. case_eq (v1 =? n); intros v1_eq.
{ rename R1 into eq_lo; { rename R1 into eq_lo;
...@@ -2342,7 +2344,7 @@ Proof. ...@@ -2342,7 +2344,7 @@ Proof.
apply Qeq_eqR in eq_lo. apply Qeq_eqR in eq_lo.
apply Qeq_bool_iff in eq_hi. apply Qeq_bool_iff in eq_hi.
apply Qeq_eqR in eq_hi. apply Qeq_eqR in eq_hi.
inversion type_f; subst. inversion type_f; subst.
apply Nat.eqb_eq in v1_eq; subst. apply Nat.eqb_eq in v1_eq; subst.
exists v0; split; try auto. exists v0; split; try auto.
rewrite <- eq_lo, <- eq_hi. rewrite <- eq_lo, <- eq_hi.
......
...@@ -204,7 +204,11 @@ Fixpoint toREval (e:exp R) := ...@@ -204,7 +204,11 @@ Fixpoint toREval (e:exp R) :=
| Downcast _ e1 => (toREval e1) | Downcast _ e1 => (toREval e1)
end. end.
(* TODO: put to REValVars here? *) Fixpoint toREvalVars (d:nat -> option mType) (n:nat) :=
match d n with
| Some m => Some M0
| None => None
end.
(** (**
...@@ -333,20 +337,12 @@ Proof. ...@@ -333,20 +337,12 @@ Proof.
Qed. Qed.
Fixpoint toREvalVars (d:nat -> option mType) (n:nat) :=
match d n with
| Some m => Some M0
| None => None
end.
(** (**
Helping lemma. Needed in soundness proof. Helping lemma. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subexpressions and then binding the result values to different evaluating the subexpressions and then binding the result values to different
variables in the Environment. variables in the Environment.
**) **)
(* TODO: write updDefVars function as well *)
Lemma binary_unfolding b f1 f2 m E vF defVars: Lemma binary_unfolding b f1 f2 m E vF defVars:
eval_exp E defVars (Binop b f1 f2) vF m -> eval_exp E defVars (Binop b f1 f2) vF m ->
exists vF1 vF2 m1 m2, exists vF1 vF2 m1 m2,
...@@ -354,7 +350,7 @@ Lemma binary_unfolding b f1 f2 m E vF defVars: ...@@ -354,7 +350,7 @@ Lemma binary_unfolding b f1 f2 m E vF defVars:
eval_exp E defVars f1 vF1 m1 /\ eval_exp E defVars f1 vF1 m1 /\
eval_exp E defVars f2 vF2 m2 /\ eval_exp E defVars f2 vF2 m2 /\
eval_exp (updEnv 2 vF2 (updEnv 1 vF1 emptyEnv)) eval_exp (updEnv 2 vF2 (updEnv 1 vF1 emptyEnv))
(fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop b (Var R 1) (Var R 2)) vF m. (Binop b (Var R 1) (Var R 2)) vF m.
Proof. Proof.
intros eval_float. intros eval_float.
......