diff --git a/coq/Expressions.v b/coq/Expressions.v index 6df158dfbf45c1e298ce8df6de9cfb22b7aa9c46..3127df9ae3a776e3bec2cdc87d3169dafa06f207 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -45,7 +45,7 @@ Definition unopEqBool (o1:unop) (o2:unop) := (** Define evaluation for unary operators on reals. - Errors are added on the expression evaluation level later. + Errors are added in the expression evaluation level later. **) Definition evalUnop (o:unop) (v:R):= match o with @@ -104,7 +104,7 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) := Define a perturbation function to ease writing of basic definitions **) Definition perturb (r:R) (e:R) := - Rmult r (Rplus 1 e). + (r * (1 + e))%R. (** Define expression evaluation relation parametric by an "error" epsilon. diff --git a/coq/Infra/Abbrevs.v b/coq/Infra/Abbrevs.v index dc2a58eb2cf642a811df5b092bb921aa647b7124..0955bf794a527a5bcfd8c253f4bb001e26677d39 100644 --- a/coq/Infra/Abbrevs.v +++ b/coq/Infra/Abbrevs.v @@ -55,17 +55,3 @@ Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :R := if y =? x then v else E y. - -(** -In the final proof we will assume that the given environment under which the -expression is executed agrees with the precondition. -Define this as meaning that for a given variable, the environments value must be -contained in the preconditions interval for it. -This definition suffices since Daisys expressions are immutable, hence no -variable can be written twice. -This means that a free variable will never be defined in the program text -**) -Definition precondValidForExec (P:nat->intv) (cenv:env) := - forall v:nat, - let (ivlo,ivhi) := P v in - (Q2R ivlo <= cenv v <= Q2R ivhi)%R. \ No newline at end of file diff --git a/hol4/abbrevsScript.sml b/hol4/abbrevsScript.sml new file mode 100644 index 0000000000000000000000000000000000000000..4e971bd118b2c9efacb45b3a42c846b6b69dabe7 --- /dev/null +++ b/hol4/abbrevsScript.sml @@ -0,0 +1,35 @@ +open preamble +open realTheory realLib + +val _ = new_theory "abbrevs"; +(** +For the moment we need only one interval type in HOL, since we do not have the +problem of computability as we have it in Coq +**) +val _ = type_abbrev("interval", ``:real#real``); +val IVlo_def = Define `IVlo (iv:interval) = FST iv`; +val IVhi_def = Define `IVhi (iv:interval) = SND iv`; + +val iv_ss = [IVlo_def,IVhi_def]; + +val _ = type_abbrev("ann", ``:interval#real``); + +(** +Later we will argue about program preconditions. +Define a precondition to be a function mapping numbers (resp. variables) to intervals. +**) +val _ = type_abbrev ("precond", ``:num->interval``); + +(** + Abbreviations for the environment types +**) +val _ = type_abbrev("env",``:num->real``); + +(** + Define environment update function as abbreviation. +**) +val updEnv_def = Define ` +updEnv (x:num) (v:real) (E:env) (y:num) :real = if y = x then v else E y`; + + +val - = export_theory(); diff --git a/hol4/expressionsScript.sml b/hol4/expressionsScript.sml index c8ee6aa4fd04e0d18a71ede7fb6d7a250169405c..9637d426ee0e5cbabb05c2fce805fa7ed014d526 100644 --- a/hol4/expressionsScript.sml +++ b/hol4/expressionsScript.sml @@ -1,5 +1,6 @@ open preamble open realTheory realLib +open abbrevsTheory val _ = ParseExtras.temp_tight_equality() val _ = new_theory "expressions"; @@ -9,18 +10,32 @@ val _ = new_theory "expressions"; Define them first **) val _ = Datatype ` - binop = Plus | Sub | Mult | Div` +binop = Plus | Sub | Mult | Div`; (** Next define an evaluation function for binary operators. Errors are added on the expression evaluation level later *) -val eval_binop_def = Define ` - eval_binop Plus v1 v2 = v1 + v2 /\ - eval_binop Sub v1 v2 = v1 - v2 /\ - eval_binop Mult v1 v2 = v1 * v2 /\ - eval_binop Div v1 v2 = v1 / (v2:real) `; +val evalBinop_def = Define ` +evalBinop Plus v1 v2 = v1 + v2 /\ +evalBinop Sub v1 v2 = v1 - v2 /\ +evalBinop Mult v1 v2 = v1 * v2 /\ +evalBinop Div v1 v2 = v1 / (v2:real)`; +(** +Expressions will use unary operators. +Define them first +**) +val _ = Datatype ` +unop = Neg | Inv` + +(** +Define evaluation for unary operators on reals. +Errors are added in the expression evaluation level later +**) +val evalUnop_def = Define ` +evalUnop Neg v = - v /\ +evalUnop Inv v = 1 / (v:real)` (** Define expressions parametric over some value type 'v. Will ease reasoning about different instantiations later. Note that we @@ -34,18 +49,14 @@ val _ = Datatype ` exp = Var num | Param num | Const 'v + | Unop unop exp | Binop binop exp exp` (** Define a perturbation function to ease writing of basic definitions **) val perturb_def = Define ` - perturb (r:real) (e:real) = r * (1 + e)` - -(** - Abbreviations for the environment types -**) -val _ = type_abbrev("env_ty",``:num->real``); +perturb (r:real) (e:real) = r * (1 + e)` (** Define expression evaluation relation parametric by an "error" @@ -53,26 +64,36 @@ val _ = type_abbrev("env_ty",``:num->real``); using a perturbation of the real valued computation by (1 + d) **) val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln ` - (!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)) /\ - (!eps env b e1 e2 v1 v2 delta. - eval_exp eps env e1 v1 /\ - eval_exp eps env e2 v2 /\ - abs delta <= eps ==> - eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2) delta))`; + (!eps E (P:num->(real # real)) x. + eval_exp eps E P (Var x) (E x)) /\ + (!eps E P x delta. + abs delta <= eps /\ + fst (P x) <= (E x) /\ + (E v)<= snd (P x) ==> + eval_exp eps E P (Param x) (perturb (E x) delta)) /\ + (!eps E P delta. + abs delta <= eps ==> + eval_exp eps E P (Const n) (perturb n delta)) /\ + (!eps E P f1 v1. + eval_exp eps E P f1 v1 ==> + eval_exp eps E P (Unop Neg f1) (evalUnop Neg v1)) /\ + (!eps E P f1 v1 delta. + abs delta <= eps /\ + eval_exp eps E P f1 v1 ==> + eval_exp eps E P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)) /\ + (!eps E P b f1 f2 v1 v2 delta. + abs delta <= eps /\ + eval_exp eps E P f1 v1 /\ + eval_exp eps E P f2 v2 ==> + eval_exp eps E P (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`; val eval_exp_cases = map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_exp_cases]) - [``eval_exp eps env (Var v) res``, - ``eval_exp eps env (Param v) res``, - ``eval_exp eps env (Const n) res``, - ``eval_exp eps env (Binop n e1 e2) res``] + [``eval_exp eps E P (Var v) res``, + ``eval_exp eps E P (Param v) res``, + ``eval_exp eps E P (Const n) res``, + ``eval_exp eps E P (Unop u e) res``, + ``eval_exp eps E P (Binop n e1 e2) res``] |> LIST_CONJ |> curry save_thm "eval_exp_cases"; val delta_0_deterministic = store_thm("delta_0_deterministic", @@ -80,8 +101,8 @@ val delta_0_deterministic = store_thm("delta_0_deterministic", fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]); val meps_0_deterministic = store_thm("meps_0_deterministic", - ``!(e: real exp) v1:real v2:real env. - eval_exp (&0) env e v1 /\ eval_exp (&0) env e v2 ==> v1 = v2``, + ``!(e: real exp) v1:real v2:real E P. + eval_exp (&0) E P e v1 /\ eval_exp (&0) E P e v2 ==> v1 = v2``, Induct \\ fs [eval_exp_cases] \\ rw [] \\ fs [delta_0_deterministic] \\ res_tac \\ fs []); @@ -97,19 +118,19 @@ val _ = Datatype ` Define evaluation of boolean expressions *) val (bval_exp_rules, bval_exp_ind, bval_exp_cases) = Hol_reln ` - (!eps env e1 e2 v1 v2. - eval_exp eps env e1 v1 /\ - eval_exp eps env e2 v2 ==> - bval eps env (Leq e1 e2) (v1 <= v2))/\ - (!eps env e1 e2 v1 v2. - eval_exp eps env e1 v1 /\ - eval_exp eps env e2 v2 ==> - bval eps env (Less e1 e2) (v1 < v2))`; + (!eps E P e1 e2 v1 v2. + eval_exp eps E P e1 v1 /\ + eval_exp eps E P e2 v2 ==> + bval eps E P (Leq e1 e2) (v1 <= v2))/\ + (!eps E P e1 e2 v1 v2. + eval_exp eps E P e1 v1 /\ + eval_exp eps E P e2 v2 ==> + bval eps E P (Less e1 e2) (v1 < v2))`; val bval_exp_cases = map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bval_exp_cases]) - [``bval eps env (Leq e1 e2) res``, - ``bval eps env (Less e1 e2) res``] + [``bval eps E P (Leq e1 e2) res``, + ``bval eps E P (Less e1 e2) res``] |> LIST_CONJ |> curry save_thm "bval_exp_cases"; (* Simplify arithmetic later by making > >= only abbreviations *) @@ -117,12 +138,12 @@ val _ = overload_on("Gr",``\(e1:('v)exp). \(e2:('v)exp). Less e2 e1``); val _ = overload_on("Greq",``\(e1:('v)exp). \(e2:('v)exp). Leq e2 e1``); val binary_unfolding = store_thm("binary_unfolding", - ``!(b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) (cenv:env_ty) (v:real). - (eval_exp eps cenv (Binop b e1 e2) v <=> +``!(b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) (cenv:env) (P:precond) (v:real). + (eval_exp eps cenv P (Binop b e1 e2) v <=> (?(v1:real) (v2:real). - eval_exp eps cenv e1 v1 /\ - eval_exp eps cenv e2 v2 /\ - eval_exp eps ((2 =+ v2) ((1 =+ v1) cenv)) (Binop b (Var 1) (Var 2)) v))``, + eval_exp eps cenv P e1 v1 /\ + eval_exp eps cenv P e2 v2 /\ + eval_exp eps ((2 =+ v2) ((1 =+ v1) cenv)) P (Binop b (Var 1) (Var 2)) v))``, fs [eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS] \\ metis_tac []);