Expressions.v 15.9 KB
Newer Older
1
(**
2
  Formalization of the base exprression language for the flover framework
3
 **)
4 5
From Flover
     Require Import Infra.RealRationalProps Infra.Ltacs.
6

7 8
From Flover
     Require Export Infra.Abbrevs Infra.NatSet Infra.MachineType.
9

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

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

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

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

43 44
Lemma binopEq_compat_eq b1 b2:
  binopEq b1 b2 = true <-> b1 = b2.
45
Proof.
46 47 48 49 50 51 52 53 54 55
  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.
56 57
Qed.

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

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

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

77 78 79 80 81 82
Lemma unopEq_sym u1 u2:
  unopEq u1 u2 = unopEq u2 u1.
Proof.
  destruct u1,u2; compute; auto.
Qed.

83 84
Lemma unopEq_compat_eq b1 b2:
  unopEq b1 b2 = true <-> b1 = b2.
85
Proof.
86
  split; case b1; case b2; intros; simpl in *; congruence.
87 88
Qed.

89 90
(**
   Define evaluation for unary operators on reals.
91
   Errors are added in the exprression evaluation level later.
92
 **)
93
Definition evalUnop (o:unop) (v:R):=
94 95 96 97 98
  match o with
  |Neg => (- v)%R
  |Inv => (/ v)%R
  end .

99
Definition evalFma (v1:R) (v2:R) (v3:R):=
Nikita Zyuzin's avatar
Nikita Zyuzin committed
100
  evalBinop Plus v1 (evalBinop Mult v2 v3).
Nikita Zyuzin's avatar
Nikita Zyuzin committed
101

102
(**
103
  Define exprressions parametric over some value type V.
104
  Will ease reasoning about different instantiations later.
105
**)
106 107 108 109 110 111 112
Inductive expr (V:Type): Type :=
  Var: nat -> expr V
| Const: mType -> V -> expr V
| Unop: unop -> expr V -> expr V
| Binop: binop -> expr V -> expr V -> expr V
| Fma: expr V -> expr V -> expr V -> expr V
| Downcast: mType -> expr V -> expr V.
113

114
Fixpoint toRExp (e:expr Q) :=
115
  match e with
Nikita Zyuzin's avatar
Nikita Zyuzin committed
116 117 118 119
  | 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)
120
  | Fma e1 e2 e3 => Fma (toRExp e1) (toRExp e2) (toRExp e3)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
121
  | Downcast m e1 => Downcast m (toRExp e1)
122
  end.
123

124
Fixpoint toREval (e:expr R) :=
125
  match e with
126
  | Var _ v => Var R v
127
  | Const _ n => Const REAL n
128 129
  | Unop o e1 => Unop o (toREval e1)
  | Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
130
  | Fma e1 e2 e3 => Fma (toREval e1) (toREval e2) (toREval e3)
131
  | Downcast _ e1 =>   Downcast REAL (toREval e1)
132
  end.
133

134
Definition toRMap (d:nat -> option mType) (n:nat) :=
='s avatar
= committed
135
  match d n with
136
  | Some m => Some REAL
='s avatar
= committed
137
  | None => None
138
  end.
139

140 141
Arguments toRMap _ _/.

142
(**
143 144 145 146
  Finally, define an error function that computes an errorneous value for a
  given type. For a fixed-point datatype, truncation is used and any
  floating-point type is perturbed. As we need not compute on this function we
  define it in Prop.
147
**)
148 149 150
Definition perturb (rVal:R) (m:mType) (delta:R) :R :=
  match m with
  (* The Real-type has no error *)
151
  |REAL => rVal
152 153 154 155 156
  (* Fixed-point numbers have an absolute error *)
  |F w f => rVal + delta
  (* Floating-point numbers have a relative error *)
  | _ => rVal * (1 + delta)
  end.
Heiko Becker's avatar
Heiko Becker committed
157

158 159
Hint Unfold perturb.

160
(**
161
Define expression evaluation relation parametric by an "error" epsilon.
162
The result value exprresses float computations according to the IEEE standard,
163 164
using a perturbation of the real valued computation by (1 + delta), where
|delta| <= machine epsilon.
165
**)
166
Open Scope R_scope.
167 168 169

Inductive eval_expr (E:env)
          (Gamma: nat -> option mType)
170
          (fBits:expr R -> option N)
171
  :(expr R) -> R -> mType -> Prop :=
172
| Var_load m x v:
173
    Gamma x = Some m ->
