Remove some unused lines from Coq development and rework definitions in HOL4...

Remove some unused lines from Coq development and rework definitions in HOL4 to contain current state of Coq development

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.

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

hol4/abbrevsScript.sml

+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();

hol4/expressionsScript.sml

 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 /\
+   (!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 env (Binop b e1 e2) (perturb (eval_binop b v1 v2) delta))`;
+         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 []);