More cleanup. Make external dependencies explicit

coq/Expressions.v

 (**
 Formalization of the base expression language for the daisy framework
  **)
-Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Interval.Interval_tactic.
-Require Import Daisy.Infra.RealConstruction Daisy.Infra.RealSimps Daisy.Infra.Abbrevs.
+Require Import Coq.Reals.Reals Coq.micromega.Psatz.
+Require Import Daisy.Infra.RealSimps Daisy.Infra.Abbrevs.
 Set Implicit Arguments.
 (**
   Expressions will use binary operators.
@@ -38,16 +38,14 @@ Inductive exp (V:Type): Type :=
 **)
 Definition perturb (r:R) (e:R) :=
   Rmult r (Rplus 1 e).
-(**
-  Abbreviation for the environment types
- **)
-Definition env_ty := nat -> R.
-Definition analysisResult :Type := exp Q -> intv * error.
 
 (**
-  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)
+Define expression evaluation relation parametric by an "error" epsilon.
+This value will be used later to express float computations using a perturbation
+of the real valued computation by (1 + delta), where |delta| <= machine epsilon.
+
+It is important that variables are not perturbed when loading from an environment.
+This is the case, since loading a float value should not increase an additional error.
 **)
 Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
   Var_load x: eval_exp eps env (Var R x) (env x)
@@ -63,6 +61,9 @@ Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
                 eval_exp eps env e2 v2 ->
                 eval_exp eps env (Binop op e1 e2) (perturb (eval_binop op v1 v2) delta).
 
+(**
+If |delta| <= 0 then perturb v delta is exactly v
+**)
 Lemma perturb_0_val (v:R) (delta:R):
   (Rabs delta <= 0)%R ->
   perturb v delta = v.
@@ -75,6 +76,9 @@ Proof.
   rewrite Rplus_0_r; auto.
 Qed.
 
+(**
+Evaluation with 0 as epsilon is deterministic
+**)
 Lemma eval_0_det (e:exp R) (env:env_ty):
   forall v1 v2,
   eval_exp R0 env e v1 ->
@@ -89,6 +93,13 @@ Proof.
   rewrite (IHe2 v3 v5); auto.
 Qed.
 
+(**
+Helping lemma. Needed in soundness proof.
+For each evaluation of using an arbitrary epsilon, we can replace it by
+evaluating the subexpressions and then binding the result values to different
+variables in the environment.
+This needs the property that variables are not perturbed as opposed to parameters
+**)
 Lemma existential_rewriting (b:binop) (e1:exp R) (e2:exp R) (eps:R) (cenv:env_ty) (v:R):
   (eval_exp eps cenv (Binop b e1 e2) v <->
    exists v1 v2,

coq/Infra/Abbrevs.v

-Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
 (**
   Some type abbreviations, to ease writing
  **)
+Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
 (**
-  Intervals are a type, consisting of a pair of two real numbers
-  Additionally add some constructing and destructing definitions for encapsulation and
-  define them to automatically unfold upon simplification.
+We define Intervals twice.
+First we define intervals of reals and fractions.
+We need both of them since the analysis argues about intervals of fractions
+and the proofs should argue about real valued exections.
+
+Intervals are defined as a type, consisting of a pair of two real numbers or fractions.
+Additionally add some constructing and destructing definitions for encapsulation and
+define them to automatically unfold upon simplification.
  **)
 Definition interval:Type := R * R.
 Definition err:Type := R.
@@ -18,18 +23,8 @@ Arguments mkInterval _ _/.
 Arguments IVlo _ /.
 Arguments IVhi _ /.
 
-Definition getIntv (val:ann) := fst val.
-Definition getErr (val:ann) := snd val.
-
-Arguments getIntv _ /.
-Arguments getErr _ /.
-
 Definition intv:Type := Q * Q.
-(*
-Record Qpos : Type := mkQPos {Qposval:> Q; QposGeq0: Qle_bool 0 Qposval = true}. *)
 Definition error :Type := Q.
-(*
-Coercion IntvOfErrors (p:error*error) := (Qposval (fst p),Qposval (snd p)):intv. *)
 
 Definition mkIntv (ivlo:Q) (ivhi:Q) := (ivlo,ivhi).
 Definition ivlo (intv:intv) := fst intv.
@@ -39,13 +34,35 @@ Arguments mkIntv _ _/.
 Arguments ivlo _ /.
 Arguments ivhi _ /.
 
+(**
+Later we will argue about program preconditions.
+Define a precondition to be a function mapping numbers (resp. variables) to intervals.
+**)
 Definition precond :Type := nat -> intv.
+
+(**
+  Abbreviation for the environment types for expression evaluation
+ **)
+Definition env_ty := nat -> R.
+
 (**
-  Define environment update function for arbitrary type as abbreviation.
-  This must be defined here, to prove some lemmas about expression evaluation.
-  See below.
+  Define environment update function as abbreviation.
 **)
-Definition updEnv (x:nat) (v: R) (E: nat -> R) (y:nat) :R :=
+Definition updEnv (x:nat) (v: R) (env:env_ty) (y:nat) :R :=
   if y =? x
   then v
-  else E y.
\ No newline at end of file
+  else env 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_ty) :=
+  forall v:nat,
+    let (ivlo,ivhi) := P v in
+    (Q2R ivlo <= cenv v <= Q2R ivhi)%R.
\ No newline at end of file

coq/Infra/ExpressionAbbrevs.v

+(**
+Some abbreviations that require having defined expressions beforehand
+**)
 Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals.
 Require Export Daisy.Infra.Abbrevs Daisy.Expressions.
 
+(**
+We treat a function mapping an expression arguing on fractions as value type
+to pairs of intervals on rationals and rational errors as the analysis result
+**)
 Definition analysisResult :Type := exp Q -> intv * error.
\ No newline at end of file
-
-Definition precondValidForExec (P:nat->intv) (cenv:nat->R) :=
-  forall v:nat,
-    let (ivlo,ivhi) := P v in
-    (Q2R ivlo <= cenv v <= Q2R ivhi)%R.
\ No newline at end of file

coq/Infra/RealRationalProps.v

 Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
 Require Import Coq.Reals.Reals Coq.micromega.Psatz.
+Require Import Flocq.Core.Fcore_Raux.
 Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions Daisy.IntervalArith.
 
 Fixpoint toRExp (e:exp Q) :=

coq/IntervalArith.v

@@ -3,6 +3,7 @@
   TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
 **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
+Require Import Coquelicot.Rcomplements.
 Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RealSimps.
 (**
   Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.

coq/PreconditionValidation.v

@@ -6,16 +6,16 @@ Import Lists.List.ListNotations.
 Fixpoint freeVars (V:Type) (e:exp V) : list nat:=
   match e with
   |Const n => []
-  |Var v => []
-  |Param v => [v]
+  |Var _ v => []
+  |Param _ v => [v]
   |Binop b e1 e2 => (freeVars V e1) ++ (freeVars V e2)
   end.
 
 Fixpoint approximatesPrecond (e:exp Q) (absenv:analysisResult) (P:precond) :=
   match e with
   |Const n => true
-  |Var v => true
-  |Param v =>
+  |Var _ v => true
+  |Param _ v =>
    let (vprelo, vprehi) := P v in
    let (iv,err) := absenv (Param Q v) in
    let (vlo,vhi) := iv in