Commit c42a6ab3 authored by Heiko Becker's avatar Heiko Becker
Browse files

Make eval_0_det proper proof in HOL-Light style and simplify coq dev

parent 692353f0
...@@ -56,10 +56,10 @@ Proof. ...@@ -56,10 +56,10 @@ Proof.
rewrite (perturb_0_val (eval_binop Plus v1 v2) delta); auto. rewrite (perturb_0_val (eval_binop Plus v1 v2) delta); auto.
unfold eval_binop in *; simpl in *. unfold eval_binop in *; simpl in *.
clear delta H2. clear delta H2.
rewrite (eval_det H4 e1_real); rewrite (eval_0_det H4 e1_real);
rewrite (eval_det H5 e2_real). rewrite (eval_0_det H5 e2_real).
rewrite (eval_det H4 e1_real) in plus_real. rewrite (eval_0_det H4 e1_real) in plus_real.
rewrite (eval_det H5 e2_real) in plus_real. rewrite (eval_0_det H5 e2_real) in plus_real.
clear H4 H5 v1 v2. clear H4 H5 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *) (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion plus_float; subst. inversion plus_float; subst.
...@@ -115,10 +115,10 @@ Proof. ...@@ -115,10 +115,10 @@ Proof.
rewrite perturb_0_val; auto. rewrite perturb_0_val; auto.
unfold eval_binop in *; simpl in *. unfold eval_binop in *; simpl in *.
clear delta H2. clear delta H2.
rewrite (eval_det H4 e1_real); rewrite (eval_0_det H4 e1_real);
rewrite (eval_det H5 e2_real). rewrite (eval_0_det H5 e2_real).
rewrite (eval_det H4 e1_real) in sub_real. rewrite (eval_0_det H4 e1_real) in sub_real.
rewrite (eval_det H5 e2_real) in sub_real. rewrite (eval_0_det H5 e2_real) in sub_real.
clear H4 H5 v1 v2. clear H4 H5 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *) (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion sub_float; subst. inversion sub_float; subst.
...@@ -183,10 +183,10 @@ Proof. ...@@ -183,10 +183,10 @@ Proof.
rewrite perturb_0_val; auto. rewrite perturb_0_val; auto.
unfold eval_binop in *; simpl in *. unfold eval_binop in *; simpl in *.
clear delta H2. clear delta H2.
rewrite (eval_det H4 e1_real); rewrite (eval_0_det H4 e1_real);
rewrite (eval_det H5 e2_real). rewrite (eval_0_det H5 e2_real).
rewrite (eval_det H4 e1_real) in mult_real. rewrite (eval_0_det H4 e1_real) in mult_real.
rewrite (eval_det H5 e2_real) in mult_real. rewrite (eval_0_det H5 e2_real) in mult_real.
clear H4 H5 v1 v2. clear H4 H5 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *) (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion mult_float; subst. inversion mult_float; subst.
......
...@@ -75,7 +75,7 @@ Proof. ...@@ -75,7 +75,7 @@ Proof.
rewrite Rplus_0_r; auto. rewrite Rplus_0_r; auto.
Qed. Qed.
Lemma eval_det (e:exp R) (env:env_ty): Lemma eval_0_det (e:exp R) (env:env_ty):
forall v1 v2, forall v1 v2,
eval_exp R0 env e v1 -> eval_exp R0 env e v1 ->
eval_exp R0 env e v2 -> eval_exp R0 env e v2 ->
...@@ -112,33 +112,6 @@ Proof. ...@@ -112,33 +112,6 @@ Proof.
constructor; auto. constructor; auto.
Qed. Qed.
Lemma sub_to_plus eps cenv e1 e2 v v2 v1:
eval_exp eps cenv e1 v1 ->
eval_exp eps cenv e2 v2 ->
eval_exp eps (updEnv 1 v1 (updEnv 2 (- v2) cenv)) (Binop Plus (Var R 1) (Var R 2)) v <->
eval_exp eps (updEnv 1 v1 (updEnv 2 v2 cenv)) (Binop Sub (Var R 1) (Var R 2)) v.
Proof.
intros eval_e2.
split.
- intros.
inversion H0; subst.
inversion H7; subst.
unfold eval_binop; simpl. unfold updEnv at 3; unfold updEnv at 3; simpl.
rewrite <- Rsub_eq_Ropp_Rplus.
constructor; auto.
+ inversion H6; subst. unfold updEnv at 3; unfold updEnv at 3; simpl. apply Var_load.
+ unfold updEnv at 3 in H7; unfold updEnv at 3 in H7; simpl in H7.
apply Var_load.
- intros.
inversion H0; subst.
inversion H7; subst.
unfold eval_binop; simpl. unfold updEnv at 3; unfold updEnv at 3; simpl.
rewrite Rsub_eq_Ropp_Rplus.
constructor; auto.
+ inversion H6; subst. unfold updEnv in *; simpl in *; apply Var_load.
+ unfold updEnv in *; simpl in *. apply Var_load.
Qed.
(** (**
Using the parametric expressions, define boolean expressions for conditionals Using the parametric expressions, define boolean expressions for conditionals
**) **)
......
-R . Daisy -R . Daisy
./IntervalValidation.v
./Expressions.v ./Expressions.v
./AbsoluteError.v ./AbsoluteError.v
./Infra/RealSimps.v
./Infra/Abbrevs.v ./Infra/Abbrevs.v
./Infra/ExpressionAbbrevs.v
./Infra/RationalConstruction.v
./Infra/RealRationalProps.v
./Infra/RealConstruction.v ./Infra/RealConstruction.v
./Infra/RationalSimps.v
./Commands.v ./Commands.v
./ErrorValidation.v
./IntervalArithQ.v
./IntervalArith.v ./IntervalArith.v
./SimpleDoppler.v ./ErrorBounds.v
./VerificationTests/SimpleDoppler.v
./VerificationTests/SimpleMultiplication.v
...@@ -9,57 +9,49 @@ needs "Expressions.hl";; ...@@ -9,57 +9,49 @@ needs "Expressions.hl";;
let updEnv = define let updEnv = define
`updEnv (x:num) (v:V) (E:num->V) =(\y. if y = x then v else E y)`;; `updEnv (x:num) (v:V) (E:num->V) =(\y. if y = x then v else E y)`;;
(**
TODO: Check wether we need Rabs (n * machineEpsilon) instead
**)
let const_abs_err_bounded = let const_abs_err_bounded =
prove ( prove (
`!(n:real) (nR:real) (nF:real) (cenv:num->real). `!(n:real) (nR:real) (nF:real) (cenv:num ->real).
eval_exp (&0) cenv (Const n) nR /\ eval_exp (&0) cenv (Const n) nR /\
eval_exp machineEpsilon cenv (Const n) nF ==> eval_exp machineEpsilon cenv (Const n) nF ==>
abs (nR - nF) <= abs (n * machineEpsilon)`, abs (nR - nF) <= abs n * machineEpsilon`,
intros "!n nR nF cenv; eval_real eval_float" intros "!n nR nF cenv; eval_real eval_float"
THEN (USE_THEN "eval_real" THEN RULE_ASSUM_TAC (MATCH_MP const_inv)
(fun th -> LABEL_TAC "eval_const_simps" THEN destruct "eval_real" "@d1. nR_eq abs_d1_0"
(MP (SPECL [`&0:real`;`cenv:num->real`; `n:real`; `nR:real`]const_inv) th))) THEN destruct "eval_float" "@d2. nF_eq abs_d2_leq"
THEN destruct "eval_const_simps" "@delta. nR_perturb abs_leq_0" THEN ASM_SIMP_TAC []
THEN ASM_SIMP_TAC[] THEN USE_THEN "abs_d1_0"
THEN (USE_THEN "abs_leq_0" (fun th ->
(fun th -> REWRITE_TAC [MP (SPECL [`n:real`; `delta:real`] perturb_0_val) th])) ASM_REWRITE_TAC [MP (SPECL [`(n:real)`; `d1:real`] perturb_0_val) th])
THEN (USE_THEN "eval_float" THEN REWRITE_TAC [perturb;abs_err_simpl; REAL_ABS_MUL]
(fun th -> LABEL_TAC "eval_const_float" THEN MATCH_MP_TAC REAL_LE_LMUL
(MP (SPECL [`machineEpsilon:real`;`cenv:num->real`; `n:real`; `nF:real`]const_inv) th))) THEN ASM_REWRITE_TAC [REAL_ABS_POS]);;
THEN destruct "eval_const_float" "@delta2. nF_eq abs_leq_meps"
THEN ASM_SIMP_TAC[perturb]
THEN REWRITE_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
THEN mp REAL_LE_LMUL THEN split THEN TRY auto
THEN SIMP_TAC [REAL_ABS_POS]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `machineEpsilon:real` THEN split THEN TRY auto
THEN SIMP_TAC[REAL_ABS_LE]);;
(**
TODO: Maybe improve bound by adding interval constraint and proving that it is leq than maxAbs of bounds
(nlo <= cenv n <= nhi)%R -> (Rabs (nR - nF) <= Rabs ((Rmax (Rabs nlo) (Rabs nhi)) * machineEpsilon))%R.
**)
let param_abs_err_bounded = let param_abs_err_bounded =
prove ( prove (
`!(v:num) (nR:real) (nF:real) (cenv:num->real). `!(n:num) (nR:real) (nF:real) (cenv:num->real).
eval_exp (&0) cenv (Param v) nR /\ eval_exp (&0) cenv (Param n) nR /\
eval_exp machineEpsilon cenv (Param v) nF ==> eval_exp machineEpsilon cenv (Param n) nF ==>
abs (nR - nF) <= abs ((cenv v) * machineEpsilon)`, (abs (nR - nF) <= abs (cenv n) * machineEpsilon)`,
intros "!v nR nF cenv; eval_real eval_float" intros "!n nR nF cenv; eval_real eval_float"
THEN (USE_THEN "eval_real" THEN RULE_ASSUM_TAC (MATCH_MP param_inv)
(fun th -> LABEL_TAC "eval_const_simps" THEN destruct "eval_real" "@d1. nR_eq abs_d1_0"
(MP (SPECL [`&0:real`;`cenv:num->real`; `v:num`; `nR:real`] param_inv) th))) THEN destruct "eval_float" "@d2. nF_eq abs_d1_leq"
THEN destruct "eval_const_simps" "@delta. nR_perturb abs_leq_0"
THEN ASM_SIMP_TAC[] THEN ASM_SIMP_TAC[]
THEN (USE_THEN "abs_leq_0" THEN USE_THEN "abs_d1_0"
(fun th -> REWRITE_TAC [MP (SPECL [`n:real`; `delta:real`] perturb_0_val) th])) (fun th ->
THEN (USE_THEN "eval_float" ASM_REWRITE_TAC [MP (SPECL [`(cenv n:real)`; `d1:real`] perturb_0_val) th])
(fun th -> LABEL_TAC "eval_const_float" THEN REWRITE_TAC [perturb; abs_err_simpl; REAL_ABS_MUL]
(MP (SPECL [`machineEpsilon:real`;`cenv:num->real`; `v:num`; `nF:real`] param_inv) th))) THEN MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[REAL_ABS_POS]);;
THEN destruct "eval_const_float" "@delta2. nF_eq abs_leq_meps"
THEN ASM_SIMP_TAC[perturb]
THEN REWRITE_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
THEN mp REAL_LE_LMUL THEN split THEN TRY auto
THEN SIMP_TAC [REAL_ABS_POS]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `machineEpsilon:real` THEN split THEN TRY auto
THEN SIMP_TAC[REAL_ABS_LE]);;
let add_abs_err_bounded = let add_abs_err_bounded =
prove ( prove (
......
(* (**
Formalization of the base expression language for the daisy framework Formalization of the base expression language for the daisy framework
*) **)
needs "Infra/tactics.hl";; needs "Infra/tactics.hl";;
needs "Infra/RealConstruction.hl";; needs "Infra/RealConstruction.hl";;
(* needs "Infra/RealSimps.hl";;
(**
Expressions will use binary operators. Expressions will use binary operators.
Define them first Define them first
*) **)
let binop_IND, binop_REC = define_type let binop_IND, binop_REC = define_type
"binop = Plus | Sub | Mult | Div ";; "binop = Plus | Sub | Mult | Div ";;
(* (**
Define an evaluation function for binary operators. Next define an evaluation function for binary operators.
Errors are added on the expression evaluation level later Errors are added on the expression evaluation level later
*) *)
let eval_binop = new_recursive_definition binop_REC let eval_binop = new_recursive_definition binop_REC
`(eval_binop Plus v1 v2 = v1 + v2) /\ `(eval_binop Plus v1 v2 = v1 + v2) /\
(eval_binop Sub v1 v2 = v1 - v2) /\ (eval_binop Sub v1 v2 = v1 - v2) /\
(eval_binop Mult v1 v2 = v1 * v2) /\ (eval_binop Mult v1 v2 = v1 * v2) /\
(eval_binop Div v1 v2 = v1 / v2)`;; (eval_binop Div v1 v2 = v1 / v2)`;;
(* (**
Define expressions parametric over some value type V. Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later. Will ease reasoning about different instantiations later.
*) Note that we differentiate between wether we use a variable from the environment or a parameter.
Parameters do not have error bounds in the invariants, so they must be perturbed, but variables from the
program will be perturbed upon binding, so we do not need to perturb them.
**)
let exp_IND, exp_REC = define_type let exp_IND, exp_REC = define_type
"exp = Var num "exp = Var num
|Param num |Param num
| Const V | Const V
| Binop binop exp exp";; | Binop binop exp exp";;
(* (**
Define the machine epsilon for floating point operations.
Current value: 2^(-53)
*)
let machineEpsilon = define `machineEpsilon:real = realFromNum 1 1 53`;;
(*
Define a perturbation function to ease writing of basic definitions Define a perturbation function to ease writing of basic definitions
*) **)
let perturb = define `(perturb:real->real->real) (r:real) (e:real) = r * ((&1) + e)`;; let perturb = define
(* `(perturb:real->real->real) (r:real) (e:real) = r * ((&1) + e)`;;
(**
Define expression evaluation relation parametric by an "error" delta. Define expression evaluation relation parametric by an "error" delta.
This value will be used later to express float computations using a perturbation This value will be used later to express float computations using a perturbation
of the real valued computation by (1 + d) of the real valued computation by (1 + d)
*) **)
let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
`(!eps env v. `(!eps env v.
eval_exp eps env (Var v) (env v)) /\ eval_exp eps env (Var v) (env v)) /\
...@@ -56,7 +56,7 @@ let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition ...@@ -56,7 +56,7 @@ let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
abs delta <= eps ==> abs delta <= eps ==>
eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) delta))`;; eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) delta))`;;
(* Inversion Lemmata, to do proofs similar to Coq proofs *) (** Inversion Lemmata, to do proofs similar to Coq proofs **)
let var_inv = let var_inv =
prove( prove(
`!eps env v val. `!eps env v val.
...@@ -145,19 +145,7 @@ let binop_inv = ...@@ -145,19 +145,7 @@ let binop_inv =
THEN EXISTS_TAC `d:real` THEN EXISTS_TAC `v1:real` THEN EXISTS_TAC `v2:real` THEN EXISTS_TAC `d:real` THEN EXISTS_TAC `v1:real` THEN EXISTS_TAC `v2:real`
THEN RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]]);; THEN RULE_ASSUM_TAC (REWRITE_RULE[injectivity "exp"]) THEN ASM_REWRITE_TAC[]]);;
let abs_leq_0_impl_zero = (** End inversion lemmata, next lemmata are also in Coq Dev. **)
prove (
`!d:real. abs d <= &0 ==> d = &0`,
INTRO_TAC "!d; abs_leq_0"
THEN SUBGOAL_TAC "abs_geq_0" `&0 <= abs d` [(REWRITE_TAC[REAL_ABS_POS])]
THEN SUBGOAL_TAC "abs_geq_leq_0" `abs d <= &0 /\ &0 <= abs d` [CONJ_TAC THEN (ASM_REWRITE_TAC[])]
THEN SUBGOAL_TAC "abs_eq_0" `abs d = &0` [ALL_TAC]
THEN MP_TAC (ASSUME `abs d <= &0 /\ &0 <= abs d`)
THEN ASM_REWRITE_TAC [SPECL [`abs d`; `&0:real`] REAL_LE_ANTISYM]
THEN MP_TAC (ASSUME `abs d = &0`)
THEN ASM_REWRITE_TAC [REAL_ABS_ZERO]);;
let perturb_0_val = let perturb_0_val =
prove ( prove (
`!(v:real) (delta:real). abs delta <= &0 ==> perturb v delta = v`, `!(v:real) (delta:real). abs delta <= &0 ==> perturb v delta = v`,
...@@ -167,123 +155,64 @@ let perturb_0_val = ...@@ -167,123 +155,64 @@ let perturb_0_val =
THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC);; THEN REAL_ARITH_TAC);;
g (`!e:(real)exp v1:real v2:real env. let eval_0_det =
eval_exp (&0) env e v1 /\ eval_exp (&0) env e v2 ==> v1 = v2`);;
e (MATCH_MP_TAC exp_IND THEN STRIP_TAC);;
(* Var Case *)
e (INTRO_TAC "!a v1 v2 env; eval_exps");;
e (destruct "eval_exps" "eval_v1 eval_v2");;
e (SUBGOAL_TAC "v1_eq_env_a" `v1:real = (env (a:num)):real`
[MATCH_MP_TAC var_inv THEN EXISTS_TAC `&0` THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "v2_eq_env_a" `v2:real = (env (a:num)):real`
[MATCH_MP_TAC var_inv THEN EXISTS_TAC `&0` THEN ASM_SIMP_TAC[]]);;
e (ASM_REWRITE_TAC[]);;
(* Param Case *)
e (STRIP_TAC);;
e (INTRO_TAC "!a v1 v2 env; eval_exps");;
e (destruct "eval_exps" "eval_v1 eval_v2");;
e (SUBGOAL_TAC "v1_eq_a" `?d. v1:real = perturb ((env (a:num)):real) d /\ abs d <= &0`
[MATCH_MP_TAC param_inv THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "v2_eq_a" `?d. v2:real = perturb ((env (a:num)):real) d /\ abs d <= &0`
[MATCH_MP_TAC param_inv THEN ASM_SIMP_TAC[]]);;
e (destruct "v1_eq_a" "@d1. v1_eq abs");;
e (destruct "v2_eq_a" "@d2. v2_eq abs2");;
e (USE_THEN "abs" (fun th -> ASM_REWRITE_TAC[MP (SPECL [`((env:num->real) a):real`; `d1:real`] perturb_0_val) th]));;
e (USE_THEN "abs2" (fun th -> ASM_REWRITE_TAC[MP (SPECL [`((env:num->real) a):real`; `d2:real`] perturb_0_val) th]));;
(* Const Case *)
e (STRIP_TAC);;
e (INTRO_TAC "!a v1 v2 env; eval_exps");;
e (destruct "eval_exps" "eval_v1 eval_v2");;
e (SUBGOAL_TAC "v1_eq_a" `?d. v1:real = perturb (a:real) d /\ abs d <= &0`
[MATCH_MP_TAC const_inv THEN EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "v2_eq_a" `?d. v2:real = perturb (a:real) d /\ abs d <= &0`
[MATCH_MP_TAC const_inv THEN EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]]);;
e (destruct "v1_eq_a" "@d1. v1_eq abs");;
e (destruct "v2_eq_a" "@d2. v2_eq abs2");;
e (SUBGOAL_TAC "abs_d1_0" `d1 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "abs_d2_0" `d2 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]);;
e (ASM_REWRITE_TAC[]);;
(* Binop Case *)
e (REPEAT STRIP_TAC);;
e (FIND_ASSUM (LABEL_TAC "IH1") `!(v1:real) (v2:real) (env:num->real).
eval_exp (&0) (env:num->real) (a1:(real)exp) (v1:real) /\
eval_exp (&0) (env:num->real) (a1:(real)exp) (v2:real)
==> (v1:real) = (v2:real)`);;
e (FIND_ASSUM (LABEL_TAC "IH2") `!(v1:real) (v2:real) (env:num->real).
eval_exp (&0) (env:num->real) (a2:(real)exp) (v1:real) /\
eval_exp (&0) (env:num->real) (a2:(real)exp) (v2:real)
==> (v1:real) = (v2:real)`);;
e (SUBGOAL_TAC "v1_eq_op_a" `?d v1' v2'. v1:real = perturb (eval_binop (a0:binop) (v1':real) (v2':real)) d /\ eval_exp (&0) env a1 v1' /\ eval_exp (&0) env a2 v2' /\ abs d <= &0`
[MATCH_MP_TAC binop_inv THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "v2_eq_op_a" `?d v1' v2'. v2:real = perturb (eval_binop (a0:binop) (v1':real) (v2':real)) d /\ eval_exp (&0) env a1 v1' /\ eval_exp (&0) env a2 v2' /\ abs d <= &0`
[MATCH_MP_TAC binop_inv THEN ASM_SIMP_TAC[]]);;
e (destruct "v1_eq_op_a" "@d1. @v11. @v21. v1_eq eval_a11 eval_a21 abs_0");;
e (destruct "v2_eq_op_a" "@d2. @v12. @v22. v2_eq eval_a12 eval_a22 abs_0");;
e (SUBGOAL_TAC "abs_d1_0" `d1 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "abs_d2_0" `d2 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]);;
e (SUBGOAL_TAC "v11_eq_v12" `v11:real = v12:real` [REMOVE_THEN "IH1" (MATCH_MP_TAC)]);;
e (EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]);;
e (SUBGOAL_TAC "v21_eq_v22" `v21:real = v22:real` [REMOVE_THEN "IH2" (MATCH_MP_TAC)]);;
e (EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]);;
e (ASM_REWRITE_TAC[]);;
let eval_0_det = top_thm();;
(* Alias for proof similarity *)
let Rsub_eq_Ropp_Rplus = real_sub;;
(** weird: cannot name lemma Rabs_err_simpl **)
let abs_err_simpl =
prove ( prove (
`!(a:real) (b:real). `!e:(real)exp v1:real v2:real env.
abs (a - (a * (&1 + b))) = abs (a * b)`, eval_exp (&0) env e v1 /\ eval_exp (&0) env e v2 ==> v1 = v2`,
intros "!a b" MATCH_MP_TAC exp_IND
THEN REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID] THEN split
THEN SUBGOAL_TAC "arith_simp" `(a:real) - ((a:real) + (a:real) * (b:real)) = -- (a * b)` [REAL_ARITH_TAC] THENL [
THEN REMOVE_THEN "arith_simp" (fun th -> REWRITE_TAC [th]) (* Var Case *)
THEN REWRITE_TAC [REAL_ABS_NEG]);; INTRO_TAC "!a v1 v2 env; eval_exps"
THEN destruct "eval_exps" "eval_v1 eval_v2"
(** THEN SUBGOAL_TAC "v1_eq_env_a" `v1:real = (env (a:num)):real`
TODO: Check wether we need Rabs (n * machineEpsilon) instead [MATCH_MP_TAC var_inv THEN EXISTS_TAC `&0` THEN ASM_SIMP_TAC[]]
**) THEN SUBGOAL_TAC "v2_eq_env_a" `v2:real = (env (a:num)):real`
[MATCH_MP_TAC var_inv THEN EXISTS_TAC `&0` THEN ASM_SIMP_TAC[]]
let const_abs_err_bounded = THEN ASM_REWRITE_TAC[];
prove ( split THENL [
`!(n:real) (nR:real) (nF:real) (cenv:num ->real). (* Param Case *)
eval_exp (&0) cenv (Const n) nR /\ INTRO_TAC "!a v1 v2 env; eval_exps"
eval_exp machineEpsilon cenv (Const n) nF ==> THEN destruct "eval_exps" "eval_v1 eval_v2"
abs (nR - nF) <= abs n * machineEpsilon`, THEN SUBGOAL_TAC "v1_eq_a" `?d. v1:real = perturb ((env (a:num)):real) d /\ abs d <= &0`
intros "!n nR nF cenv; eval_real eval_float" [MATCH_MP_TAC param_inv THEN ASM_SIMP_TAC[]]
THEN RULE_ASSUM_TAC (MATCH_MP const_inv) THEN SUBGOAL_TAC "v2_eq_a" `?d. v2:real = perturb ((env (a:num)):real) d /\ abs d <= &0`
THEN destruct "eval_real" "@d1. nR_eq abs_d1_0" [MATCH_MP_TAC param_inv THEN ASM_SIMP_TAC[]]
THEN destruct "eval_float" "@d2. nF_eq abs_d2_leq" THEN destruct "v1_eq_a" "@d1. v1_eq abs"
THEN ASM_SIMP_TAC [] THEN destruct "v2_eq_a" "@d2. v2_eq abs2"
THEN USE_THEN "abs_d1_0" THEN USE_THEN "abs" (fun th -> ASM_REWRITE_TAC[MP (SPECL [`((env:num->real) a):real`; `d1:real`] perturb_0_val) th])
(fun th -> THEN USE_THEN "abs2" (fun th -> ASM_REWRITE_TAC[MP (SPECL [`((env:num->real) a):real`; `d2:real`] perturb_0_val) th]);
ASM_REWRITE_TAC [MP (SPECL [`(n:real)`; `d1:real`] perturb_0_val) th]) (* Const Case *)
THEN REWRITE_TAC [perturb;abs_err_simpl; REAL_ABS_MUL] split THENL [
THEN MATCH_MP_TAC REAL_LE_LMUL INTRO_TAC "!a v1 v2 env; eval_exps"
THEN ASM_REWRITE_TAC [REAL_ABS_POS]);; THEN destruct "eval_exps" "eval_v1 eval_v2"
THEN SUBGOAL_TAC "v1_eq_a" `?d. v1:real = perturb (a:real) d /\ abs d <= &0`
[MATCH_MP_TAC const_inv THEN EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]]
THEN SUBGOAL_TAC "v2_eq_a" `?d. v2:real = perturb (a:real) d /\ abs d <= &0`
[MATCH_MP_TAC const_inv THEN EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[]]
THEN destruct "v1_eq_a" "@d1. v1_eq abs"
THEN destruct "v2_eq_a" "@d2. v2_eq abs2"
THEN SUBGOAL_TAC "abs_d1_0" `d1 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]
THEN SUBGOAL_TAC "abs_d2_0" `d2 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]
THEN ASM_REWRITE_TAC[];
(* Binop Case *)
intros "!a0 a1 a2; IH1 IH2;!v1 v2 env; eval_v1 eval_v2"
THEN SUBGOAL_TAC "v1_eq_op_a" `?d v1' v2'. v1:real = perturb (eval_binop (a0:binop) (v1':real) (v2':real)) d /\ eval_exp (&0) env a1 v1' /\ eval_exp (&0) env a2 v2' /\ abs d <= &0`
[MATCH_MP_TAC binop_inv THEN ASM_SIMP_TAC[]]
THEN SUBGOAL_TAC "v2_eq_op_a" `?d v1' v2'. v2:real = perturb (eval_binop (a0:binop) (v1':real) (v2':real)) d /\ eval_exp (&0) env a1 v1' /\ eval_exp (&0) env a2 v2' /\ abs d <= &0`
[MATCH_MP_TAC binop_inv THEN ASM_SIMP_TAC[]]
THEN destruct "v1_eq_op_a" "@d1. @v11. @v21. v1_eq eval_a11 eval_a21 abs_0"
THEN destruct "v2_eq_op_a" "@d2. @v12. @v22. v2_eq eval_a12 eval_a22 abs_0"
THEN SUBGOAL_TAC "abs_d1_0" `d1 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]
THEN SUBGOAL_TAC "abs_d2_0" `d2 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_SIMP_TAC[]]
THEN SUBGOAL_TAC "v11_eq_v12" `v11:real = v12:real` [REMOVE_THEN "IH1" (MATCH_MP_TAC)]
THENL[
EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[];
SUBGOAL_TAC "v21_eq_v22" `v21:real = v22:real` [REMOVE_THEN "IH2" (MATCH_MP_TAC)]
THENL[
EXISTS_TAC `env:num->real` THEN ASM_SIMP_TAC[];
ASM_REWRITE_TAC[]]]]]]);;
(**
TODO: Maybe improve bound by adding interval constraint and proving that it is leq than maxAbs of bounds
(nlo <= cenv n <= nhi)%R -> (Rabs (nR - nF) <= Rabs ((Rmax (Rabs nlo) (Rabs nhi)) * machineEpsilon))%R.
**)
let param_abs_err_bounded =
prove (
`!(n:num) (nR:real) (nF:real) (cenv:num->real).
eval_exp (&0) cenv (Param n) nR /\
eval_exp machineEpsilon cenv (Param n) nF ==>
(abs (nR - nF) <= abs (cenv n) * machineEpsilon)`,
intros "!n nR nF cenv; eval_real eval_float"
THEN RULE_ASSUM_TAC (MATCH_MP param_inv)
THEN destruct "eval_real" "@d1. nR_eq abs_d1_0"
THEN destruct "eval_float" "@d2. nF_eq abs_d1_leq"
THEN ASM_SIMP_TAC[]
THEN USE_THEN "abs_d1_0"
(fun th ->
ASM_REWRITE_TAC [MP (SPECL [`(cenv n:real)`; `d1:real`] perturb_0_val) th])
THEN REWRITE_TAC [perturb; abs_err_simpl; REAL_ABS_MUL]
THEN MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[REAL_ABS_POS]);;
(* (*
Using the parametric expressions, define boolean expressions for conditionals Using the parametric expressions, define boolean expressions for conditionals
*) *)
......
...@@ -23,3 +23,32 @@ let REAL_ABS_ERR_SIMPL = ...@@ -23,3 +23,32 @@ let REAL_ABS_ERR_SIMPL =
intros "!a b" intros "!a b"
THEN REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID; REAL_ADD_SUB2; REAL_ABS_NEG] THEN REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID; REAL_ADD_SUB2; REAL_ABS_NEG]
THEN auto);; THEN auto);;
let abs_leq_0_impl_zero =
prove (
`!d:real. abs d <= &0 ==> d = &0`,
INTRO_TAC "!d; abs_leq_0"
THEN SUBGOAL_TAC "abs_geq_0" `&0 <= abs d` [(REWRITE_TAC[REAL_ABS_POS])]
THEN SUBGOAL_TAC "abs_geq_leq_0" `abs d <= &0 /\ &0 <= abs d` [CONJ_TAC THEN (ASM_REWRITE_TAC[])]
THEN SUBGOAL_TAC "abs_eq_0" `abs d = &0` [ALL_TAC]
THEN MP_TAC (ASSUME `abs d <= &0 /\ &0 <= abs d`)
THEN ASM_REWRITE_TAC [SPECL [`abs d`; `&0:real`] REAL_LE_ANTISYM]
THEN MP_TAC (ASSUME `abs d = &0`)
THEN ASM_REWRITE_TAC [REAL_ABS_ZERO]);;
(** weird: cannot name lemma Rabs_err_simpl **)
let abs_err_simpl =
prove (
`!(a:real) (b:real).
abs (a - (a * (&1 + b))) = abs (a * b)`,
intros "!a b"
THEN REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID]
THEN SUBGOAL_TAC "arith_simp" `(a:real) - ((a:real) + (a:real) * (b:real)) = -- (a * b)` [REAL_ARITH_TAC]
THEN REMOVE_THEN "arith_simp" (fun th -> REWRITE_TAC [th])
THEN REWRITE_TAC [REAL_ABS_NEG]);;
(*
Define the machine epsilon for floating point operations.
Current value: 2^(-53)
*)
let machineEpsilon = define `machineEpsilon:real = &1 /((&2) pow 53)`;;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment