Skip to content
Snippets Groups Projects
Commit 903bfabb authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove expression lemmata necessary for final result

parent 549d141a
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 122 additions and 39 deletions
hol/Expressions.hl
+ 122
− 39
View file @ 903bfabb
......@@ -2,7 +2,7 @@
Formalization of the base expression language for the daisy framework
*)
needs "Infra/tactics.hl";;
(* needs "/home/heiko/Git_Repos/hol-light/IEEE/make.ml";; *)
needs "Infra/RealConstruction.hl";;
(*
Expressions will use binary operators.
Define them first
......@@ -22,20 +22,20 @@ let eval_binop = new_recursive_definition binop_REC
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
*)
let exp_IND, exp_REC= define_type
let exp_IND, exp_REC = define_type
"exp = Var num
|Param num
| Const V
| Binop binop exp exp";;
(*
Define the machine epsilon for floating point operations.
FIXME: Currently set to 1.0 instead of the concrete value!
Current value: 2^(-53)
*)
let m_eps = define `m_eps:real = (&1)`;;
let machineEpsilon = define `machineEpsilon:real = realFromNum 1 1 53`;;
(*
Define a perturbation function to ease writing of basic definitions
*)
let perturb = define `(perturb:real->real->real) = \r e. r * ((&1) + e)`;;
new_type_abbrev ("env_ty",`:num->real`);;
let perturb = define `(perturb:real->real->real) (r:real) (e:real) = r * ((&1) + e)`;;
(*
Define expression evaluation relation parametric by an "error" delta.
This value will be used later to express float computations using a perturbation
......@@ -44,6 +44,9 @@ new_type_abbrev ("env_ty",`:num->real`);;
let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
`(!eps env v.
eval_exp eps env (Var v) (env v)) /\
(!eps env v delta.
abs delta <= eps ==>
eval_exp eps env (Param v) (perturb (env v) delta)) /\
(!eps env n delta.
abs delta <= eps ==>
eval_exp eps env (Const n) (perturb n delta)) /\
......@@ -53,6 +56,7 @@ let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
abs delta <= eps ==>
eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) delta))`;;
(* Inversion Lemmata, to do proofs similar to Coq proofs *)
let var_inv =
prove(
`!eps env v val.
......@@ -60,20 +64,16 @@ let var_inv =
ONCE_REWRITE_TAC
[eval_exp_CASES] THEN
INTRO_TAC "!eps env v val; cases_exp" THEN
REMOVE_THEN "cases_exp" (DESTRUCT_TAC "varc | constc | binopc") THENL
[REMOVE_THEN "varc" (DESTRUCT_TAC "@v2. var_eq val_eq") THEN
RULE_ASSUM_TAC (REWRITE_RULE [injectivity "exp"]) THEN ASM_REWRITE_TAC [];
REMOVE_THEN "constc" (DESTRUCT_TAC "@n. @d. var_eq _ _") THEN
SUBGOAL_TAC "" `F`
[MP_TAC (ASSUME `Var (v:num) = Const (n:real)`) THEN
ASM_REWRITE_TAC [distinctness "exp"]];
REMOVE_THEN "cases_exp" (DESTRUCT_TAC "varc | paramc | constc | binopc")
THENL [
REMOVE_THEN "varc" (DESTRUCT_TAC "@v2. var_eq val_eq") THEN
RULE_ASSUM_TAC (REWRITE_RULE [injectivity "exp"]) THEN ASM_REWRITE_TAC [];
REMOVE_THEN "paramc" (DESTRUCT_TAC "@n. @d. var_eq _ _") THEN lcontra "var_eq" "exp";
REMOVE_THEN "constc" (DESTRUCT_TAC "@n. @d. var_eq _ _") THEN
lcontra "var_eq" "exp";
REMOVE_THEN "binopc"
(DESTRUCT_TAC "@b. @e1. @e2. @v1. @v2. @d. var_eq _ _ _ _") THEN
SUBGOAL_TAC "" `F`
[MP_TAC
(ASSUME
`Var (v:num) = Binop (b:binop) (e1:(real)exp) (e2:(real)exp)`) THEN
ASM_REWRITE_TAC [distinctness "exp"]]] THEN
lcontra "var_eq" "exp"] THEN
FIRST_ASSUM CONTR_TAC);;
let var_equiv =
......@@ -89,6 +89,24 @@ let var_equiv =
intros "val_eq"
THEN ASM_REWRITE_TAC[eval_exp_RULES]]);;
let param_inv =
prove
(`!eps env n v.
eval_exp eps env (Param n) v ==> ?d. v = perturb (env n) d /\ abs d <= eps`,
ONCE_REWRITE_TAC
[eval_exp_CASES] THEN
INTRO_TAC "!eps env n v; cases_exp" THEN
REMOVE_THEN "cases_exp" (DESTRUCT_TAC "varc | paramc | constc | binopc") THENL
[REMOVE_THEN "varc" (DESTRUCT_TAC "@v. const_eq _") THEN
lcontra "const_eq" "exp";
REMOVE_THEN "paramc" (DESTRUCT_TAC "@n2. @d. c_eq v_eq abs_less") THEN
EXISTS_TAC `d:real` THEN
RULE_ASSUM_TAC (REWRITE_RULE [injectivity "exp"]) THEN ASM_REWRITE_TAC [];
REMOVE_THEN "constc" (DESTRUCT_TAC "@n. @d. var_eq _ _") THEN lcontra "var_eq" "exp";
REMOVE_THEN "binopc"
(DESTRUCT_TAC "@b. @e1. @e2. @v1. @v2. @d. const_eq _ _ _ _") THEN
lcontra "const_eq" "exp"]);;
let const_inv =
prove
(`!eps env n v.
......@@ -96,23 +114,16 @@ let const_inv =
ONCE_REWRITE_TAC
[eval_exp_CASES] THEN
INTRO_TAC "!eps env n v; cases_exp" THEN
REMOVE_THEN "cases_exp" (DESTRUCT_TAC "varc | constc | binopc") THENL
REMOVE_THEN "cases_exp" (DESTRUCT_TAC "varc | paramc | constc | binopc") THENL
[REMOVE_THEN "varc" (DESTRUCT_TAC "@v. const_eq _") THEN
REMOVE_THEN "const_eq"
(fun th ->
SUBGOAL_TAC "" `F`
[MP_TAC th THEN ASM_REWRITE_TAC [distinctness "exp"]] THEN
FIRST_ASSUM CONTR_TAC);
lcontra "const_eq" "exp";
REMOVE_THEN "paramc" (DESTRUCT_TAC "@n. @d. var_eq _ _") THEN lcontra "var_eq" "exp";
REMOVE_THEN "constc" (DESTRUCT_TAC "@n2. @d. c_eq v_eq abs_less") THEN
EXISTS_TAC `d:real` THEN
RULE_ASSUM_TAC (REWRITE_RULE [injectivity "exp"]) THEN ASM_REWRITE_TAC [];
REMOVE_THEN "binopc"
(DESTRUCT_TAC "@b. @e1. @e2. @v1. @v2. @d. const_eq _ _ _ _") THEN
REMOVE_THEN "const_eq"
(fun th ->
SUBGOAL_TAC "" `F`
[MP_TAC th THEN ASM_REWRITE_TAC [distinctness "exp"]] THEN
FIRST_ASSUM CONTR_TAC)]);;
lcontra "const_eq" "exp"]);;
let binop_inv =
prove
......@@ -125,18 +136,14 @@ let binop_inv =
abs d <= eps`,
INTRO_TAC "!eps env b e1 e2 v; cases_exp"
THEN RULE_ASSUM_TAC (ONCE_REWRITE_RULE[eval_exp_CASES])
THEN destruct "cases_exp" "varc | constc | binopc "
THEN destruct "cases_exp" "varc | paramc | constc | binopc "
THENL [
destruct "varc" "@v. b_eq _" THEN lcontradiction "b_eq" "exp";
destruct "constc" "@n. @d. b_eq _ _" THEN lcontradiction "b_eq" "exp";
destruct "varc" "@v. b_eq _" THEN lcontra "b_eq" "exp";
destruct "paramc" "@n. @d. b_eq _ _" THEN lcontra "b_eq" "exp";
destruct "constc" "@n. @d. b_eq _ _" THEN lcontra "b_eq" "exp";
destruct "binopc" "@b2. @e1'. @e2'. @v1. @v2. @d. b_eq v_eq eval_e1 eval_e2 abs_delta"
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[]]);;
(*
Define real evaluation as a predicate on the epsilon of the evaluation relation
*)
let is_real_value = define
`is_real_value (e:(real)exp) (env:env_ty) (v:real) = eval_exp (&0) env e v`;;
let abs_leq_0_impl_zero =
prove (
......@@ -151,10 +158,18 @@ let abs_leq_0_impl_zero =
THEN ASM_REWRITE_TAC [REAL_ABS_ZERO]);;
let perturb_0_val =
prove (
`!(v:real) (delta:real). abs delta <= &0 ==> perturb v delta = v`,
intros "!v delta; abs_leq_0"
THEN SIMP_TAC[perturb]
THEN RULE_ASSUM_TAC (MATCH_MP abs_leq_0_impl_zero)
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC);;
g (`!e:(real)exp v1:real v2:real env.
eval_exp (&0) env e v1 /\ eval_exp (&0) env e v2 ==> v1 = v2`);;
e (MATCH_MP_TAC exp_IND);;
e (STRIP_TAC);;
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");;
......@@ -163,6 +178,18 @@ e (SUBGOAL_TAC "v1_eq_env_a" `v1:real = (env (a:num)):real`
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");;
......@@ -201,6 +228,62 @@ 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 (
`!(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]);;
(**
TODO: Check wether we need Rabs (n * machineEpsilon) instead
**)
let const_abs_err_bounded =
prove (
`!(n:real) (nR:real) (nF:real) (cenv:num ->real).
eval_exp (&0) cenv (Const n) nR /\
eval_exp machineEpsilon cenv (Const n) nF ==>
abs (nR - nF) <= abs n * machineEpsilon`,
intros "!n nR nF cenv; eval_real eval_float"
THEN RULE_ASSUM_TAC (MATCH_MP const_inv)
THEN destruct "eval_real" "@d1. nR_eq abs_d1_0"
THEN destruct "eval_float" "@d2. nF_eq abs_d2_leq"
THEN ASM_SIMP_TAC []
THEN USE_THEN "abs_d1_0"
(fun th ->
ASM_REWRITE_TAC [MP (SPECL [`(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]);;
(**
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
*)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment