Start working on toy example proof, add coq definitions

coq/exps.v

+(**
+Formalization of the base expression language for the daisy framework
+ **)
+Require Import Coq.Reals.Reals.
+Set Implicit Arguments.
+(**
+  Expressions will use binary operators.
+  Define them first
+**)
+Inductive binop : Type := Plus | Sub | Mult | Div.
+(**
+  Next define an evaluation function for binary operators on reals.
+  Errors are added on the expression evaluation level later.
+ **)
+Fixpoint eval_binop (o:binop) (v1:R) (v2:R) :=
+  match o with
+  | Plus => Rplus v1 v2
+  | Sub => Rminus v1 v2
+  | Mult => Rmult v1 v2
+  | Div => Rdiv v1 v2
+  end.
+(*
+  Define expressions parametric over some value type V.
+  Will ease reasoning about different instantiations later.
+*)
+Inductive exp (V:Type): Type :=
+  Var: nat -> exp V
+| Const: V -> exp V
+| Binop: binop -> exp V -> exp V -> exp V.
+(**
+  Define the machine epsilon for floating point operations.
+  FIXME: Currently set to 1.0 instead of the concrete value!
+**)
+Definition m_eps:R := 1.
+(**
+  Define a perturbation function to ease writing of basic definitions
+**)
+Definition perturb (r:R) (e:R) :=
+  Rmult r (Rplus 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.
+**)
+Fixpoint eval_err (e:exp R) (err_fun:exp R-> R) (env:nat -> R) :=
+  match e with
+  |Var _ n => perturb (env n) (err_fun (Var _ n))
+  |Const v => perturb v (err_fun (Const v))
+  |Binop op e1 e2 => let v1 := eval_err e1 err_fun env in
+                    let v2 := eval_err e2 err_fun env in
+                    perturb (eval_binop op v1 v2) (err_fun (Binop op e1 e2))
+  end.
+(**
+  Define real evaluation as stated above:
+**)
+Definition eval_real (e:exp R) (env:nat -> R) := eval_err e (fun x => R0) env.
+(**
+  float evaluation is non-deterministic, since the perturbation is existencially quantified
+  --> state as predicate when float evaluation using errors is valid, related to errors
+**)
+Definition is_valid_err_float (err_fun: nat -> R) : Prop :=
+  forall id, exists n:R,
+      (n = err_fun id \/ (Ropp n) = err_fun id) /\
+      Rle (Rabs n) m_eps.
+(**
+  Using the parametric expressions, define boolean expressions for conditionals
+**)
+Inductive bexp (V:Type) : Type :=
+  leq: exp V -> exp V -> bexp V
+| less: exp V -> exp V -> bexp V.
+(**
+  Define evaluation of booleans for reals
+**)
+Fixpoint bval_SIMPS (b:bexp R) (env:nat -> R) (eval: exp R -> (nat -> R) -> R) :=
+  match b with
+  |leq e1 e2 => Rle (eval e1 env) (eval e2 env)
+  |less e1 e2 => Rlt (eval e1 env) (eval e2 env)
+end.
+
+(**
+ Simplify arithmetic later by making > >= only abbreviations
+**)
+Definition gr := fun (V:Type) (e1: exp V) (e2: exp V) => less e2 e1.
+Definition greq := fun (V:Type) (e1:exp V) (e2: exp V) => leq e2 e1.
\ No newline at end of file

hol/exps.hl

@@ -5,6 +5,21 @@
 needs "Infra/tactics.hl";;
 (* needs "/home/heiko/Git_Repos/hol-light/IEEE/make.ml";; *)
 
+(*
+  Expressions will use binary operators.
+  Define them first
+*)
+let binop_INDUCT, binop_REC = define_type
+  "binop = Plus | Sub | Mult | Div ";;
+(*
+  Define an evaluation function for binary operators.
+  Errors are added on the expression evaluation level later
+*)
+let eval_binop = new_recursive_definition binop_REC
+  `(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)`;;
 (*
   Define expressions parametric over some value type V.
   Will ease reasoning about different instantiations later.
@@ -12,21 +27,16 @@ needs "Infra/tactics.hl";;
 let exp_INDUCT, exp_REC= define_type
   "exp = Var num
   | Const V
-  | Plus exp exp
-  | Sub exp exp
-  | Mult exp exp
-  | Div exp exp";;
-
+  | Binop binop 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)`;;
+let perturb = define `(perturb:real->real->real) = \r e. r * ((&1) + e)`;;
 (*
   Define expression evaluation parametric by an "error function".
   This function will be used later to express float computations using a perturbation
@@ -34,32 +44,19 @@ let perturb_def = define `(perturb:real->real->real) = \r e. e * ((&1) + e)`;;
   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))))`;;
+  `(eval_err (Var name) err_fun env
+    = perturb (env name) (err_fun (Var name))) /\
+  (eval_err (Const v) err_fun env
+   = perturb v (err_fun (Const v))) /\
+  (eval_err (Binop binop e1 e2) err_fun env
+   = perturb (eval_binop binop (eval_err e1 err_fun env) (eval_err e2 err_fun env))
+      (err_fun (Binop binop 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) env`;;
+  `eval_real (e:(real)exp) (env:num->real) = eval_err e (\x. &0) env`;;
 
 (*
   float evaluation is non-deterministic, since the perturbation is existencially quantified

hol/toy_example.hl

 (*
-
+  Toy Example to get a feeling for what needs to be done for certificate checking
 *)
 needs "daisy_lang.hl";;
 
@@ -8,7 +8,25 @@ let prg = define
   Let 1 (Mult (Const (&2)) (Var 2))
     (Ret (Mult (Const (&3)) (Var 1)))`;;
 
-let prg_float = define
-  `prg_float:(float)cmd =
+let abs_err = define `abs_err = &1`;; (* TODO: FIXME *)
+
+g `!fl_err_fun err_ids env env_final_real env_final_float.
+  is_valid_err_float fl_err_fun ==>
+  bstep prg env eval_real Nop env_final_real ==>
+  bstep prg env (\e. eval_err e fl_err_fun err_ids) Nop env_final_float ==>
+  abs (env_final_real 0 - env_final_float 0) <= abs_err`;;
 
-g `
+e (REWRITE_TAC [prg]);;
+e (INTRO_TAC
+     "!fl_err_fun err_ids env env_final_real env_final_float;
+      error_fl_valid; terminates_real; terminates_float");;
+e (SUBGOAL_THEN `?v. eval_real (Mult (Const (&2)) (Var 2)) env = v` (LABEL_TAC "exists_val"));;
+e (REWRITE_TAC[eval_real;eval_err]);;
+e (REWRITE_TAC[perturb]);;
+e (EXISTS_TAC `&0`);;
+e (REAL_ARITH_TAC);;
+e (REMOVE_THEN "exists_val" (DESTRUCT_TAC "@v. val_def"));;
+e (SUBGOAL_THEN `bstep (Ret (Mult (Const (&3)) (Var 1))) (upd_env 1 v env) eval_real Nop env_final_real` ASSUME_TAC);;
+e (ASM_MESON_TAC[bstep_CASES]);;
+e (REWRITE_TAC[bstep_CASES]);;
+b();;