174
    E x = Some v ->
175
    eval_expr E Gamma fBits (Var R x) v m
176
| Const_dist m n delta:
177
    Rabs delta <= mTypeToR m ->
178
    eval_expr E Gamma fBits (Const m n) (perturb n m delta) m
179
| Unop_neg m f1 v1:
180 181
    eval_expr E Gamma fBits f1 v1 m ->
    eval_expr E Gamma fBits (Unop Neg f1) (evalUnop Neg v1) m
182
| Unop_inv m f1 v1 delta:
183
    Rabs delta <= mTypeToR m ->
184
    eval_expr E Gamma fBits  f1 v1 m ->
185
    (~ v1 = 0)%R  ->
186
    eval_expr E Gamma fBits (Unop Inv f1) (perturb (evalUnop Inv v1) m delta) m
187 188
| Downcast_dist m m1 f1 v1 delta:
    isMorePrecise m1 m = true ->
189
    Rabs delta <= mTypeToR m ->
190 191 192 193 194 195
    eval_expr E Gamma fBits f1 v1 m1 ->
    eval_expr E Gamma fBits (Downcast m f1) (perturb v1 m delta) m
| Binop_dist m1 m2 op f1 f2 v1 v2 fBit delta m:
    Rabs delta <= mTypeToR m ->
    eval_expr E Gamma fBits f1 v1 m1 ->
    eval_expr E Gamma fBits f2 v2 m2 ->
196
    ((op = Div) -> (~ v2 = 0)%R) ->
197 198 199 200 201 202 203 204 205 206 207 208
    (isFixedPoint m1 -> isFixedPoint m2 -> fBits (Binop op f1 f2) = Some fBit) ->
    join m1 m2 fBit = Some m ->
    eval_expr E Gamma fBits (Binop op f1 f2) (perturb (evalBinop op v1 v2) m delta) m
| Fma_dist m1 m2 m3 m f1 f2 f3 v1 v2 v3 fBit delta:
    Rabs delta <= mTypeToR m ->
    eval_expr E Gamma fBits f1 v1 m1 ->
    eval_expr E Gamma fBits f2 v2 m2 ->
    eval_expr E Gamma fBits f3 v3 m3 ->
    (isFixedPoint m1 -> isFixedPoint m2 ->
     isFixedPoint m3 -> fBits (Fma f1 f2 f3) = Some fBit) ->
    join3 m1 m2 m3 fBit = Some m ->
    eval_expr E Gamma fBits (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m.
209

210
Close Scope R_scope.
211

212
Hint Constructors eval_expr.
213

214 215 216
(** *)
(*   Show some simpler (more general) rule lemmata *)
(* **)
217
Lemma Const_dist' m n delta v m' E Gamma fBits:
218 219
  Rle (Rabs delta) (mTypeToR m') ->
  v = perturb n m delta ->
220
  m' = m ->
221
  eval_expr E Gamma fBits (Const m n) v m'.
222 223 224 225 226 227
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Const_dist'.

228 229
Lemma Unop_neg' m f1 v1 v m' E Gamma fBits:
  eval_expr E Gamma fBits f1 v1 m ->
230 231
  v = evalUnop Neg v1 ->
  m' = m ->
232
  eval_expr E Gamma fBits (Unop Neg f1) v m'.
233 234 235 236 237 238
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Unop_neg'.

239
Lemma Unop_inv' m f1 v1 delta v m' E Gamma fBits:
240
  Rle (Rabs delta) (mTypeToR m') ->
241
  eval_expr E Gamma fBits  f1 v1 m ->
242
  (~ v1 = 0)%R  ->
243
  v = perturb (evalUnop Inv v1) m delta ->
244
  m' = m ->
245
  eval_expr E Gamma fBits (Unop Inv f1) v m'.
246 247 248 249 250 251
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Unop_inv'.

252
Lemma Downcast_dist' m m1 f1 v1 delta v m' E Gamma fBits:
253
  isMorePrecise m1 m = true ->
254
  Rle (Rabs delta) (mTypeToR m') ->
255
  eval_expr E Gamma fBits f1 v1 m1 ->
256
  v = (perturb v1 m delta) ->
257
  m' = m ->
258
  eval_expr E Gamma fBits (Downcast m f1) v m'.
259 260 261 262 263 264
Proof.
  intros; subst; eauto.
Qed.

Hint Resolve Downcast_dist'.

265
Lemma Binop_dist' m1 m2 op f1 f2 v1 v2 delta v m' E Gamma fBits fBit:
266
  Rle (Rabs delta) (mTypeToR m') ->
267 268
  eval_expr E Gamma fBits f1 v1 m1 ->
  eval_expr E Gamma fBits f2 v2 m2 ->
269
  ((op = Div) -> (~ v2 = 0)%R) ->
270
  v = perturb (evalBinop op v1 v2) m' delta ->
271 272 273
  Some m' = join m1 m2 fBit ->
  (isFixedPoint m1 -> isFixedPoint m2 -> fBits (Binop op f1 f2) = Some fBit) ->
  eval_expr E Gamma fBits (Binop op f1 f2) v m'.
274
Proof.
275
  intros; subst; eauto.
276 277 278
Qed.

Hint Resolve Binop_dist'.
279

280
Lemma Fma_dist' m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma fBits fBit:
281
  Rle (Rabs delta) (mTypeToR m') ->
282 283 284
  eval_expr E Gamma fBits f1 v1 m1 ->
  eval_expr E Gamma fBits f2 v2 m2 ->
  eval_expr E Gamma fBits f3 v3 m3 ->
285
  v = perturb (evalFma v1 v2 v3) m' delta ->
286 287 288 289
  Some m' = join3 m1 m2 m3 fBit ->
  (isFixedPoint m1 -> isFixedPoint m2 ->
   isFixedPoint m3 -> fBits (Fma f1 f2 f3) = Some fBit) ->
  eval_expr E Gamma fBits (Fma f1 f2 f3) v m'.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
290
Proof.
291
  intros; subst; eauto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
292 293
Qed.

294
Hint Resolve Fma_dist'.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
295

296
(**
297
  Define the set of "used" variables of an exprression to be the set of variables
298 299
  occuring in it
**)
300
Fixpoint usedVars (V:Type) (e:expr V) :NatSet.t :=
301 302
  match e with
  | Var _ x => NatSet.singleton x
303 304
  | Unop u e1 => usedVars e1
  | Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
305
  | Fma e1 e2 e3 => NatSet.union (usedVars e1) (NatSet.union (usedVars e2) (usedVars e3))
306
  | Downcast _ e1 => usedVars e1
307 308
  | _ => NatSet.empty
  end.
309

310 311
Lemma toRMap_eval_REAL f v E Gamma fBits m:
  eval_expr E (toRMap Gamma) fBits (toREval f) v m -> m = REAL.
312
Proof.
313
  revert v E Gamma fBits m.
314 315 316 317 318 319 320 321 322 323
  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.
324
  - assert (m1 = REAL)
325
      by (eapply IHf1; eauto).
326
    assert (m2 = REAL)
327
      by (eapply IHf2; eauto);
328 329
      subst; eauto.
    cbn in *; congruence.
330
  - assert (m1 = REAL)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
331
      by (eapply IHf1; eauto).
332
    assert (m2 = REAL)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
333
      by (eapply IHf2; eauto).
334
    assert (m3 = REAL)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
335 336
      by (eapply IHf3; eauto);
      subst; auto.
337
    cbn in *; congruence.
338 339
Qed.

340
(**
341
  If |delta| <= 0 then perturb v delta is exactly v.
342
**)
343
Lemma delta_0_deterministic (v:R) m (delta:R):
Heiko Becker's avatar
Heiko Becker committed
344
  (Rabs delta <= 0)%R ->
345
  perturb v m delta = v.
Heiko Becker's avatar
Heiko Becker committed
346 347
Proof.
  intros abs_0; apply Rabs_0_impl_eq in abs_0; subst.
348
  unfold perturb. destruct m; lra.
Heiko Becker's avatar
Heiko Becker committed
349 350
Qed.

351
(**
352
Evaluation with 0 as machine epsilon is deterministic
353
**)
354
Lemma meps_0_deterministic (f:expr R) (E:env) Gamma fBits:
355
  forall v1 v2,
356 357
  eval_expr E (toRMap Gamma) fBits (toREval f) v1 REAL ->
  eval_expr E (toRMap Gamma) fBits (toREval f) v2 REAL ->
358 359
  v1 = v2.
Proof.
360 361 362 363 364 365
  induction f;
    intros v1 v2 ev1 ev2.
  - inversion ev1; inversion ev2; subst.
    rewrite H1 in H6.
    inversion H6; auto.
  - inversion ev1; inversion ev2; subst.
366
    simpl in *; subst; auto.
367 368
  - inversion ev1; inversion ev2; subst; try congruence.
    + rewrite (IHf v0 v3); eauto.
369
    + cbn in H1, H8. subst. rewrite (IHf v0 v3); eauto.
370
  - inversion ev1; inversion ev2; subst.
371 372 373 374
    assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
    assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
    assert (m1 = REAL) by (eapply toRMap_eval_REAL; eauto).
    assert (m2 = REAL) by (eapply toRMap_eval_REAL; eauto).
375
    subst.
376 377
    rewrite (IHf1 v0 v4); try auto.
    rewrite (IHf2 v3 v5); try auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
378
  - inversion ev1; inversion ev2; subst.
379 380 381 382 383 384
    assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
    assert (m1 = REAL) by (eapply toRMap_eval_REAL; eauto).
    assert (m2 = REAL) by (eapply toRMap_eval_REAL; eauto).
    assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
    assert (m4 = REAL) by (eapply toRMap_eval_REAL; eauto).
    assert (m5 = REAL) by (eapply toRMap_eval_REAL; eauto).
Nikita Zyuzin's avatar
Nikita Zyuzin committed
385 386 387 388
    subst.
    rewrite (IHf1 v0 v5); try auto.
    rewrite (IHf2 v3 v6); try auto.
    rewrite (IHf3 v4 v7); try auto.
389
  - inversion ev1; inversion ev2; subst.
390 391
    apply REAL_least_precision in H1;
      apply REAL_least_precision in H7; subst.
392
    rewrite (IHf v0 v3); try auto.
393 394
Qed.

395
(**
Nikita Zyuzin's avatar
Nikita Zyuzin committed
396
Helping lemmas. Needed in soundness proof.
397
For each evaluation of using an arbitrary epsilon, we can replace it by
398
evaluating the subexprressions and then binding the result values to different
399
variables in the Environment.
400
 **)
401
Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 m Gamma fBits fBit delta:
402
  (b = Div -> ~(v2 = 0 )%R) ->
403 404 405 406 407 408
  (isFixedPoint m1 -> isFixedPoint m2 -> fBits (Binop b f1 f2) = Some fBit) ->
  (join m1 m2 fBit = Some m) ->
  (Rabs delta <= mTypeToR m)%R ->
  eval_expr E Gamma fBits f1 v1 m1 ->
  eval_expr E Gamma fBits f2 v2 m2 ->
  eval_expr E Gamma fBits (Binop b f1 f2) (perturb (evalBinop b v1 v2) m delta) m ->
409
  eval_expr (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
410
           (updDefVars 2 m2 (updDefVars 1 m1 Gamma))
411 412 413 414 415 416
           (fun e =>
              match e with
              | Binop b (Var _ 1) (Var _ 2) => fBits (Binop b f1 f2)
              | _ => fBits e
           end)
             (Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) m delta) m.
417
Proof.
418
  intros no_div_zero eval_f1 eval_f2 eval_float.
419 420 421
  econstructor; try eauto.
  - eapply Var_load; cbn; auto.
  - eapply Var_load; cbn; auto.
422 423
Qed.

424 425 426 427 428 429 430 431 432
Lemma fma_unfolding f1 f2 f3 E v1 v2 v3 m1 m2 m3 m Gamma fBits fBit delta:
  (isFixedPoint m1 -> isFixedPoint m2 ->
   isFixedPoint m3 -> fBits (Fma f1 f2 f3) = Some fBit) ->
  Some m = join3 m1 m2 m3 fBit ->
  (Rabs delta <= mTypeToR m)%R ->
  eval_expr E Gamma fBits f1 v1 m1 ->
  eval_expr E Gamma fBits f2 v2 m2 ->
  eval_expr E Gamma fBits f3 v3 m3 ->
  eval_expr E Gamma fBits (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m ->
433
  eval_expr (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
Nikita Zyuzin's avatar
Nikita Zyuzin committed
434
           (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 Gamma)))
435 436 437 438 439 440
           (fun e =>
              match e with
              | Fma (Var _ 1) (Var _ 2) (Var _ 3) => fBits (Fma f1 f2 f3)
              | _ => fBits e
           end)
             (Fma (Var R 1) (Var R 2) (Var R 3)) (perturb (evalFma v1 v2 v3) m delta) m.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
441
Proof.
442 443
  econstructor; try eauto;
    eapply Var_load; cbn; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
444 445
Qed.

Heiko Becker's avatar
Heiko Becker committed
446
Lemma eval_eq_env e:
447
  forall E1 E2 Gamma fBits v m,
Heiko Becker's avatar
Heiko Becker committed
448
    (forall x, E1 x = E2 x) ->
449 450
    eval_expr E1 Gamma fBits e v m ->
    eval_expr E2 Gamma fBits e v m.
Heiko Becker's avatar
Heiko Becker committed
451 452
Proof.
  induction e; intros;
453
    (match_pat (eval_expr _ _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
Heiko Becker's avatar
Heiko Becker committed
454 455 456 457 458
    try eauto.
  eapply Var_load; auto.
  rewrite <- (H n); auto.
Qed.

459
Lemma eval_expr_ignore_bind e:
460 461
  forall x v m Gamma E fBits,
    eval_expr E Gamma fBits e v m ->
462 463
    ~ NatSet.In x (usedVars e) ->
    forall m_new v_new,
464
    eval_expr (updEnv x v_new E) (updDefVars x m_new Gamma) fBits e v m.
465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
Proof.
  induction e; intros * eval_e no_usedVar *; cbn in *;
    inversion eval_e; subst; try eauto.
  - assert (n <> x).
    { hnf. intros. subst. apply no_usedVar; set_tac. }
    rewrite <- Nat.eqb_neq in H.
    eapply Var_load.
    + unfold updDefVars.
      rewrite H; auto.
    + unfold updEnv.
      rewrite H; auto.
  - eapply Binop_dist'; eauto;
      [ eapply IHe1 | eapply IHe2];
      eauto;
      hnf; intros; eapply no_usedVar;
      set_tac.
  - eapply Fma_dist'; eauto;
      [eapply IHe1 | eapply IHe2 | eapply IHe3];
      eauto;
      hnf; intros; eapply no_usedVar;
        set_tac.
Qed.
487 488 489 490 491 492 493 494

Lemma Rmap_updVars_comm Gamma n m:
  forall x,
    updDefVars n REAL (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x.
Proof.
  unfold updDefVars, toRMap; simpl.
  intros x; destruct (x =? n); try auto.
Qed.
495
(*
496 497 498
(**
Analogous lemma for unary expressions.
**)
499 500
Lemma unary_unfolding (e:expr R) (eps:R) (E:env) (v:R):
  (eval_expr eps E (Unop Inv e) v <->
501
   exists v1,
502 503
     eval_expr eps E e v1 /\
     eval_expr eps (updEnv 1 v1 E) (Unop Inv (Var R 1)) v).
504 505 506 507 508 509 510 511 512
Proof.
  split.
  - intros eval_un.
    inversion eval_un; subst.
    exists v1.
    repeat split; try auto.
    constructor; try auto.
    constructor; auto.
  - intros exists_val.
513 514
    destruct exists_val as [v1 [eval_f1 eval_e_E]].
    inversion eval_e_E; subst.
515 516 517
    inversion H1; subst.
    unfold updEnv in *; simpl in *.
    constructor; auto.
518
    inversion H3; subst; auto.
519
Qed. *)
520

521
(*   Using the parametric exprressions, define boolean exprressions for conditionals *)
522
(* **)
523 524 525
(* Inductive bexpr (V:Type) : Type := *)
(*   leq: expr V -> expr V -> bexpr V *)
(* | less: expr V -> expr V -> bexpr V. *)
526

527
(**
528
  Define evaluation of boolean exprressions
529
 **)
530 531 532 533
(* Inductive bval (E:env): (bexpr R) -> Prop -> Prop := *)
(*   leq_eval (f1:expr R) (f2:expr R) (v1:R) (v2:R): *)
(*     eval_expr E f1 v1 -> *)
(*     eval_expr E f2 v2 -> *)
534
(*     bval E (leq f1 f2) (Rle v1 v2) *)
535 536 537
(* |less_eval (f1:expr R) (f2:expr R) (v1:R) (v2:R): *)
(*     eval_expr E f1 v1 -> *)
(*     eval_expr E f2 v2 -> *)
538 539 540 541
(*     bval E (less f1 f2) (Rlt v1 v2). *)
(* (** *)
(*  Simplify arithmetic later by making > >= only abbreviations *)
(* **) *)
542 543
(* Definition gr := fun (V:Type) (f1: expr V) (f2: expr V) => less f2 f1. *)
(* Definition greq := fun (V:Type) (f1:expr V) (f2: expr V) => leq f2 f1. *)