Stqrting the port to HOL4 of the mixed precision formalization

coq/Expressions.v

@@ -204,6 +204,7 @@ Fixpoint toREval (e:exp R) :=
   | Downcast _ e1 =>  (toREval e1)
   end.
 
+(* TODO: put to REValVars here? *)
 
 
 (**
@@ -272,7 +273,7 @@ Proof.
   lra.
 Qed.
 
-    
+(* TODO: need of `general` case? *)
 Lemma general_meps_0_deterministic (f:exp R) (E:env) defVars:
   forall v1 v2 m1,
     m1 = M0 ->

coq/Infra/MachineType.v

@@ -11,7 +11,7 @@ Definition inj_eps_Q (e:mType) : Q :=
   match e with
   | M0 => 0
   | M32 => (Qpower (2#1) (Zneg 24))
-  | M64 => (Qpower (2#1) (Zneg 54))
+  | M64 => (Qpower (2#1) (Zneg 53))
   | M128 => (Qpower (2#1) (Zneg 113))
   | M256 => (Qpower (2#1) (Zneg 237))
   end.
@@ -38,6 +38,7 @@ Qed.
 (* Definition mTypeEqBool (m1:mType) (m2:mType) := *)
 (*   Qeq_bool (meps m1) (meps m2). *)
 
+(* TODO: unused? *)
 Theorem eq_mType_dec: forall (m1 m2:mType), {m1 = m2} + {m1 <> m2}.
 Proof.
   intros.
@@ -147,6 +148,11 @@ Qed.
 (*   Qle (meps m1) (meps m2). *)
 
 
+Definition computeJoin (m1:mType) (m2:mType) :=
+  if (isMorePrecise m1 m2) then m1 else m2.
+
+
+(* Everything below is unused? *)
 Definition isJoinOf (m:mType) (m1:mType) (m2:mType) :=
   (* is m the join of m1 and m2 ?*)
   if (isMorePrecise m1 m2) then
@@ -154,10 +160,6 @@ Definition isJoinOf (m:mType) (m1:mType) (m2:mType) :=
   else
     mTypeEqBool m m2.
 
-
-Definition computeJoin (m1:mType) (m2:mType) :=
-  if (isMorePrecise m1 m2) then m1 else m2.
-
 Lemma ifisMorePreciseM0 (m:mType) :
   isMorePrecise M0 m = true -> m = M0.
 Proof.

hol4/ExpressionsScript.sml

@@ -3,7 +3,7 @@
  **)
 open preamble miscTheory
 open realTheory realLib sptreeTheory
-open AbbrevsTheory
+open AbbrevsTheory MachineTypeTheory
 
 val _ = ParseExtras.temp_tight_equality()
 
@@ -47,9 +47,19 @@ val evalUnop_def = Define `
 **)
 val _ = Datatype `
   exp = Var num
-      | Const 'v
+      | Const mType 'v
       | Unop unop exp
-      | Binop binop exp exp`
+      | Binop binop exp exp
+      | Downcast mType exp`
+
+val toREval_def = Define `
+  toREval (e:real exp) : real exp =
+	case e of
+	  | Var n => Var n
+	  | Const m n => Const M0 n
+	  | Unop u e1 => Unop u (toREval e1)
+	  | Binop bop e1 e2 => Binop bop (toREval e1) (toREval e2)
+	  | Downcast m e1 => (toREval e1)`;
 
 (**
   Define a perturbation function to ease writing of basic definitions
@@ -64,43 +74,51 @@ using a perturbation of the real valued computation by (1 + delta), where
 |delta| <= machine epsilon.
 **)
 val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
-  (!eps E x v.
+  (!E defVars m x v.
+     defVars x = SOME m /\
      E x = SOME v ==>
-     eval_exp eps E (Var x) v) /\
-  (!eps E n delta.
-     abs delta <= eps ==>
-     eval_exp eps E (Const n) (perturb n delta)) /\
-  (!eps E f1 v1.
-     eval_exp eps E f1 v1 ==>
-     eval_exp eps E (Unop Neg f1) (evalUnop Neg v1)) /\
-  (!eps E f1 v1 delta.
-     abs delta <= eps /\
-     eval_exp eps E f1 v1 ==>
-     eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta)) /\
-  (!eps E b f1 f2 v1 v2 delta.
-     abs delta <= eps /\
-     eval_exp eps E f1 v1 /\
-     eval_exp eps E f2 v2 /\
-    ((b = Div) ==> (~ v2 = 0)) ==>
-     eval_exp eps E (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
+     eval_exp E defVars (Var x) v m) /\
+  (!E defVars m n delta.
+     abs delta <= (meps m) ==>
+     eval_exp E defVars (Const m n) (perturb n delta) m) /\
+  (!E defVars m f1 v1.
+     eval_exp E defVars f1 v1 m ==>
+     eval_exp E defVars (Unop Neg f1) (evalUnop Neg v1) m) /\
+  (!E defVars m f1 v1 delta.
+     abs delta <= (meps m) /\
+     eval_exp E defVars f1 v1 m ==>
+     eval_exp E defVars (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m) /\
+  (!E defVars m1 m2 b f1 f2 v1 v2 delta.
+     abs delta <= (meps (computeJoin m1 m2)) /\
+     eval_exp E defVars f1 v1 m1 /\
+     eval_exp E defVars f2 v2 m2 /\
+     ((b = Div) ==> (~ v2 = 0)) ==>
+     eval_exp E defVars (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (computeJoin m1 m2)) /\
+  (!E defVars m m1 f1 v1 delta.
+     isMorePrecise m1 m = T /\
+     abs delta <= (meps m) /\
+     eval_exp E defVars f1 v1 m1 ==>
+     eval_exp E defVars (Downcast m f1) (perturb v1 delta) m)`;
 
 (**
   Generate a better case lemma
 **)
 val eval_exp_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_exp_cases])
-    [``eval_exp eps E (Var v) res``,
-     ``eval_exp eps E (Const n) res``,
-     ``eval_exp eps E (Unop u e) res``,
-     ``eval_exp eps E (Binop n e1 e2) res``]
+    [``eval_exp E defVars (Var v) res m``,
+     ``eval_exp E defVars (Const m n) res m``,
+     ``eval_exp E defVars (Unop u e) res m``,
+     ``eval_exp E defVars (Binop n e1 e2) res m``,
+	 ``eval_exp E defVars (Downcast m e1) res m``]
   |> LIST_CONJ |> curry save_thm "eval_exp_cases";
 
-val [Var_load, Const_dist, Unop_neg, Unop_inv, Binop_dist] = CONJ_LIST 5 eval_exp_rules;
+val [Var_load, Const_dist, Unop_neg, Unop_inv, Binop_dist, Downcast_dist] = CONJ_LIST 6 eval_exp_rules;
 save_thm ("Var_load", Var_load);
 save_thm ("Const_dist", Const_dist);
 save_thm ("Unop_neg", Unop_neg);
 save_thm ("Unop_inv", Unop_inv);
 save_thm ("Binop_dist", Binop_dist);
+save_thm ("Downcast_dist", Downcast_dist);
 
 (**
   Define the set of "used" variables of an expression to be the set of variables
@@ -112,6 +130,7 @@ val usedVars_def = Define `
       | Var x => insert x () (LN)
       | Unop u e1 => usedVars e1
       | Binop b e1 e2 => union (usedVars e1) (usedVars e2)
+	  | Downcast m e1 => usedVars e1
       | _ => LN`;
 
 (**
@@ -125,11 +144,34 @@ val delta_0_deterministic = store_thm("delta_0_deterministic",
 Evaluation with 0 as machine epsilon is deterministic
 **)
 val meps_0_deterministic = store_thm("meps_0_deterministic",
-  ``!(e: real exp) v1:real v2:real E.
-      eval_exp (&0) E e v1 /\ eval_exp (&0) E e v2 ==> v1 = v2``,
+  ``!(e: real exp) v1:real v2:real E defVars.
+      eval_exp E defVars (toREval e) v1 M0 /\ eval_exp E defVars (toREval e) v2 M0 ==> v1 = v2``,
   Induct \\ fs [eval_exp_cases]
-  \\ rw [] \\ fs [delta_0_deterministic]
-  \\ res_tac \\ fs []);
+	  \\ rw [toREval_def]
+	  \\ rw [] \\ fs [meps_def,inj_eps_Q_def,delta_0_deterministic]
+	 \\ res_tac \\ fs []);
+
+Induct 
+    >- (rw [toREval_def] >> fs [eval_exp_cases] >> rw [] >> fs [delta_0_deterministic] >> res_tac >> fs [])
+    >- (rw [toREval_def] \\ fs [eval_exp_cases] \\ rw [] \\ fs [meps_def,inj_eps_Q_def] \\ fs [delta_0_deterministic] \\ res_tac \\ fs [])
+    >- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ fs [eval_exp_cases]
+	   >- (res_tac \\ fs [REAL_NEG_EQ])
+	   >- rw []
+	   >- rw []
+	   >- (res_tac \\ fs [meps_def,inj_eps_Q_def,delta_0_deterministic]))
+    >- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ fs [eval_exp_cases] \\ 
+`abs delta <= meps M0` by fs [] \\ res_tac
+qpat_x_assum `abs delta <= meps (computeJoin m1 m2)` kall_tac
+qpat_x_assum `_ = computeJoin m1 m2` kall_tac
+`abs delta' <= meps M0` by fs [] \\ res_tac
+qpat_x_assum `abs delta' <= meps (computeJoin m1' m2')` kall_tac
+qpat_x_assum `_ = computeJoin _ _ ` kall_tac
+fs [meps_def,inj_eps_Q_def,delta_0_deterministic]
+`v1'' = v1'` by res_tac
+
+
+simp [toREval_def] \\ fs [eval_exp_cases] \\ rw [] \\ fs [meps_def,inj_eps_Q_def] \\ fs [delta_0_deterministic] \\ res_tac \\ fs []
+    
 
 (**
 Helping lemma. Needed in soundness proof.

hol4/MachineTypeScript.sml

+open preamble miscTheory
+open realTheory realLib sptreeTheory
+
+val _ = new_theory "MachineType";
+
+val _ = Datatype `
+  mType = M0 | M32 | M64 | M128 | M256`;
+
+val inj_eps_Q_def = Define `
+  inj_eps_Q (m:mType) : real =
+    case m of 
+      | M0 => 0
+      | M32 => 1 / (2 pow 24)
+      | M64 => 1 / (2 pow 53)
+      | M128 => 1 / (2 pow 113)
+      | M256 => 1 / (2 pow 237)`;
+
+val meps_def = Define `meps = inj_eps_Q`;
+
+val inj_eps_pos = store_thm("inj_eps_pos",
+  ``!e. 0 <= inj_eps_Q e``,
+  Cases_on `e` >> EVAL_TAC);
+
+
+(* check if m1 is more precise than m2, i.e. if the epsilon of m1 is *)
+(*   smaller than the epsilon of m2 *)
+val isMorePrecise_def = Define `
+  isMorePrecise (m1:mType) (m2:mType) =
+    if (m2 = M0) then 
+	T
+    else if (m1 = M0) then
+	m2 = M0
+    else
+        (meps m1) <= (meps m2)`;
+
+val computeJoin_def = Define `
+  computeJoin (m1:mType) (m2:mType) =
+	if (isMorePrecise m1 m2) then m1 else m2`;
+
+
+val _ = export_theory();