Expressions.v 16.1 KB
Newer Older
1
(**
2
  Formalization of the base expression language for the daisy framework
3
 **)
4 5 6 7 8 9
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith
               Coq.QArith.Qreals.
Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps
               Daisy.Infra.Ltacs.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet
        Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
10

11 12 13 14 15
(**
  Expressions will use binary operators.
  Define them first
**)
Inductive binop : Type := Plus | Sub | Mult | Div.
16

17
Definition binopEq (b1:binop) (b2:binop) :=
='s avatar
= committed
18 19 20 21 22 23
  match b1, b2 with
  | Plus, Plus => true
  | Sub,  Sub  => true
  | Mult, Mult => true
  | Div,  Div  => true
  | _,_ => false
24 25
  end.

26 27 28 29
(**
  Next define an evaluation function for binary operators on reals.
  Errors are added on the expression evaluation level later.
 **)
30
Definition evalBinop (o:binop) (v1:R) (v2:R) :=
31 32 33 34 35 36
  match o with
  | Plus => Rplus v1 v2
  | Sub => Rminus v1 v2
  | Mult => Rmult v1 v2
  | Div => Rdiv v1 v2
  end.
37

38 39
Lemma binopEq_refl b:
  binopEq b b = true.
40 41 42 43
Proof.
  case b; auto.
Qed.

44 45
Lemma binopEq_compat_eq b1 b2:
  binopEq b1 b2 = true <-> b1 = b2.
46
Proof.
47 48 49 50 51 52 53 54 55 56
  split; case b1; case b2; intros; simpl in *; congruence.
Qed.

Lemma binopEq_compat_eq_false b1 b2:
  binopEq b1 b2 = false <-> ~ (b1 = b2).
Proof.
  split; intros neq.
  - hnf; intros; subst. rewrite binopEq_refl in neq.
    congruence.
  - destruct b1; destruct b2; cbv; congruence.
57 58
Qed.

59 60 61 62 63 64
(**
   Expressions will use unary operators.
   Define them first
 **)
Inductive unop: Type := Neg | Inv.

65
Definition unopEq (o1:unop) (o2:unop) :=
='s avatar
= committed
66 67 68 69
  match o1, o2 with
  | Neg, Neg => true
  | Inv, Inv => true
  | _ , _ => false
70 71
  end.

72 73
Lemma unopEq_refl b:
  unopEq b b = true.
74 75 76 77
Proof.
  case b; auto.
Qed.

78 79
Lemma unopEq_compat_eq b1 b2:
  unopEq b1 b2 = true <-> b1 = b2.
80
Proof.
81
  split; case b1; case b2; intros; simpl in *; congruence.
82 83
Qed.

84 85
(**
   Define evaluation for unary operators on reals.
86
   Errors are added in the expression evaluation level later.
87
 **)
88
Definition evalUnop (o:unop) (v:R):=
89 90 91 92 93
  match o with
  |Neg => (- v)%R
  |Inv => (/ v)%R
  end .

Nikita Zyuzin's avatar
Nikita Zyuzin committed
94 95 96 97 98 99 100 101 102 103 104
(**
  Expressions will use ternary operators
  Define them first
**)
Inductive terop: Type := Fma.

Definition teropEq (o1: terop) (o2: terop) :=
  match o1, o2 with
  | Fma, Fma => true
  end.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
105 106
Lemma teropEq_refl t:
  teropEq t t = true.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
107
Proof.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
108
  now destruct t.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
109 110
Qed.

Nikita Zyuzin's avatar
Nikita Zyuzin committed
111 112
Lemma teropEq_compat_eq t1 t2:
  teropEq t1 t2 = true <-> t1 = t2.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
113
Proof.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
114
  now destruct t1, t2.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
115 116 117 118 119 120 121
Qed.

Definition evalTerop (o: terop) (v1: R) (v2: R) (v3: R) :=
  match o with
  | Fma => Rplus v1 (Rmult v2 v3)
  end.

122
(**
123 124
  Define expressions parametric over some value type V.
  Will ease reasoning about different instantiations later.
125
**)
126 127
Inductive exp (V:Type): Type :=
  Var: nat -> exp V
128
| Const: mType -> V -> exp V
129
| Unop: unop -> exp V -> exp V
130
| Binop: binop -> exp V -> exp V -> exp V
Nikita Zyuzin's avatar
Nikita Zyuzin committed
131
| Terop: terop -> exp V -> exp V -> exp V -> exp V
132
| Downcast: mType -> exp V -> exp V.
133

134 135 136 137
(**
  Boolean equality function on expressions.
  Used in certificates to define the analysis result as function
**)
138
Fixpoint expEq (e1:exp Q) (e2:exp Q) :=
='s avatar
= committed
139
  match e1, e2 with
140
  | Var _ v1, Var _ v2 => (v1 =? v2)
141 142 143 144 145 146
  | Const m1 n1, Const m2 n2 =>
    (mTypeEq m1 m2) && (Qeq_bool n1 n2)
  | Unop o1 e11, Unop o2 e22 =>
    (unopEq o1 o2) && (expEq e11 e22)
  | Binop o1 e11 e12, Binop o2 e21 e22 =>
    (binopEq o1 o2) && (expEq e11 e21) && (expEq e12 e22)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
147 148
  | Terop o1 e11 e12 e13, Terop o2 e21 e22 e23 =>
    (teropEq o1 o2) && (expEq e11 e21) && (expEq e12 e22) && (expEq e13 e23)
149 150
  | Downcast m1 f1, Downcast m2 f2 =>
    (mTypeEq m1 m2) && (expEq f1 f2)
='s avatar
= committed
151
  | _, _ => false
152 153
  end.

154 155
Lemma expEq_refl e:
  expEq e e = true.
156
Proof.
157
  induction e; try (apply andb_true_iff; split); simpl in *; auto .
158
  - symmetry; apply beq_nat_refl.
159
  - apply mTypeEq_refl.
160 161 162
  - apply Qeq_bool_iff; lra.
  - case u; auto.
  - case b; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
163
  - case t. firstorder.
164
  - apply mTypeEq_refl.
165
Qed.
166

167 168
Lemma expEq_sym e e':
  expEq e e' = expEq e' e.
169 170 171
Proof.
  revert e'.
  induction e; intros e'; destruct e'; simpl; try auto.
172
  - apply Nat.eqb_sym.
173
  - f_equal.
174
    + apply mTypeEq_sym; auto.
175 176 177 178
    + apply Qeq_bool_sym.
  - f_equal.
    + destruct u; auto.
    + apply IHe.
='s avatar
= committed
179
  - f_equal.
180
    + f_equal.
181
      * destruct b; auto.
182
      * apply IHe1.
183
    + apply IHe2.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
184 185 186 187 188
  - f_equal.
    + f_equal.
      * destruct t, t0. simpl. apply IHe1.
      * apply IHe2.
    + apply IHe3.
189
  - f_equal.
190
    + apply mTypeEq_sym; auto.
191 192 193
    + apply IHe.
Qed.

194 195 196 197
Lemma expEq_trans e f g:
  expEq e f = true ->
  expEq f g = true ->
  expEq e g = true.
='s avatar
= committed
198
Proof.
199
  revert e f g; induction e;
200 201 202 203 204 205
    destruct f; intros g eq1 eq2;
      destruct g; simpl in *; try congruence;
        try rewrite Nat.eqb_eq in *;
        subst; try auto.
  - andb_to_prop eq1;
      andb_to_prop eq2.
206 207
    rewrite mTypeEq_compat_eq in L, L0; subst.
    rewrite mTypeEq_refl; simpl.
208 209 210
    rewrite Qeq_bool_iff in *; lra.
  - andb_to_prop eq1;
      andb_to_prop eq2.
211 212
    rewrite unopEq_compat_eq in *; subst.
    rewrite unopEq_refl; simpl.
='s avatar
= committed
213
    eapply IHe; eauto.
214 215
  - andb_to_prop eq1;
      andb_to_prop eq2.
216 217
    rewrite binopEq_compat_eq in *; subst.
    rewrite binopEq_refl; simpl.
218 219
    apply andb_true_iff.
    split; [eapply IHe1; eauto | eapply IHe2; eauto].
Nikita Zyuzin's avatar
Nikita Zyuzin committed
220 221 222 223 224 225
  - andb_to_prop eq1;
      andb_to_prop eq2.
    rewrite teropEq_compat_eq in *; subst.
    rewrite teropEq_refl; simpl.
    rewrite andb_true_iff.
    rewrite andb_true_iff.
226
    split; [split; [eapply IHe1; eauto | eapply IHe2; eauto] | eapply IHe3; eauto].
227 228
  - andb_to_prop eq1;
      andb_to_prop eq2.
229 230
    rewrite mTypeEq_compat_eq in *; subst.
    rewrite mTypeEq_refl; simpl.
='s avatar
= committed
231 232 233
    eapply IHe; eauto.
Qed.

234 235
Fixpoint toRExp (e:exp Q) :=
  match e with
Nikita Zyuzin's avatar
Nikita Zyuzin committed
236 237 238 239 240 241
  | Var _ v => Var R v
  | Const m n => Const m (Q2R n)
  | Unop o e1 => Unop o (toRExp e1)
  | Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2)
  | Terop o e1 e2 e3 => Terop o (toRExp e1) (toRExp e2) (toRExp e3)
  | Downcast m e1 => Downcast m (toRExp e1)
242
  end.
243

244 245
Fixpoint toREval (e:exp R) :=
  match e with
246
  | Var _ v => Var R v
247
  | Const _ n => Const M0 n
248 249
  | Unop o e1 => Unop o (toREval e1)
  | Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
250
  | Terop o e1 e2 e3 => Terop o (toREval e1) (toREval e2) (toREval e3)
251
  | Downcast _ e1 =>   Downcast M0 (toREval e1)
252
  end.
253

254
Definition toRMap (d:nat -> option mType) (n:nat) :=
='s avatar
= committed
255 256 257
  match d n with
  | Some m => Some M0
  | None => None
258
  end.
259

260 261
Arguments toRMap _ _/.

262 263 264 265
(**
  Define a perturbation function to ease writing of basic definitions
**)
Definition perturb (r:R) (e:R) :=
266
  (r * (1 + e))%R.
Heiko Becker's avatar
Heiko Becker committed
267

268 269
Hint Unfold perturb.

270
(**
271
Define expression evaluation relation parametric by an "error" epsilon.
272 273 274
The result value expresses float computations according to the IEEE standard,
using a perturbation of the real valued computation by (1 + delta), where
|delta| <= machine epsilon.
275
**)
276
Inductive eval_exp (E:env) (Gamma: nat -> option mType) :(exp R) -> R -> mType -> Prop :=
277
| Var_load m x v:
278
    Gamma x = Some m ->
279
    E x = Some v ->
280
    eval_exp E Gamma (Var R x) v m
281
| Const_dist m n delta:
282 283
    Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
    eval_exp E Gamma (Const m n) (perturb n delta) m
284
| Unop_neg m f1 v1:
285 286
    eval_exp E Gamma f1 v1 m ->
    eval_exp E Gamma (Unop Neg f1) (evalUnop Neg v1) m
