Commit 7f36eb27 authored by ='s avatar =
Browse files

Continuing the Port of errorvalidation

parent 4d669498
......@@ -14,6 +14,7 @@ expression may yield different values for different machine epsilons
**)
Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
|approxRefl A:
(* TODO: this is weird. why not start with defVars?*)
approxEnv emptyEnv (fun n => None) A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
approxEnv E1 defVars A fVars dVars E2 ->
......
......@@ -98,7 +98,7 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
Lemma expEqBool_refl e:
expEqBool e e = true.
Proof.
induction e; try (apply andb_true_iff; split); simpl in *; auto; try (apply EquivEqBoolEq; auto).
induction e; try (apply andb_true_iff; split); simpl in *; auto; try (apply EquivEqBoolEq; auto).
- symmetry; apply beq_nat_refl.
- apply Qeq_bool_iff; lra.
- case u; auto.
......@@ -113,14 +113,14 @@ Proof.
case_eq (a =? b); intros.
- apply beq_nat_true in H.
rewrite H.
apply beq_nat_refl.
apply beq_nat_refl.
- apply beq_nat_false in H.
case_eq (b =? a); intros.
+ apply beq_nat_true in H0.
rewrite H0 in H.
auto.
+ auto.
Qed.
Qed.
Lemma expEqBool_sym e e':
expEqBool e e' = expEqBool e' e.
......@@ -134,7 +134,7 @@ Proof.
- f_equal.
+ destruct u; auto.
+ apply IHe.
- f_equal.
- f_equal.
+ destruct b; auto.
+ f_equal.
* apply IHe1.
......@@ -154,7 +154,7 @@ Proof.
apply beq_nat_true in H1.
subst.
unfold expEqBool.
rewrite <- beq_nat_refl.
rewrite <- beq_nat_refl.
auto.
- apply EquivEqBoolEq in H1.
apply EquivEqBoolEq in H.
......@@ -184,7 +184,7 @@ Proof.
eapply IHe; eauto.
Qed.
Fixpoint toRExp (e:exp Q) :=
match e with
......@@ -289,7 +289,7 @@ Proof.
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
- inversion eval_v1; inversion eval_v2; subst; auto;
try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
+ apply Ropp_eq_compat. apply (IHf v0 v3 M0); auto.
+ apply Ropp_eq_compat. apply (IHf v0 v3 M0); auto.
+ inversion H4.
+ inversion H5.
+ rewrite (IHf v0 v3 M0); auto.
......@@ -317,7 +317,7 @@ Qed.
(* - simpl; auto. *)
(* Qed. *)
(**
Evaluation with 0 as machine epsilon is deterministic
**)
......@@ -329,7 +329,7 @@ Lemma meps_0_deterministic (f:exp R) (E:env) defVars:
Proof.
intros v1 v2 ev1 ev2.
assert (M0 = M0) by auto.
apply (general_meps_0_deterministic f H ev1 ev2).
apply (general_meps_0_deterministic f H ev1 ev2).
Qed.
......
......@@ -45,7 +45,7 @@ Fixpoint typeCmd (defVars:nat -> option mType) (f:cmd Q): option mType :=
else None
|None => None
end
|Ret e => typeExpression defVars e
|Ret e => typeExpression defVars e
end.
Fixpoint typeMapCmd (defVars:nat -> option mType) (f:cmd Q) (f':exp Q) : option mType :=
......@@ -106,84 +106,84 @@ Fixpoint typeCheckCmd (c:cmd Q) (defVars:nat -> option mType) (tMap:exp Q -> opt
| Ret e => typeCheck e defVars tMap
end.
Lemma eqTypeExpression e m defVars:
typeMap defVars e e = Some m <-> typeExpression defVars e = Some m.
Proof.
revert m defVars; induction e; intros.
- split; intros.
+ simpl in *.
rewrite <- beq_nat_refl in H; simpl in H; auto.
+ simpl in *.
rewrite <- beq_nat_refl; simpl; auto.
- split; intros; simpl in *.
+ rewrite mTypeEqBool_refl,Qeq_bool_refl in H; simpl in H; auto.
+ rewrite mTypeEqBool_refl,Qeq_bool_refl; simpl; auto.
- split; intros; simpl in *.
+ rewrite unopEqBool_refl,expEqBool_refl in H; simpl in H; auto.
+ rewrite unopEqBool_refl,expEqBool_refl; simpl; auto.
- split; intros; simpl in *.
+ rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl in H; simpl in H; auto.
+ rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl; simpl; auto.
- split; intros; simpl in *.
+ rewrite mTypeEqBool_refl,expEqBool_refl in H; simpl in H; auto.
+ rewrite mTypeEqBool_refl,expEqBool_refl; simpl; auto.
Qed.
(* Lemma eqTypeExpression e m defVars: *)
(* typeMap defVars e e = Some m <-> typeExpression defVars e = Some m. *)
(* Proof. *)
(* revert m defVars; induction e; intros. *)
(* - split; intros. *)
(* + simpl in *. *)
(* rewrite <- beq_nat_refl in H; simpl in H; auto. *)
(* + simpl in *. *)
(* rewrite <- beq_nat_refl; simpl; auto. *)
(* - split; intros; simpl in *. *)
(* + rewrite mTypeEqBool_refl,Qeq_bool_refl in H; simpl in H; auto. *)
(* + rewrite mTypeEqBool_refl,Qeq_bool_refl; simpl; auto. *)
(* - split; intros; simpl in *. *)
(* + rewrite unopEqBool_refl,expEqBool_refl in H; simpl in H; auto. *)
(* + rewrite unopEqBool_refl,expEqBool_refl; simpl; auto. *)
(* - split; intros; simpl in *. *)
(* + rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl in H; simpl in H; auto. *)
(* + rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl; simpl; auto. *)
(* - split; intros; simpl in *. *)
(* + rewrite mTypeEqBool_refl,expEqBool_refl in H; simpl in H; auto. *)
(* + rewrite mTypeEqBool_refl,expEqBool_refl; simpl; auto. *)
(* Qed. *)
Definition Gamma_stronger (Gamma1 Gamma2: exp Q -> option mType):=
(forall e m, Gamma1 e = Some m -> Gamma2 e = Some m).
(* Definition Gamma_stronger (Gamma1 Gamma2: exp Q -> option mType):= *)
(* (forall e m, Gamma1 e = Some m -> Gamma2 e = Some m). *)
Lemma Gamma_stronger_trans Gamma1 Gamma2 Gamma3 :
Gamma_stronger Gamma1 Gamma2 ->
Gamma_stronger Gamma2 Gamma3 ->
Gamma_stronger Gamma1 Gamma3.
Proof.
intros g12 g23 e m hyp.
unfold Gamma_stronger in g12,g23.
apply g23; apply g12; auto.
Qed.
(* Lemma Gamma_stronger_trans Gamma1 Gamma2 Gamma3 : *)
(* Gamma_stronger Gamma1 Gamma2 -> *)
(* Gamma_stronger Gamma2 Gamma3 -> *)
(* Gamma_stronger Gamma1 Gamma3. *)
(* Proof. *)
(* intros g12 g23 e m hyp. *)
(* unfold Gamma_stronger in g12,g23. *)
(* apply g23; apply g12; auto. *)
(* Qed. *)
Lemma Gamma_strengthening e Gamma1 Gamma2 defVars:
Gamma_stronger Gamma1 Gamma2 ->
typeCheck e defVars Gamma1 = true ->
typeCheck e defVars Gamma2 = true.
Proof.
revert Gamma1 Gamma2; induction e; intros.
- simpl in *.
case_eq (Gamma1 (Var Q n)); intros; rewrite H1 in H0; [ | inversion H0 ].
specialize (H _ _ H1); rewrite H.
auto.
- simpl in *.
case_eq (Gamma1 (Const m v)); intros; rewrite H1 in H0; [ | inversion H0 ].
specialize (H _ _ H1); rewrite H.
auto.
- simpl in *.
case_eq (Gamma1 (Unop u e)); intros; rewrite H1 in H0; [ | inversion H0 ].
rewrite (H _ _ H1).
case_eq (Gamma1 e); intros; rewrite H2 in H0; [ | inversion H0 ].
apply andb_true_iff in H0; destruct H0.
apply EquivEqBoolEq in H0; subst.
rewrite (H _ _ H2).
rewrite mTypeEqBool_refl; simpl.
eapply IHe; eauto.
- simpl in *.
case_eq (Gamma1 (Binop b e1 e2)); intros; rewrite H1 in H0; [ | inversion H0 ].
case_eq (Gamma1 e1); intros; rewrite H2 in H0; [ | inversion H0 ].
case_eq (Gamma1 e2); intros; rewrite H3 in H0; [ | inversion H0 ].
rewrite (H _ _ H1), (H _ _ H2), (H _ _ H3).
andb_to_prop H0.
rewrite L0; simpl.
apply andb_true_iff; split.
+ eapply IHe1; eauto.
+ eapply IHe2; eauto.
- simpl in *.
case_eq (Gamma1 (Downcast m e)); intros; rewrite H1 in H0; [ | inversion H0 ].
case_eq (Gamma1 e); intros; rewrite H2 in H0; [ | inversion H0 ].
rewrite (H _ _ H1), (H _ _ H2).
andb_to_prop H0.
rewrite L0, R0; simpl.
eapply IHe; eauto.
Qed.
(* Lemma Gamma_strengthening e Gamma1 Gamma2 defVars: *)
(* Gamma_stronger Gamma1 Gamma2 -> *)
(* typeCheck e defVars Gamma1 = true -> *)
(* typeCheck e defVars Gamma2 = true. *)
(* Proof. *)
(* revert Gamma1 Gamma2; induction e; intros. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Var Q n)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* specialize (H _ _ H1); rewrite H. *)
(* auto. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Const m v)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* specialize (H _ _ H1); rewrite H. *)
(* auto. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Unop u e)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* rewrite (H _ _ H1). *)
(* case_eq (Gamma1 e); intros; rewrite H2 in H0; [ | inversion H0 ]. *)
(* apply andb_true_iff in H0; destruct H0. *)
(* apply EquivEqBoolEq in H0; subst. *)
(* rewrite (H _ _ H2). *)
(* rewrite mTypeEqBool_refl; simpl. *)
(* eapply IHe; eauto. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Binop b e1 e2)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* case_eq (Gamma1 e1); intros; rewrite H2 in H0; [ | inversion H0 ]. *)
(* case_eq (Gamma1 e2); intros; rewrite H3 in H0; [ | inversion H0 ]. *)
(* rewrite (H _ _ H1), (H _ _ H2), (H _ _ H3). *)
(* andb_to_prop H0. *)
(* rewrite L0; simpl. *)
(* apply andb_true_iff; split. *)
(* + eapply IHe1; eauto. *)
(* + eapply IHe2; eauto. *)
(* - simpl in *. *)
(* case_eq (Gamma1 (Downcast m e)); intros; rewrite H1 in H0; [ | inversion H0 ]. *)
(* case_eq (Gamma1 e); intros; rewrite H2 in H0; [ | inversion H0 ]. *)
(* rewrite (H _ _ H1), (H _ _ H2). *)
(* andb_to_prop H0. *)
(* rewrite L0, R0; simpl. *)
(* eapply IHe; eauto. *)
(* Qed. *)
Theorem typingSoundnessExp e defVars E:
......
......@@ -5,18 +5,19 @@ open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory
val _ = new_theory "Environments";
val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(!(A:analysisResult).
approxEnv emptyEnv A LN LN emptyEnv) /\
(!(E1:env) (E2:env) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 A fVars dVars E2 /\
(abs (v1 - v2) <= abs v1 * machineEpsilon) /\
(!(defVars: num -> mType option) (A:analysisResult).
approxEnv emptyEnv defVars A LN LN emptyEnv) /\
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 defVars A fVars dVars E2 /\
(defVars x = SOME m) /\
(abs (v1 - v2) <= abs v1 * (meps m)) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) A (insert x () fVars) dVars (updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 A fVars dVars E2 /\
approxEnv (updEnv x v1 E1) defVars A (insert x () fVars) dVars (updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 defVars A fVars dVars E2 /\
(abs (v1 - v2) <= SND (A (Var x))) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) A fVars (insert x () dVars) (updEnv x v2 E2))`;
approxEnv (updEnv x v1 E1) defVars A fVars (insert x () dVars) (updEnv x v2 E2))`;
val [approxRefl, approxUpdFree, approxUpdBound] = CONJ_LIST 3 approxEnv_rules;
save_thm ("approxRefl", approxRefl);
......
......@@ -8,8 +8,8 @@
**)
open preamble
open simpLib realTheory realLib RealArith pred_setTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics MachineTypeTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory TypingTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
val _ = new_theory "ErrorValidation";
......@@ -17,23 +17,24 @@ val _ = new_theory "ErrorValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val validErrorbound_def = Define `
validErrorbound e (absenv:analysisResult) (dVars:num_set)=
validErrorbound e (typeMap: real exp -> mType option) (absenv:analysisResult) (dVars:num_set)=
let (intv, err) = absenv e in
if (0 <= err)
then
let mopt = typeMap e in
case mopt of
| NONE => F
| SOME m =>
if (0 <= err) then
case e of
| Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * machineEpsilon <= err)
| Const n => (maxAbs intv * machineEpsilon <= err)
| Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * (meps m) <= err)
| Const _ n => (maxAbs intv * (meps m) <= err)
| Unop Neg f =>
if (validErrorbound f absenv dVars)
then
if (validErrorbound f typeMap absenv dVars) then
err = (SND (absenv f))
else
F
| Unop Inv f => F
| Binop op f1 f2 =>
(if (validErrorbound f1 absenv dVars /\ validErrorbound f2 absenv dVars)
then
(if (validErrorbound f1 typeMap absenv dVars /\ validErrorbound f2 typeMap absenv dVars) then
let (ive1, err1) = absenv f1 in
let (ive2, err2) = absenv f2 in
let errIve1 = widenInterval ive1 err1 in
......@@ -41,52 +42,62 @@ val validErrorbound_def = Define `
let upperBoundE1 = maxAbs ive1 in
let upperBoundE2 = maxAbs ive2 in
case op of
| Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * machineEpsilon) <= err
| Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * machineEpsilon) <= err
| Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * machineEpsilon) <= err
| Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * (meps m)) <= err
| Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * (meps m)) <= err
| Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * (meps m)) <= err
| Div =>
(if (IVhi errIve2 < 0 \/ 0 < IVlo errIve2)
then
let upperBoundInvE2 = maxAbs (invertInterval ive2) in
let minAbsIve2 = minAbsFun (errIve2) in
let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in
((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * machineEpsilon) <= err)
((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * (meps m)) <= err)
else F)
else F)
| Downcast m1 e1 =>
let (ive1, err1) = absenv e1 in
let rec_res = validErrorbound e1 typeMap absenv dVars in
let errIve1 = widenInterval ive1 err1 in
rec_res /\ ( (err1 + maxAbs errIve1 * (meps m1)) <= err)
else F`;
val validErrorboundCmd_def = Define `
validErrorboundCmd (f:real cmd) (env:analysisResult) (dVars:num_set)=
validErrorboundCmd (f:real cmd) (typeMap: real exp -> mType option) (env:analysisResult) (dVars:num_set)=
case f of
| Let x e g =>
if validErrorboundCmd g env (insert x () dVars)
then
(validErrorbound e env dVars/\
(env e = env (Var x)))
else F
| Ret e =>
validErrorbound e env dVars`;
| Let m x e g =>
(* TODO: compare env eq test with coq *)
if (validErrorbound e typeMap env dVars /\ (env e = env (Var x))) then
validErrorboundCmd g typeMap env (insert x () dVars)
else F
| Ret e =>
validErrorbound e typeMap env dVars`;
val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
val err_always_positive = store_thm ("err_always_positive",
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real) dVars.
(validErrorbound (e:real exp) (absenv:analysisResult) dVars) /\
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real) dVars (tmap: real exp -> mType option).
(validErrorbound e tmap absenv dVars) /\
((iv,err) = absenv e) ==>
0 <= err``,
once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\
Cases_on `e` \\
qpat_assum `(iv,err) = absenv e` (fn thm => fs [GSYM thm]) \\
Cases_on `absenv e0` \\ Cases_on `absenv e'` \\ fs[]);
qpat_assum `(iv,err) = absenv e` (fn thm => fs [GSYM thm])
>- (Cases_on `tmap (Var n)` \\ fs [])
>- (Cases_on `tmap (Const m v)` \\ fs [])
>- (Cases_on `tmap (Unop u e')` \\ fs [])
>- (Cases_on `tmap (Binop b e' e0)` \\ fs [])
>- (Cases_on `tmap (Downcast m e')` \\ fs []));
val validErrorboundCorrectVariable_ind = prove (
``!(E1 E2:env) absenv fVars dVars.
approxEnv E1 absenv fVars dVars E2 ==>
!(v:num) (nR nF err nlo nhi:real) (P:precond).
eval_exp 0 E1 (Var v) nR /\
eval_exp machineEpsilon E2 (Var v) nF /\
``!(E1 E2:env) absenv fVars dVars defVars.
approxEnv E1 defVars absenv fVars dVars E2 ==>
!(v:num) (nR nF err nlo nhi:real) (P:precond) (Gamma: real exp -> mType option) m.
typeCheck (Var v) defVars Gamma /\
eval_exp E1 (toREvalVars defVars) (toREval (Var v)) nR M0 /\
eval_exp E2 defVars (Var v) nF m /\
validIntervalbounds (Var v) absenv P dVars /\
validErrorbound (Var v) absenv dVars /\
validErrorbound (Var v) Gamma absenv dVars /\
(!v.
v IN domain dVars ==>
?r.
......@@ -102,12 +113,13 @@ val validErrorboundCorrectVariable_ind = prove (
abs (nR - nF) <= err``,
(* rule induction on approximation relation *)
qspec_then
`\E1 absenv fVars dVars E2.
!(v:num) (nR nF err nlo nhi:real) (P:precond).
eval_exp 0 E1 (Var v) nR /\
eval_exp machineEpsilon E2 (Var v) nF /\
`\E1 defVars absenv fVars dVars E2.
!(v:num) (nR nF err nlo nhi:real) (P:precond) (Gamma: real exp -> mType option) m.
typeCheck (Var v) defVars Gamma /\
eval_exp E1 (toREvalVars defVars) (toREval (Var v)) nR M0 /\
eval_exp E2 defVars (Var v) nF m /\
validIntervalbounds (Var v) absenv P dVars /\
validErrorbound (Var v) absenv dVars /\
validErrorbound (Var v) Gamma absenv dVars /\
(!v.
v IN domain dVars ==>
?r.
......@@ -123,8 +135,8 @@ val validErrorboundCorrectVariable_ind = prove (
abs (nR - nF) <= err` (fn thm => ASSUME_TAC (SIMP_RULE std_ss [] thm)) approxEnv_ind
\\ first_x_assum match_mp_tac
\\ rpt strip_tac
\\ inversion `eval_exp 0 _ _ _` eval_exp_cases
\\ inversion `eval_exp machineEpsilon _ _ _` eval_exp_cases
\\ fs [toREval_def] \\ inversion `eval_exp _ _ _ _ M0` eval_exp_cases
\\ inversion `eval_exp _ defVars _ _ _` eval_exp_cases
>- (fs [emptyEnv_def])
>- (fs[updEnv_def]
\\ Cases_on `v = x` \\ rveq
......@@ -133,11 +145,15 @@ val validErrorboundCorrectVariable_ind = prove (
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ conj_tac \\ fs []
\\ fs [typeCheck_def]
\\ `Gamma (Var v) = SOME m` by (Cases_on `Gamma (Var v)` \\ rveq \\ fs [] \\ rveq)
\\ qpat_assum `Gamma _ = SOME _` (fn thm => fs [thm]) \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (nlo, nhi) * machineEpsilon`
\\ qexists_tac `maxAbs (nlo, nhi) * (meps m)`
\\ conj_tac \\ fs []
\\ match_mp_tac REAL_LE_RMUL_IMP
\\ fs [mEps_geq_zero]
\\ conj_tac \\ fs [meps_def,inj_eps_pos]
\\ match_mp_tac contained_leq_maxAbs
\\ rewrite_tac [contained_def, IVlo_def, IVhi_def]
\\ qspecl_then [`Var v`, `A`] ASSUME_TAC validIntervalbounds_sound
......@@ -149,9 +165,9 @@ val validErrorboundCorrectVariable_ind = prove (
\\ rpt conj_tac
>- (fs [usedVars_def, SUBSET_DEF, domain_insert])
>- (rpt strip_tac \\ first_x_assum match_mp_tac \\ fs [])
>- (match_mp_tac Var_load \\ fs [updEnv_def]))
>- (fs [toREval_def] \\ match_mp_tac Var_load \\ fs [updEnv_def,toREvalVars_def]))
>- (first_x_assum match_mp_tac
\\ qexistsl_tac [`v`, `nlo`, `nhi`, `P`]
\\ qexistsl_tac [`v`, `nlo`, `nhi`, `P`, `Gamma`, `m'`]
\\ fs []
\\ rpt conj_tac
>- (match_mp_tac Var_load \\ fs [])
......@@ -179,7 +195,8 @@ val validErrorboundCorrectVariable_ind = prove (
>- (fs [validErrorbound_def, lookup_union]
\\ rveq \\ Cases_on `lookup v fVars` \\ fs[])
>- (first_x_assum match_mp_tac
\\ qexistsl_tac [`v`, `nlo`, `nhi`, `P`]
\\ qexistsl_tac [`v`, `nlo`, `nhi`, `P`, `Gamma`, `m`]
\\ fs []
\\ rpt conj_tac
>- (match_mp_tac Var_load \\ fs [])
>- (match_mp_tac Var_load \\ fs [])
......@@ -202,16 +219,16 @@ val validErrorboundCorrectVariable_ind = prove (
>- (rveq \\ fs [lookup_union]
\\ Cases_on `lookup v' fVars`
\\ fs [domain_lookup])
>- (rveq \\ fs []))
>- (fs []))));
>- (rveq \\ fs [])))));
val validErrorboundCorrectVariable = store_thm ("validErrorboundCorrectVariable",
``!(E1 E2:env) absenv fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond).
approxEnv E1 absenv fVars dVars E2 /\
eval_exp 0 E1 (Var v) nR /\
eval_exp machineEpsilon E2 (Var v) nF /\
``!(E1 E2:env) absenv fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond) m Gamma defVars.
typeCheck (Var v) defVars Gamma /\
approxEnv E1 defVars absenv fVars dVars E2 /\
eval_exp E1 (toREvalVars defVars) (toREval (Var v)) nR M0 /\
eval_exp E2 defVars (Var v) nF m /\
validIntervalbounds (Var v) absenv P dVars /\
validErrorbound (Var v) absenv dVars /\
validErrorbound (Var v) Gamma absenv dVars /\
(!v.
v IN domain dVars ==>
?r.
......@@ -227,46 +244,54 @@ val validErrorboundCorrectVariable = store_thm ("validErrorboundCorrectVariable"
abs (nR - nF) <= err``,
rpt strip_tac
\\ drule validErrorboundCorrectVariable_ind
\\ disch_then (fn thm => qspecl_then [`v`, `nR`, `nF`, `err`, `nlo`, `nhi`, `P`] ASSUME_TAC thm)
\\ disch_then (fn thm => qspecl_then [`v`, `nR`, `nF`, `err`, `nlo`, `nhi`, `P`, `Gamma`, `m`] ASSUME_TAC thm)
\\ fs []);
val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant",
``!(E1 E2:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) dVars.
eval_exp 0 E1 (Const n) nR /\
eval_exp machineEpsilon E2 (Const n) nF /\
validErrorbound (Const n) absenv dVars /\
FST (FST (absenv (Const n))) <= nR /\
nR <= SND (FST (absenv (Const n))) /\
(absenv (Const n) = ((nlo,nhi),e)) ==>
``!(E1 E2:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) dVars m Gamma defVars.
eval_exp E1 (toREvalVars defVars) (toREval (Const m n)) nR M0 /\
eval_exp E2 defVars (Const m n) nF m /\
typeCheck (Const m n) defVars Gamma /\
validErrorbound (Const m n) Gamma absenv dVars /\
FST (FST (absenv (Const m n))) <= nR /\
nR <= SND (FST (absenv (Const m n))) /\
(absenv (Const m n) = ((nlo,nhi),e)) ==>
(abs (nR - nF)) <= e``,
once_rewrite_tac [validErrorbound_def]
\\ rpt strip_tac \\ fs[]
\\ inversion `eval_exp 0 _ (Const n) nR` eval_exp_cases \\ rveq
\\ simp [delta_0_deterministic]
\\ inversion `eval_exp machineEpsilon _ _ _` eval_exp_cases \\ rveq
\\ fs [toREval_def] \\ inversion `eval_exp _ _ _ _ M0` eval_exp_cases \\ rveq
\\ simp [delta_M0_deterministic]
\\ inversion `eval_exp _ _ _ _ m` eval_exp_cases \\ rveq
\\ simp[perturb_def]
\\ rename1 `abs deltaF <= machineEpsilon`
\\ rename1 `abs deltaF <= (meps m)`
\\ simp [Rabs_err_simpl, ABS_MUL]
\\ fs [typeCheck_def]
\\ `Gamma (Const m n) = SOME m` by (Cases_on `Gamma (Const m n)` \\ fs [] \\ rveq)
\\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (nlo, nhi) * machineEpsilon` \\ conj_tac \\ TRY (simp[])
\\ qexists_tac `maxAbs (nlo, nhi) * (meps m)` \\ conj_tac \\ TRY (simp[])
\\ match_mp_tac REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp[ABS_POS])
\\ simp[maxAbs_def]
\\ match_mp_tac maxAbs
\\ qspecl_then [`delta`, `n`] (fn thm => fs [thm]) delta_0_deterministic
\\ qspecl_then [`delta`] (fn thm => fs [thm]) delta_M0_deterministic
\\ qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2))
\\ simp[]);
val validErrorboundCorrectAddition = store_thm ("validErrorboundCorrectAddition",
``!(E1 E2:env) (absenv:analysisResult) (e1:real exp) (e2:real exp)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) dVars.
eval_exp 0 E1 e1 nR1 /\
eval_exp 0 E1 e2 nR2 /\
eval_exp 0 E1 (Binop Plus e1 e2) nR /\
eval_exp machineEpsilon E2 e1 nF1 /\
eval_exp machineEpsilon E2 e2 nF2 /\
eval_exp machineEpsilon
(updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (Binop Plus (Var 1) (Var 2)) nF /\
validErrorbound (Binop Plus e1 e2) absenv dVars /\
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 Gamma defVars.
(m = computeJoin m1 m2) /\
eval_exp E1 (toREvalVars defVars) (toREval e1) nR1 M0 /\
eval_exp E1 (toREvalVars defVars) (toREval e2) nR2 M0 /\
eval_exp E1 (toREvalVars defVars) (toREval (Binop Plus e1 e2)) nR M0 /\<