Expressions.v 5.47 KB
Newer Older
1 2 3
(**
Formalization of the base expression language for the daisy framework
 **)
Heiko Becker's avatar
Heiko Becker committed
4
Require Import Coq.Reals.Reals Interval.Interval_tactic.
Heiko Becker's avatar
Heiko Becker committed
5
Require Import Daisy.Infra.RealConstruction.
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
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!
Heiko Becker's avatar
Heiko Becker committed
34 35 36
 **)
Definition machineEpsilon:R := realFromNum 1 1 53.
(* Definition machineEpsilon:R := realFromNum 11102230246251565 16 16. *)
37 38 39 40 41
(**
  Define a perturbation function to ease writing of basic definitions
**)
Definition perturb (r:R) (e:R) :=
  Rmult r (Rplus 1 e).
42 43 44 45
(**
  Abbreviation for the type of an environment
 **)
Definition env_ty := nat -> R.
46
(**
47 48
  Define expression evaluation relation parametric by an "error" delta.
  This value will be used later to express float computations using a perturbation
49 50
  of the real valued computation by (1 + d)
**)
51
Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
52 53 54 55 56 57 58 59 60
  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).
61 62
(**
  Define real evaluation as stated above:
63
 **)
64
Definition is_real_value (e:exp R) (env:env_ty) (v:R) := eval_exp R0 env e v.
65
(**
66 67 68 69 70 71 72 73 74 75 76 77 78 79
  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.

80
Lemma eval_det (e:exp R) (env:env_ty):
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
  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.
Heiko Becker's avatar
Heiko Becker committed
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140

Lemma perturb_0_val (v:R) (delta:R):
  (Rabs delta <= 0)%R ->
  perturb v delta = v.
Proof.
  intros abs_0; apply Rabs_0_impl_eq in abs_0; subst.
  unfold perturb.
  rewrite Rmult_plus_distr_l.
  rewrite Rmult_0_r.
  rewrite Rmult_1_r.
  rewrite Rplus_0_r; auto.
Qed.

Lemma Rsub_eq_Ropp_Rplus (a:R) (b:R) :
  (a - b = a + (- b))%R.
Proof.
  field_simplify; reflexivity.
Qed.

Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
  forall cenv:nat -> R,
  eval_exp 0%R cenv (Const n) nR ->
  eval_exp machineEpsilon cenv (Const n) nF ->
  (Rabs (nR - nF) <= Rabs (n * machineEpsilon))%R.
Proof.
  intros cenv eval_real eval_float.
  inversion eval_real; subst.
  rewrite perturb_0_val; auto.
  inversion eval_float; subst.
  unfold perturb; simpl.
  rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
  rewrite Ropp_plus_distr.
  assert (-n + (- (n * delta0)) = ( -(n * delta0) + - n))%R by (rewrite Rplus_comm; auto).
  rewrite H.
  rewrite <- Rsub_eq_Ropp_Rplus.
  rewrite Rplus_minus.
  rewrite Rabs_Ropp.
  repeat rewrite Rabs_mult.
  apply Rmult_le_compat_l.
  - apply Rabs_pos.
  - assert (Rabs machineEpsilon = machineEpsilon).
    + unfold machineEpsilon.
Heiko Becker's avatar
Heiko Becker committed
141
      unfold realFromNum, negativePower.
Heiko Becker's avatar
Heiko Becker committed
142 143 144 145 146 147 148 149
      unfold Rabs.
      destruct Rcase_abs; auto.
      exfalso.
      apply (Rlt_not_ge _ _ r).
      interval.
    + rewrite H2; auto.
Qed.

Heiko Becker's avatar
Heiko Becker committed
150 151 152 153 154 155 156 157
Lemma var_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R) (nlo:R) (nhi:R):
  (nlo <= cenv n <= nhi)%R ->
  eval_exp 0%R cenv (Var R n) nR ->
  eval_exp machineEpsilon cenv (Var R n) nF ->
  (Rabs (nR - nF) <= Rabs ((Rmax (Rabs nlo) (Rabs nhi)) * machineEpsilon))%R.
Proof.
  intros [lo_le_env env_le_hi] eval_real eval_float.
  inversion eval_real; subst.
Heiko Becker's avatar
Heiko Becker committed
158 159 160
  (* rewrite perturb_0_val. *)
Admitted.

161 162 163 164 165 166 167 168
(**
  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
169
 **)
170
Inductive bval (eps:R) (env:env_ty) : (bexp R) -> Prop -> Prop :=
171 172 173 174 175 176 177 178
  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).
179 180 181 182 183
(**
 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.