287
| Unop_inv m f1 v1 delta:
288 289 290 291
    Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
    eval_exp E Gamma  f1 v1 m ->
    (~ v1 = 0)%R  ->
    eval_exp E Gamma (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m
292
| Downcast_dist m m1 f1 v1 delta:
293
    (* Downcast expression f1 (evaluating to machine type m1), to a machine type m, less precise than m1.*)
294
    isMorePrecise m1 m = true ->
295 296 297
    Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
    eval_exp E Gamma f1 v1 m1 ->
    eval_exp E Gamma (Downcast m f1) (perturb v1 delta) m
298
| Binop_dist m1 m2 op f1 f2 v1 v2 delta:
299 300 301
    Rle (Rabs delta) (Q2R (mTypeToQ (join m1 m2))) ->
    eval_exp E Gamma f1 v1 m1 ->
    eval_exp E Gamma f2 v2 m2 ->
302
    ((op = Div) -> (~ v2 = 0)%R) ->
Nikita Zyuzin's avatar
Nikita Zyuzin committed
303 304 305 306 307 308 309 310 311
    eval_exp E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta)  (join m1 m2)
| Terop_dist m1 m2 m3 op f1 f2 f3 v1 v2 v3 delta:
    Rle (Rabs delta) (Q2R (mTypeToQ (join3 m1 m2 m3))) ->
    eval_exp E Gamma f1 v1 m1 ->
    eval_exp E Gamma f2 v2 m2 ->
    eval_exp E Gamma f3 v3 m3 ->
    eval_exp E Gamma (Terop op f1 f2 f3)
             (perturb (evalTerop op v1 v2 v3) delta)
             (join3 m1 m2 m3).
312 313 314 315

Hint Constructors eval_exp.

(**
316
  Show some simpler (more general) rule lemmata
317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332
**)
Lemma Const_dist' m n delta v m' E Gamma:
  Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
  v = perturb n delta ->
  m' = m ->
  eval_exp E Gamma (Const m n) v m'.
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Const_dist'.

Lemma Unop_neg' m f1 v1 v m' E Gamma:
  eval_exp E Gamma f1 v1 m ->
  v = evalUnop Neg v1 ->
  m' = m ->
333
  eval_exp E Gamma (Unop Neg f1) v m'.
334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Unop_neg'.

Lemma Unop_inv' m f1 v1 delta v m' E Gamma:
  Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
  eval_exp E Gamma  f1 v1 m ->
  (~ v1 = 0)%R  ->
  v = perturb (evalUnop Inv v1) delta ->
  m' = m ->
  eval_exp E Gamma (Unop Inv f1) v m'.
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Unop_inv'.

Lemma Downcast_dist' m m1 f1 v1 delta v m' E Gamma:
  isMorePrecise m1 m = true ->
  Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
  eval_exp E Gamma f1 v1 m1 ->
  v = (perturb v1 delta) ->
  m' = m ->
  eval_exp E Gamma (Downcast m f1) v m'.
Proof.
  intros; subst; eauto.
Qed.

Hint Resolve Downcast_dist'.

