Prove exp eval deterministic in coq, prove side-lemma in HOL

coq/exps.v

@@ -38,31 +38,56 @@ Definition m_eps:R := 1.
 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
+  Define expression evaluation relation parametric by an "error" delta.
+  This value 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.
+Inductive eval_exp (eps:R) (env:nat -> R) : (exp R) -> R -> Prop :=
+  Var_load x: eval_exp eps env (Var R x) (env x)
+| Const_dist n delta:
+    Rle (Rabs delta) eps ->
+    eval_exp eps env (Const n) (perturb n delta)
+|Binop_dist op e1 e2 v1 v2 delta:
+   Rle (Rabs delta) eps ->
+                eval_exp eps env e1 v1 ->
+                eval_exp eps env e2 v2 ->
+                eval_exp eps env (Binop op e1 e2) (perturb (eval_binop op v1 v2) delta).
 (**
   Define real evaluation as stated above:
-**)
-Definition eval_real (e:exp R) (env:nat -> R) := eval_err e (fun x => R0) env.
+ **)
+Definition is_real_value (e:exp R) (env:nat -> R) (v:R) := eval_exp R0 env e v.
 (**
-  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.
+  Prove that using eps = 0 makes the evaluation deterministic
+ **)
+Lemma Rabs_0_impl_eq (d:R):
+  Rle (Rabs d) R0 -> d = R0.
+Proof.
+  intros abs_leq_0.
+  pose proof (Rabs_pos d) as abs_geq_0.
+  pose proof (Rle_antisym (Rabs d) R0 abs_leq_0 abs_geq_0) as Rabs_eq.
+  rewrite <- Rabs_R0 in Rabs_eq.
+  apply Rsqr_eq_asb_1 in Rabs_eq.
+  rewrite Rsqr_0 in Rabs_eq.
+  apply Rsqr_0_uniq in Rabs_eq; assumption.
+Qed.
+
+Lemma eval_det (e:exp R) (env:nat -> R):
+  forall v1 v2,
+  eval_exp R0 env e v1 ->
+  eval_exp R0 env e v2 ->
+  v1 = v2.
+Proof.
+  induction e; intros v1 v2 eval_v1 eval_v2; inversion eval_v1; inversion eval_v2; try auto.
+  - apply Rabs_0_impl_eq in H0;
+      apply Rabs_0_impl_eq in H3.
+    rewrite H0, H3; reflexivity.
+  - apply Rabs_0_impl_eq in H2;
+      apply Rabs_0_impl_eq in H9.
+    rewrite H2, H9.
+    subst.
+    rewrite (IHe1 v0 v4); auto.
+    rewrite (IHe2 v3 v5); auto.
+Qed.
 (**
   Using the parametric expressions, define boolean expressions for conditionals
 **)
@@ -71,13 +96,16 @@ Inductive bexp (V:Type) : Type :=
 | 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.
-
+ **)
+Inductive bval (eps:R) (env:nat -> R) : (bexp R) -> Prop -> Prop :=
+  leq_eval (e1:exp R) (e2:exp R) (v1:R) (v2:R):
+    eval_exp eps env e1 v1 ->
+    eval_exp eps env e2 v2 ->
+    bval eps env (leq e1 e2) (Rle v1 v2)
+|less_eval (e1:exp R) (e2:exp R) (v1:R) (v2:R):
+    eval_exp eps env e1 v1 ->
+    eval_exp eps env e2 v2 ->
+    bval eps env (less e1 e2) (Rlt v1 v2).
 (**
  Simplify arithmetic later by making > >= only abbreviations
 **)

hol/exps.hl

@@ -56,6 +56,18 @@ let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
 *)
 let is_real_value = define
   `is_real_value (e:(real)exp) (env:num->real) (v:real) = eval_exp (&0) env e v`;;
+
+let abs_leq_0_impl_zero =
+  prove (
+    `!d:real. abs d <= &0 ==> d = &0`,
+    INTRO_TAC "!d; abs_leq_0"
+      THEN SUBGOAL_TAC "abs_geq_0" `&0 <= abs d` [(REWRITE_TAC[REAL_ABS_POS])]
+      THEN SUBGOAL_TAC "abs_geq_leq_0" `abs d <= &0 /\ &0 <= abs d` [CONJ_TAC THEN (ASM_REWRITE_TAC[])]
+      THEN SUBGOAL_TAC "abs_eq_0" `abs d = &0` [ALL_TAC]
+          THEN MP_TAC (ASSUME `abs d <= &0 /\ &0 <= abs d`)
+          THEN ASM_REWRITE_TAC [SPECL [`abs d`; `&0:real`] REAL_LE_ANTISYM]
+          THEN MP_TAC (ASSUME `abs d = &0`)
+          THEN ASM_REWRITE_TAC [REAL_ABS_ZERO]);;
 (*
   Using the parametric expressions, define boolean expressions for conditionals
 *)