From a9f3048929f55aa6fd47dd30d82a0ce7e2cc914b Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Tue, 3 Jan 2017 10:43:14 +0100
Subject: [PATCH] Remove some unused lines from Coq development and rework
 definitions in HOL4 to contain current state of Coq development

---
 coq/Expressions.v          |   4 +-
 coq/Infra/Abbrevs.v        |  14 -----
 hol4/abbrevsScript.sml     |  35 ++++++++++++
 hol4/expressionsScript.sml | 113 ++++++++++++++++++++++---------------
 4 files changed, 104 insertions(+), 62 deletions(-)
 create mode 100644 hol4/abbrevsScript.sml

diff --git a/coq/Expressions.v b/coq/Expressions.v
index 6df158d..3127df9 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 dc2a58e..0955bf7 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 0000000..4e971bd
--- /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 c8ee6aa..9637d42 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 []);
 
-- 
GitLab