Lemma Binop_dist' m1 m2 op f1 f2 v1 v2 delta v m' E Gamma:
  Rle (Rabs delta) (Q2R (mTypeToQ m')) ->
  eval_exp E Gamma f1 v1 m1 ->
  eval_exp E Gamma f2 v2 m2 ->
  ((op = Div) -> (~ v2 = 0)%R) ->
  v = perturb (evalBinop op v1 v2) delta ->
  m' = join m1 m2 ->
  eval_exp E Gamma (Binop op f1 f2) v m'.
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Binop_dist'.
379

Nikita Zyuzin's avatar
Nikita Zyuzin committed
380 381 382 383 384 385 386 387 388 389 390 391 392 393
Lemma Terop_dist' m1 m2 m3 op f1 f2 f3 v1 v2 v3 delta v m' E Gamma:
  Rle (Rabs delta) (Q2R (mTypeToQ m')) ->
  eval_exp E Gamma f1 v1 m1 ->
  eval_exp E Gamma f2 v2 m2 ->
  eval_exp E Gamma f3 v3 m3 ->
  v = perturb (evalTerop op v1 v2 v3) delta ->
  m' = join3 m1 m2 m3 ->
  eval_exp E Gamma (Terop op f1 f2 f3) v m'.
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Terop_dist'.

394 395 396 397 398
(**
  Define the set of "used" variables of an expression to be the set of variables
  occuring in it
**)
Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
399 400
  match e with
  | Var _ x => NatSet.singleton x
401 402
  | Unop u e1 => usedVars e1
  | Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
403
  | Terop t e1 e2 e3 => NatSet.union (usedVars e1) (NatSet.union (usedVars e2) (usedVars e3))
404
  | Downcast _ e1 => usedVars e1
405 406
  | _ => NatSet.empty
  end.
407

408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426
Lemma toRMap_eval_M0 f v E Gamma m:
  eval_exp E (toRMap Gamma) (toREval f) v m -> m = M0.
Proof.
  revert v E Gamma m.
  induction f; intros * eval_f; inversion eval_f; subst;
  repeat
    match goal with
    | H: context[toRMap _ _] |- _ => unfold toRMap in H
    | H: context[match ?Gamma ?v with | _ => _ end ] |- _ => destruct (Gamma v) eqn:?
    | H: Some ?m1 = Some ?m2 |- _ => inversion H; try auto
    | H: None = Some ?m |- _ => inversion H
    end; try auto.
  - eapply IHf; eauto.
  - eapply IHf; eauto.
  - assert (m1 = M0)
      by (eapply IHf1; eauto).
    assert (m2 = M0)
      by (eapply IHf2; eauto);
      subst; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
427 428 429 430 431 432 433
  - assert (m1 = M0)
      by (eapply IHf1; eauto).
    assert (m2 = M0)
      by (eapply IHf2; eauto).
    assert (m3 = M0)
      by (eapply IHf3; eauto);
      subst; auto.
434 435
Qed.

436
(**
437
  If |delta| <= 0 then perturb v delta is exactly v.
438
**)
439
Lemma delta_0_deterministic (v:R) (delta:R):
Heiko Becker's avatar
Heiko Becker committed
440 441 442 443
  (Rabs delta <= 0)%R ->
  perturb v delta = v.
Proof.
  intros abs_0; apply Rabs_0_impl_eq in abs_0; subst.
444
  unfold perturb. lra.
Heiko Becker's avatar
Heiko Becker committed
445 446
Qed.

447
(**
448
Evaluation with 0 as machine epsilon is deterministic
449
**)
450
Lemma meps_0_deterministic (f:exp R) (E:env) Gamma:
451
  forall v1 v2,
452 453
  eval_exp E (toRMap Gamma) (toREval f) v1 M0 ->
  eval_exp E (toRMap Gamma) (toREval f) v2 M0 ->
454 455
  v1 = v2.
Proof.
456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471
  induction f;
    intros v1 v2 ev1 ev2.
  - inversion ev1; inversion ev2; subst.
    rewrite H1 in H6.
    inversion H6; auto.
  - inversion ev1; inversion ev2; subst.
    simpl in *.
    rewrite Q2R0_is_0 in *;
    repeat (rewrite delta_0_deterministic; try auto).
  - inversion ev1; inversion ev2; subst; try congruence.
    + rewrite (IHf v0 v3); eauto.
    + rewrite (IHf v0 v3); eauto.
      simpl in *.
      rewrite Q2R0_is_0 in *;
        repeat (rewrite delta_0_deterministic; try auto).
  - inversion ev1; inversion ev2; subst.
472 473 474 475 476
    assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m1 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m2 = M0) by (eapply toRMap_eval_M0; eauto).
    subst.
477 478 479 480 481
    rewrite (IHf1 v0 v4); try auto.
    rewrite (IHf2 v3 v5); try auto.
    simpl in *.
    rewrite Q2R0_is_0 in *.
    repeat (rewrite delta_0_deterministic; try auto).
Nikita Zyuzin's avatar
Nikita Zyuzin committed
482 483 484 485 486 487 488 489 490 491 492 493 494 495
  - inversion ev1; inversion ev2; subst.
    assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m1 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m2 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m4 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m5 = M0) by (eapply toRMap_eval_M0; eauto).
    subst.
    rewrite (IHf1 v0 v5); try auto.
    rewrite (IHf2 v3 v6); try auto.
    rewrite (IHf3 v4 v7); try auto.
    simpl in *.
    rewrite Q2R0_is_0 in *.
    repeat (rewrite delta_0_deterministic; try auto).
496 497 498 499 500 501 502
  - inversion ev1; inversion ev2; subst.
    apply M0_least_precision in H1;
      apply M0_least_precision in H7; subst.
    rewrite (IHf v0 v3); try auto.
    simpl in *.
    rewrite Q2R0_is_0 in *.
    repeat (rewrite delta_0_deterministic; try auto).
503 504
Qed.

505 506 507 508
(**
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
509
variables in the Environment.
510
 **)
511
Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 Gamma delta:
512
  (b = Div -> ~(v2 = 0 )%R) ->
513
  (Rabs delta <= Q2R (mTypeToQ (join m1 m2)))%R ->
514 515
  eval_exp E Gamma f1 v1 m1 ->
  eval_exp E Gamma f2 v2 m2 ->
516
  eval_exp E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2) ->
517 518
  eval_exp (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
           (updDefVars 2 m2 (updDefVars 1 m1 Gamma))
519
             (Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) delta) (join m1 m2).
520
Proof.
521 522
  intros no_div_zero eval_f1 eval_f2 eval_float.
  econstructor; try auto.
523 524
Qed.

Heiko Becker's avatar
Heiko Becker committed
525 526 527 528 529 530 531 532 533 534 535 536 537
Lemma eval_eq_env e:
  forall E1 E2 Gamma v m,
    (forall x, E1 x = E2 x) ->
    eval_exp E1 Gamma e v m ->
    eval_exp E2 Gamma e v m.
Proof.
  induction e; intros;
    (match_pat (eval_exp _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
    try eauto.
  eapply Var_load; auto.
  rewrite <- (H n); auto.
Qed.

538
(*
539 540 541
(**
Analogous lemma for unary expressions.
**)
542 543
Lemma unary_unfolding (e:exp R) (eps:R) (E:env) (v:R):
  (eval_exp eps E (Unop Inv e) v <->
544
   exists v1,
545 546
     eval_exp eps E e v1 /\
     eval_exp eps (updEnv 1 v1 E) (Unop Inv (Var R 1)) v).
547 548 549 550 551 552 553 554 555
Proof.
  split.
  - intros eval_un.
    inversion eval_un; subst.
    exists v1.
    repeat split; try auto.
    constructor; try auto.
    constructor; auto.
  - intros exists_val.
556 557
    destruct exists_val as [v1 [eval_f1 eval_e_E]].
    inversion eval_e_E; subst.
558 559 560
    inversion H1; subst.
    unfold updEnv in *; simpl in *.
    constructor; auto.
561
    inversion H3; subst; auto.
562
Qed. *)
563

564
(*   Using the parametric expressions, define boolean expressions for conditionals *)
565
(* **)
566 567 568
(* Inductive bexp (V:Type) : Type := *)
(*   leq: exp V -> exp V -> bexp V *)
(* | less: exp V -> exp V -> bexp V. *)
569

570
(**
571
  Define evaluation of boolean expressions
572
 **)
573 574 575 576 577 578 579 580 581 582 583 584 585
(* Inductive bval (E:env): (bexp R) -> Prop -> Prop := *)
(*   leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): *)
(*     eval_exp E f1 v1 -> *)
(*     eval_exp E f2 v2 -> *)
(*     bval E (leq f1 f2) (Rle v1 v2) *)
(* |less_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): *)
(*     eval_exp E f1 v1 -> *)
(*     eval_exp E f2 v2 -> *)
(*     bval E (less f1 f2) (Rlt v1 v2). *)
(* (** *)
(*  Simplify arithmetic later by making > >= only abbreviations *)
(* **) *)
(* Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1. *)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
586
(* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *)