Some minor syntactic simplifications in coq dev

coq/Commands.v

 (**
  Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
-FIXME: Currently the semantics are stateful. But daisy actually assumes that a variable may not be verwritten?
  **)
 Require Import Coq.Reals.Reals.
 Require Export Daisy.Infra.ExpressionAbbrevs.
@@ -30,10 +29,10 @@ Inductive sstep : cmd R -> env -> env -> precond -> R -> cmd R -> env -> Prop :=
   parametric by the evaluation function
  **)
 Inductive bstep : cmd R -> env -> env -> precond -> R -> cmd R -> env -> Prop :=
-  let_b x e s s' VarEnv ParamEnv P v eps env2:
+  let_b x e s s' VarEnv ParamEnv P v eps VarEnv2:
     eval_exp eps VarEnv ParamEnv P e v ->
-    bstep s (updEnv x v VarEnv) ParamEnv P eps s' env2 ->
-    bstep (Let R x e s) VarEnv ParamEnv P eps s' env2
+    bstep s (updEnv x v VarEnv) ParamEnv P eps s' VarEnv2 ->
+    bstep (Let R x e s) VarEnv ParamEnv P eps s' VarEnv2
  |ret_b e VarEnv ParamEnv P v eps:
     eval_exp eps VarEnv ParamEnv P e v ->
     bstep (Ret R e) VarEnv ParamEnv P eps (Nop R) (updEnv 0 v VarEnv).
\ No newline at end of file

coq/Environments.v

@@ -16,27 +16,5 @@ expression may yield different values for different machine epsilons
 Inductive approxEnv : env -> analysisResult -> env -> Prop :=
 |approxRefl E A: approxEnv E A E
 |approxUpd E1 E2 A v1 v2 x: approxEnv E1 A E2 ->
-							(Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
-                            approxEnv (updEnv x v1 E1) A (updEnv x v2 E2).
-
-(*
-Lemma small_step_preserves_sim A P f g E1 E2 E1' E2' eps:
-  approxEnv E1 A E2 ->
-  sstep f E1 P 0 g E1' ->
-  sstep f E2 P eps g E2' ->
-  approxEnv E1' A E2'.
-Proof.
-  intros approxBefore.
-  induction f; intros stepLet1 stepLet2.
-  - inversion stepLet1; inversion stepLet2; subst.
-    eapply approxUpd.
-    apply approxBefore.
-    instantiate (1 := Rabs (v - v0)).
-    lra.
-  - inversion stepLet1; inversion stepLet2; subst.
-    eapply approxUpd.
-    apply approxBefore.
-    instantiate (1 := Rabs(v - v0)).
-    lra.
-  - inversion stepLet1.
-Qed. *)
\ No newline at end of file
+			    (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
+                            approxEnv (updEnv x v1 E1) A (updEnv x v2 E2).
\ No newline at end of file

coq/Expressions.v

@@ -117,9 +117,11 @@ Unary negation is special! We do not have a new error here since IEE 754 gives u
 **)
 Inductive eval_exp (eps:R) (VarEnv:env) (ParamEnv:env) (P:precond) : (exp R) -> R -> Prop :=
   Var_load x: eval_exp eps VarEnv ParamEnv P (Var R x) (VarEnv x)
-| Param_acc x delta:
+| Param_acc x delta delta_lo delta_hi:
     ((Rabs delta) <= eps)%R ->
-    ((perturb (Q2R (fst (P x))) delta) <= perturb (ParamEnv x) delta <= (perturb (Q2R (snd (P x))) delta))%R ->
+    ((Rabs delta_lo) <= eps)%R ->
+    ((Rabs delta_hi) <= eps)%R ->
+    ((perturb (Q2R (fst (P x))) delta_lo) <= perturb (ParamEnv x) delta <= (perturb (Q2R (snd (P x))) delta_hi))%R ->
     eval_exp eps VarEnv ParamEnv P (Param R x) (perturb (ParamEnv x) delta)
 | Const_dist n delta:
     Rle (Rabs delta) eps ->