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

Make expression evaluation parametric by some perturbation function, as discussed this morning

parent e5d57657
(*
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
*)
needs "Infra/tactics.hl";;
needs "/home/heiko/Git_Repos/hol-light/IEEE/make.ml";;
(*
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
*)
let exp_INDUCT, exp_REC= define_type
"exp = Var num
| Const V
| Plus exp exp
| Sub exp exp
| Mult exp exp
| Div exp exp";;
(*
Since we want to stay with real values for the moment,
show that real valued expressions can be evaluated
by constructing the corresponding function
*)
let eval_real_EXISTS = prove_general_recursive_function_exists
`?eval_real.
(!x (E:num->real). eval_real (Var x) E = E x) /\
(!(v:real) E. eval_real (Const v) E = v) /\
(!e1 e2 E. eval_real (Plus e1 e2) E = (eval_real e1) E + (eval_real e2) E) /\
(!e1 e2 E. eval_real (Sub e1 e2) E = (eval_real e1) E - (eval_real e2) E) /\
(!e1 e2 E. eval_real (Mult e1 e2) E = (eval_real e1) E * (eval_real e2) E) /\
(!e1 e2 E. eval_real (Div e1 e2) E = (eval_real e1) E / (eval_real e2) E)`;;
(*
Since HOL Light could prove the existence of the evaluation function,
we can define it using the defining equations from the theorem.
*)
let eval_real_DEF = new_specification ["eval_real"] eval_real_EXISTS;;
(*
Toy examples showing how to evaluate terms and functions in HOL Light
let test = `exp_eval (Const (&1)) (\x. &1)`;;
let test = REWRITE_CONV[exp_eval_DEF] test;;
rhs (concl test);;
*)
(*
Prove totality of expression evaluation for reals assuming totality of the environment
TODO: Make totality totality on occuring variables
*)
let eval_real_total =
prove (
`!(e:(real)exp) (s:num->real).
(!x:num. ?v:real. s x = v) ==>
?v. exp_eval e s = v`,
MATCH_MP_TAC exp_INDUCT THEN REPEAT STRIP_TAC THEN MESON_TAC[]);;
(*
More formal proof, to get feeling about tactics.
TODO: Time consumption compared?
g `!e (s:num->real). (!x:num. ?v:real. s x = v) ==> ?v. exp_eval e s = v`;;
e (MATCH_MP_TAC exp_INDUCT THEN REPEAT STRIP_TAC);;
e (SPECIALIZE `a:num` `!(x:num). ?(v:real). (s:num->real) x = v`);;
e (SPECIALIZE `a:num` `!(x:num). ?(v:real). (s:num->real) x = v`);;
e (DESTRUCT_TAC "@v. v_def" (ASSUME `?(v:real). (s:num->real) a = v`));;
e (EXISTS_TAC `v:real`);;
e (ASM_REWRITE_TAC[exp_eval_SIMPS]);;
e (EXISTS_TAC `a:real`);;
e (REWRITE_TAC [exp_eval_SIMPS]);;
e (SPECIALIZE `s:num->real` `!s. (!x. ?v. s x = v) ==> (?v. exp_eval a0 s = v)`);;
e (SUBGOAL_TAC "val_def_a0" `?v. exp_eval a0 s = v` [ALL_TAC]);;
e (MATCH_MP_TAC (ASSUME `(!x. ?v. s x = v) ==> (?v. exp_eval a0 s = v)`) THEN ASM_REWRITE_TAC[]);;
e (SPECIALIZE `s:num->real` `!s. (!x. ?v. s x = v) ==> (?v. exp_eval a1 s = v)`);;
e (SUBGOAL_TAC "val_def_a1" `?v. exp_eval a1 s = v` [ALL_TAC]);;
e (MATCH_MP_TAC (ASSUME `(!x. ?v. s x = v) ==> (?v. exp_eval a1 s = v)`) THEN ASM_REWRITE_TAC[]);;
e (DESTRUCT_TAC "@v1. v1_def" (ASSUME `?v. exp_eval a0 s = v`));;
e (DESTRUCT_TAC "@v2. v2_def" (ASSUME `?v. exp_eval a1 s = v`));;
e (EXISTS_TAC `(v1:real) + (v2:real)` THEN ASM_REWRITE_TAC[exp_eval_SIMPS]);;
e (MESON_TAC[]);;
e (MESON_TAC[]);;
e (MESON_TAC[]);;
let exp_eval_total = top_thm();; *)
(*
Next define a "float" type that we can use to plug in to the framework
We need to make a basic type definition because we want to approximate the reals by these floats and enforce a correlation between the parameters
*)
promote_all_values();;
let p2_valid = prove
(`is_valid_flformat (2,2)`,
ASM_REWRITE_TAC [is_valid_flformat] THEN REPEAT STRIP_TAC THEN ARITH_TAC);;
g `?(fmt:flformat) (x:real). is_float fmt x`;;
e (ASM_REWRITE_TAC[is_float;is_frac_and_exp;flr;flp]);;
e (EXISTS_TAC `mk_flformat(2,2)`);;
e (EXISTS_TAC `&1`);;
e (EXISTS_TAC `1`);;
e (EXISTS_TAC `&1:int`);;
e (STRIP_TAC THEN TRY (ARITH_TAC));;
e (DESTRUCT_TAC "rw_sound valid_rw" flformat_typbij);;
e (SUBGOAL_TAC "mk_dest_22"
`dest_flformat(mk_flformat (2,2)) = (2,2)`
[(ASM_MESON_TAC[p2_valid])]);;
e (ASM_REWRITE_TAC[ASSUME `dest_flformat (mk_flformat (2,2)) = 2,2`]);;
e (STRIP_TAC THEN TRY (ARITH_TAC));;
e (ASM_REWRITE_TAC[REAL_ABS_1;ipow; (INT_REDUCE_CONV `(&1):int - &2 + &1`)]);;
e (REWRITE_TAC [(INT_REDUCE_CONV `(if &0:int <= &0:int
then &2:real pow num_of_int (&0)
else inv (&2:real pow num_of_int (-- &0)))`)]);;
e (SUBGOAL_TAC "pow_0_eq_1" `&2:real pow num_of_int (&0) = &1:real` [ASM_REWRITE_TAC[NUM_OF_INT_OF_NUM;real_pow]]);;
e (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let exists_float_type_pred =
prove
(`?(fmt:flformat) (x:real). is_float fmt x`,
let lemma1 = prove
(`is_valid_flformat (2,2)`,
ASM_REWRITE_TAC [is_valid_flformat] THEN REPEAT STRIP_TAC THEN
ARITH_TAC)
in
ASM_REWRITE_TAC [is_float; is_frac_and_exp; flr; flp] THEN
EXISTS_TAC `mk_flformat(2,2)` THEN
EXISTS_TAC `&1` THEN
EXISTS_TAC `1` THEN
EXISTS_TAC `&1:int` THEN
STRIP_TAC THENL [ARITH_TAC; ALL_TAC] THEN
DESTRUCT_TAC "rw_sound valid_rw" flformat_typbij THEN
SUBGOAL_TAC "mk_dest_22" `dest_flformat (mk_flformat (2,2)) = 2,2`
[ASM_MESON_TAC [lemma1]] THEN
ASM_REWRITE_TAC [ASSUME `dest_flformat (mk_flformat (2,2)) = 2,2`] THEN
STRIP_TAC THENL [ARITH_TAC; ALL_TAC] THEN
ASM_REWRITE_TAC [REAL_ABS_1; ipow; INT_REDUCE_CONV `(&1):int - &2 + &1`] THEN
REWRITE_TAC
[INT_REDUCE_CONV
`(if &0:int <= &0:int
then &2:real pow num_of_int (&0)
else inv (&2:real pow num_of_int (-- &0)))`] THEN
SUBGOAL_TAC "pow_0_eq_1" `&2:real pow num_of_int (&0) = &1:real`
[ASM_REWRITE_TAC [NUM_OF_INT_OF_NUM; real_pow]] THEN
ASM_REWRITE_TAC [] THEN REAL_ARITH_TAC);;
(*
For the moment, floats are simply axiomatized reals!
FIXME!!
*)
new_type_abbrev ("float",`:real`);;
let m_eps = define `m_eps:real = (&1)`;; (* TODO *)
let get_float = define
`get_float (x:real) = ?xf:real d:real. abs (d) <= m_eps /\ xf = x * (&1 + d)`;;
let eval_float_SIMPS =define
`(!x E:num->real. eval_float (Var x) E <=> get_float (E x)) /\
(!v:real E:num->real. eval_float (Const v) E <=> get_float v) /\
(!e1 e2 E. eval_float (Plus e1 e2) E <=>
((eval_float e1 E <=> v1) /\ (eval_float e2 E <=> v2) ==>
get_float (v1 + v2)))`;;
/\
(!e1 e2 E. eval_float (Sub e1 e2) E <=> get_float (eval_float E e1 - eval_float E e2)) /\
(!e1 e2 E. eval_float (Mult e1 e2) E <=> get_float (eval_float E e1 * eval_float E e2)) /\
(!e1 e2 E. eval_float (Div e1 e2) E <=> get_float (eval_float E e1 / eval_float E e2))`;;
needs "exps.hl";;
(*
Using the parametric expressions, define boolean expressions for conditionals
*)
......
(*
Formalization of the base expression language for the daisy framework
*)
needs "Infra/tactics.hl";;
(* needs "/home/heiko/Git_Repos/hol-light/IEEE/make.ml";; *)
(*
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
*)
let exp_INDUCT, exp_REC= define_type
"exp = Var num
| Const V
| Plus exp exp
| Sub exp exp
| Mult exp exp
| Div exp exp";;
(*
Define the machine epsilon for floating point operations.
FIXME: Currently set to 1.0 instead of the concrete value!
*)
let m_eps = define `m_eps:real = (&1)`;;
(*
Define a perturbation function to ease writing of basic definitions
*)
let perturb_def = define `(perturb:real->real->real) = \r e. e * ((&1) + e)`;;
(*
Define expression evaluation parametric by an "error function".
This function will be used later to express float computations using a perturbation
of the real valued computation by (1 + d)
Additionally we need an "error id" function which uniquely numbers an expression.
*)
let eval_err = new_recursive_definition exp_REC
`(eval_err (Var name) err_fun err_id_fun env
= perturb (env name) (err_fun (err_id_fun (Var name)))) /\
(eval_err (Const v) err_fun err_id_fun env
= perturb v (err_fun (err_id_fun (Const v)))) /\
(eval_err (Plus e1 e2) err_fun err_id_fun env
= perturb (
(eval_err e1 err_fun err_id_fun env) + (eval_err e2 err_fun err_id_fun env))
(err_fun (err_id_fun (Plus e1 e2)))) /\
(eval_err (Sub e1 e2) err_fun err_id_fun env
= perturb (
(eval_err e1 err_fun err_id_fun env) - (eval_err e2 err_fun err_id_fun env))
(err_fun (err_id_fun (Sub e1 e2)))) /\
(eval_err (Mult e1 e2)err_fun err_id_fun env
= perturb (
(eval_err e1 err_fun err_id_fun env) * (eval_err e2 err_fun err_id_fun env))
(err_fun (err_id_fun (Mult e1 e2)))) /\
(eval_err (Div e1 e2) err_fun err_id_fun env
= perturb (
(eval_err e1 err_fun err_id_fun env) / (eval_err e2 err_fun err_id_fun env))
(err_fun (err_id_fun (Div e1 e2))))`;;
(*
Define real evaluation as stated above:
*)
let eval_real = define
`eval_real (e:(real)exp) (env:num->real) = eval_err e (\x. &0) (\x. &0)`;;
(*
float evaluation is non-deterministic, since the perturbation is existencially quantified
--> state as predicate when float evaluation using errors is valid, related to errors
*)
let is_valid_err_float = define
`is_valid_err_float (err_fun:num->real) <=>
!id. ?n.
(&n = err_fun id \/ --(&n) = err_fun id) /\
abs (&n) <= m_eps`;;
(*
Prove totality of expression evaluation for reals assuming totality of the environment
TODO: Make totality totality on occuring variables
*)
let eval_real_total =
prove (
`!(e:(real)exp) (s:num->real).
(!x:num. ?v:real. s x = v) ==>
?v. exp_eval e s = v`,
MATCH_MP_TAC exp_INDUCT THEN REPEAT STRIP_TAC THEN MESON_TAC[]);;
(*
More formal proof, to get feeling about tactics.
TODO: Time consumption compared?
g `!e (s:num->real). (!x:num. ?v:real. s x = v) ==> ?v. exp_eval e s = v`;;
e (MATCH_MP_TAC exp_INDUCT THEN REPEAT STRIP_TAC);;
e (SPECIALIZE `a:num` `!(x:num). ?(v:real). (s:num->real) x = v`);;
e (SPECIALIZE `a:num` `!(x:num). ?(v:real). (s:num->real) x = v`);;
e (DESTRUCT_TAC "@v. v_def" (ASSUME `?(v:real). (s:num->real) a = v`));;
e (EXISTS_TAC `v:real`);;
e (ASM_REWRITE_TAC[exp_eval_SIMPS]);;
e (EXISTS_TAC `a:real`);;
e (REWRITE_TAC [exp_eval_SIMPS]);;
e (SPECIALIZE `s:num->real` `!s. (!x. ?v. s x = v) ==> (?v. exp_eval a0 s = v)`);;
e (SUBGOAL_TAC "val_def_a0" `?v. exp_eval a0 s = v` [ALL_TAC]);;
e (MATCH_MP_TAC (ASSUME `(!x. ?v. s x = v) ==> (?v. exp_eval a0 s = v)`) THEN ASM_REWRITE_TAC[]);;
e (SPECIALIZE `s:num->real` `!s. (!x. ?v. s x = v) ==> (?v. exp_eval a1 s = v)`);;
e (SUBGOAL_TAC "val_def_a1" `?v. exp_eval a1 s = v` [ALL_TAC]);;
e (MATCH_MP_TAC (ASSUME `(!x. ?v. s x = v) ==> (?v. exp_eval a1 s = v)`) THEN ASM_REWRITE_TAC[]);;
e (DESTRUCT_TAC "@v1. v1_def" (ASSUME `?v. exp_eval a0 s = v`));;
e (DESTRUCT_TAC "@v2. v2_def" (ASSUME `?v. exp_eval a1 s = v`));;
e (EXISTS_TAC `(v1:real) + (v2:real)` THEN ASM_REWRITE_TAC[exp_eval_SIMPS]);;
e (MESON_TAC[]);;
e (MESON_TAC[]);;
e (MESON_TAC[]);;
let exp_eval_total = top_thm();; *)
(*
Next define a "float" type that we can use to plug in to the framework
We need to make a basic type definition because we want to approximate the reals by these floats and enforce a correlation between the parameters
*)
let p2_valid = prove
(`is_valid_flformat (2,2)`,
ASM_REWRITE_TAC [is_valid_flformat] THEN REPEAT STRIP_TAC THEN ARITH_TAC);;
g `?(fmt:flformat) (x:real). is_float fmt x`;;
e (ASM_REWRITE_TAC[is_float;is_frac_and_exp;flr;flp]);;
e (EXISTS_TAC `mk_flformat(2,2)`);;
e (EXISTS_TAC `&1`);;
e (EXISTS_TAC `1`);;
e (EXISTS_TAC `&1:int`);;
e (STRIP_TAC THEN TRY (ARITH_TAC));;
e (DESTRUCT_TAC "rw_sound valid_rw" flformat_typbij);;
e (SUBGOAL_TAC "mk_dest_22"
`dest_flformat(mk_flformat (2,2)) = (2,2)`
[(ASM_MESON_TAC[p2_valid])]);;
e (ASM_REWRITE_TAC[ASSUME `dest_flformat (mk_flformat (2,2)) = 2,2`]);;
e (STRIP_TAC THEN TRY (ARITH_TAC));;
e (ASM_REWRITE_TAC[REAL_ABS_1;ipow; (INT_REDUCE_CONV `(&1):int - &2 + &1`)]);;
e (REWRITE_TAC [(INT_REDUCE_CONV `(if &0:int <= &0:int
then &2:real pow num_of_int (&0)
else inv (&2:real pow num_of_int (-- &0)))`)]);;
e (SUBGOAL_TAC "pow_0_eq_1" `&2:real pow num_of_int (&0) = &1:real` [ASM_REWRITE_TAC[NUM_OF_INT_OF_NUM;real_pow]]);;
e (ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let exists_float_type_pred =
prove
(`?(fmt:flformat) (x:real). is_float fmt x`,
let lemma1 = prove
(`is_valid_flformat (2,2)`,
ASM_REWRITE_TAC [is_valid_flformat] THEN REPEAT STRIP_TAC THEN
ARITH_TAC)
in
ASM_REWRITE_TAC [is_float; is_frac_and_exp; flr; flp] THEN
EXISTS_TAC `mk_flformat(2,2)` THEN
EXISTS_TAC `&1` THEN
EXISTS_TAC `1` THEN
EXISTS_TAC `&1:int` THEN
STRIP_TAC THENL [ARITH_TAC; ALL_TAC] THEN
DESTRUCT_TAC "rw_sound valid_rw" flformat_typbij THEN
SUBGOAL_TAC "mk_dest_22" `dest_flformat (mk_flformat (2,2)) = 2,2`
[ASM_MESON_TAC [lemma1]] THEN
ASM_REWRITE_TAC [ASSUME `dest_flformat (mk_flformat (2,2)) = 2,2`] THEN
STRIP_TAC THENL [ARITH_TAC; ALL_TAC] THEN
ASM_REWRITE_TAC [REAL_ABS_1; ipow; INT_REDUCE_CONV `(&1):int - &2 + &1`] THEN
REWRITE_TAC
[INT_REDUCE_CONV
`(if &0:int <= &0:int
then &2:real pow num_of_int (&0)
else inv (&2:real pow num_of_int (-- &0)))`] THEN
SUBGOAL_TAC "pow_0_eq_1" `&2:real pow num_of_int (&0) = &1:real`
[ASM_REWRITE_TAC [NUM_OF_INT_OF_NUM; real_pow]] THEN
ASM_REWRITE_TAC [] THEN REAL_ARITH_TAC);;
(*
For the moment, floats are simply axiomatized reals!
FIXME!!
*)
new_type_abbrev ("float",`:real`);;
let is_abs_float = define
`is_abs_float (x:real) <=> ?xf:real d:real. abs (d) <= m_eps /\ xf = x * (&1 + d)`;;
let eval_float_RULES, eval_float_INDUCT, eval_float_CASES = new_inductive_definition
`(!x (E:num->real).
is_abs_float (E x) ==>
eval_float (Var x) E (E x)) /\
(!v:real E:num->real.
is_abs_float v ==>
eval_float (Const v) E v) /\
(!e1 e2 E. eval_float e1 E v1 /\ eval_float e2 E v2 ==> is_abs_float
eval_float (Plus e1 e2) E <=>
((eval_float e1 E <=> v1) /\ (eval_float e2 E <=> v2) ==>
get_float (v1 + v2)))`;;
/\
(!e1 e2 E. eval_float (Sub e1 e2) E <=> get_float (eval_float E e1 - eval_float E e2)) /\
(!e1 e2 E. eval_float (Mult e1 e2) E <=> get_float (eval_float E e1 * eval_float E e2)) /\
(!e1 e2 E. eval_float (Div e1 e2) E <=> get_float (eval_float E e1 / eval_float E e2))`;;
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