ExpressionAbbrevs.v 15.9 KB
Newer Older
1
(**
2
  Some abbreviations that require having defined exprressions beforehand
3
  If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
4
**)
5 6
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QOrderedType Coq.FSets.FMapAVL Coq.FSets.FMapFacts Coq.Reals.ROrderedType Recdef.
Require Export Flover.Infra.Abbrevs Flover.AffineForm Flover.Expressions Flover.Infra.Ltacs Flover.OrderedExpressions.
Heiko Becker's avatar
Heiko Becker committed
7

8
Module Q_orderedExps := ExprOrderedType (Q_as_OT).
Heiko Becker's avatar
Heiko Becker committed
9 10
Module legacy_OrderedQExps := Structures.OrdersAlt.Backport_OT (Q_orderedExps).

11 12
Module R_orderedExps := ExprOrderedType (R_as_OT).

13 14 15 16 17 18 19 20 21
Functional Scheme exprCompare_ind := Induction for Q_orderedExps.exprCompare Sort Prop.

Lemma expr_compare_eq_eval_compat (e1 e2: expr Q):
  Q_orderedExps.exprCompare e1 e2 = Eq -> (toRExp e1) = (toRExp e2).
Proof.
  intros Heq.
  functional induction (Q_orderedExps.exprCompare e1 e2); simpl in Heq;
    try congruence; try (simpl; f_equal; auto); try (now rewrite <- mTypeEq_compat_eq);
      try now apply Nat.compare_eq.
22 23
  - rewrite <- Qeq_alt in Heq.
    now apply Qeq_eqR.
24 25
  - apply Ndec.Pcompare_Peqb in e6.
    apply Pos.eqb_eq in e6; subst.
26
    apply N.compare_eq in Heq; subst; auto.
27 28 29
  - simpl in e3.
    apply andb_false_iff in e3.
    apply Ndec.Pcompare_Peqb in e6.
30
    apply Pos.eqb_eq in e6; subst.
31 32
    apply N.compare_eq in Heq; subst; auto.
    rewrite N.eqb_refl, Pos.eqb_refl in e3.
33 34 35 36 37 38
    destruct e3; congruence.
  - unfold unopEq in e5.
    destruct u1, u2; congruence.
  - simpl in e5.
    apply andb_false_iff in e5.
    apply Ndec.Pcompare_Peqb in e8.
39
    rewrite Pos.eqb_eq in e8; subst.
40
    apply N.compare_eq in Heq; subst.
41 42 43 44
    destruct e5; congruence.
  - simpl in e5.
    apply andb_false_iff in e5.
    apply Ndec.Pcompare_Peqb in e8.
45
    rewrite Pos.eqb_eq in e8.
46 47
    apply N.compare_eq in Heq; subst.
    rewrite N.eqb_refl, Pos.eqb_refl in *.
48 49
    destruct e5; congruence.
Qed.
50

51 52
Lemma Qcompare_Rcompare q1 q2:
  Qcompare q1 q2 = Rcompare (Q2R q1) (Q2R q2).
53
Proof.
54
  destruct (Qcompare q1 q2) eqn:q_check.
55 56 57 58 59 60
  - rewrite <- Qeq_alt in q_check.
    apply Qeq_eqR in q_check.
    rewrite q_check in *.
    rewrite R_orderedExps.V_orderedFacts.compare_refl in *; auto.
  - rewrite <- Qlt_alt in q_check.
    apply Qlt_Rlt in q_check.
61
    symmetry.
62 63
    rewrite R_orderedExps.V_orderedFacts.compare_lt_iff; auto.
  - rewrite <- Qgt_alt in q_check.
64
    symmetry.
65 66 67 68 69 70 71 72 73 74
    rewrite R_orderedExps.V_orderedFacts.compare_gt_iff.
    auto using Qlt_Rlt.
Qed.

Lemma QcompareExp_RcompareExp e1 e2:
  Q_orderedExps.exprCompare e1 e2 = R_orderedExps.exprCompare (toRExp e1) (toRExp e2).
Proof.
  functional induction (Q_orderedExps.exprCompare e1 e2); simpl in *; try auto; try congruence;
    try rewrite e3;
  try rewrite <- IHc, e6; try auto.
75
  - destruct (Qcompare v1 v2) eqn:q_comp; rewrite Qcompare_Rcompare in q_comp; auto.
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
  - rewrite e6; auto.
  - rewrite e6; auto.
  - rewrite e6; auto.
  - rewrite e5, IHc; auto.
  - rewrite e5, e6; auto.
  - rewrite e5, e6; auto.
  - rewrite <- IHc, <- IHc0, e4, e3; auto.
  - rewrite <- IHc, e3, <- IHc0, e4; auto.
  - rewrite <- IHc, e3, <- IHc0, e4; auto.
  - rewrite <- IHc, e3; auto.
  - rewrite <- IHc, e3; auto.
  - rewrite <- IHc, e5; auto.
  - rewrite e5, e8; auto.
  - rewrite e5, e8; auto.
  - rewrite e5, e8; auto.
Qed.

93 94 95 96 97 98 99 100 101 102
(* Lemma QcompareExp_toREvalcompare e1 e2: *)
(*   Q_orderedExps.exprCompare e1 e2 = R_orderedExps.exprCompare (toREval (toRExp e1)) (toREval (toRExp e2)). *)
(* Proof. *)
(*   functional induction (Q_orderedExps.exprCompare e1 e2); *)
(*     try auto; try congruence. *)
(*   - rewrite Qcompare_Rcompare; auto. *)
(*   - simpl in *; congruence. *)
(*   - simpl in *; congruence. *)
(*   -  *)

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 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
Lemma usedVars_eq_compat e1 e2:
  Q_orderedExps.eq e1 e2 ->
  NatSet.eq (usedVars e1) (usedVars e2).
Proof.
  intros Heq.
  unfold Q_orderedExps.eq in Heq.
  functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
  - apply Nat.compare_eq in Heq.
    now rewrite Heq.
  - now set_tac.
  - simpl.
    reflexivity.
  - set_tac.
  - specialize (IHc e6).
    specialize (IHc0 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    simpl.
    now rewrite IHc, IHc0.
  - specialize (IHc e6).
    specialize (IHc0 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    simpl.
    now rewrite IHc, IHc0.
  - specialize (IHc e6).
    specialize (IHc0 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    simpl.
    now rewrite IHc, IHc0.
  - specialize (IHc e6).
    specialize (IHc0 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    simpl.
    now rewrite IHc, IHc0.
  - specialize (IHc e3).
    specialize (IHc0 e4).
    specialize (IHc1 Heq).
    apply NatSet.eq_leibniz in IHc.
    apply NatSet.eq_leibniz in IHc0.
    apply NatSet.eq_leibniz in IHc1.
    simpl.
    now rewrite IHc, IHc0, IHc1.
  - simpl.
    now apply IHc.
  - simpl in e5.
    rewrite andb_false_iff in e5.
    destruct e5.
    + apply Ndec.Pcompare_Peqb in e8.
      congruence.
    + apply N.compare_eq in Heq; subst.
      rewrite N.eqb_refl in H; congruence.
Qed.

Lemma usedVars_toREval_toRExp_compat e:
  usedVars (toREval (toRExp e)) = usedVars e.
Proof.
  induction e; simpl; set_tac.
  - now rewrite IHe1, IHe2.
  - now rewrite IHe1, IHe2, IHe3.
Qed.

167 168
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
Module FloverMapFacts := OrdProperties (FloverMap).
Heiko Becker's avatar
Heiko Becker committed
169

170
Definition analysisResult :Type := FloverMap.t (intv * error).
Nikita Zyuzin's avatar
Nikita Zyuzin committed
171
Definition expressionsAffine: Type := FloverMap.t (affine_form Q).
Heiko Becker's avatar
Heiko Becker committed
172

Nikita Zyuzin's avatar
Nikita Zyuzin committed
173
Definition contained_flover_map V expmap1 expmap2 :=
174
  forall (e: expr Q) (v: V), FloverMap.find e expmap1 = Some v -> FloverMap.find e expmap2 = Some v.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
175 176 177 178 179 180 181 182 183 184 185 186

Instance contained_flover_map_preorder (V: Type) : PreOrder (@contained_flover_map V).
Proof.
  constructor; unfold Reflexive, Transitive, contained_flover_map; eauto.
Qed.

Lemma contained_flover_map_extension V (expmap: FloverMap.t V) e v:
  FloverMap.find e expmap = None ->
  contained_flover_map expmap (FloverMap.add e v expmap).
Proof.
  intros Hnone e' v' Hcont.
  rewrite <- Hcont.
187
  destruct (Q_orderedExps.exprCompare e e') eqn: Hcomp.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
188 189 190 191 192
  - assert (FloverMap.find e expmap = FloverMap.find e' expmap) by (apply FloverMapFacts.P.F.find_o; auto); congruence.
  - apply FloverMapFacts.P.F.add_neq_o; congruence.
  - apply FloverMapFacts.P.F.add_neq_o; congruence.
Qed.

193 194 195 196 197 198
Lemma contained_flover_map_add_compat V (expmap1 expmap2: FloverMap.t V) e v:
  contained_flover_map expmap1 expmap2 ->
  contained_flover_map (FloverMap.add e v expmap1) (FloverMap.add e v expmap2).
Proof.
  unfold contained_flover_map.
  intros A e' v' B.
199
  destruct (Q_orderedExps.exprCompare e e') eqn: Hcomp.
200 201 202 203 204 205 206 207 208 209
  - rewrite FloverMapFacts.P.F.add_eq_o in B; auto.
    rewrite FloverMapFacts.P.F.add_eq_o; auto.
  - rewrite FloverMapFacts.P.F.add_neq_o in B; try congruence.
    rewrite FloverMapFacts.P.F.add_neq_o; try congruence.
    auto.
  - rewrite FloverMapFacts.P.F.add_neq_o in B; try congruence.
    rewrite FloverMapFacts.P.F.add_neq_o; try congruence.
    auto.
Qed.

210 211 212 213 214 215 216 217 218 219 220 221
Lemma contained_flover_map_none (V: Type) (e: expr Q) (expmap1: FloverMap.t V) expmap2:
  contained_flover_map expmap1 expmap2 ->
  FloverMap.find e expmap2 = None ->
  FloverMap.find e expmap1 = None.
Proof.
  intros cont Hfound1.
  unfold contained_flover_map in cont.
  destruct (FloverMap.find e expmap1) eqn: Heq; auto.
  apply cont in Heq.
  congruence.
Qed.

222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247
Lemma map_find_add e1 e2 m map1:
  FloverMap.find e1 (FloverMap.add e2 m map1) =
  match Q_orderedExps.compare e2 e1 with
  |Eq => Some m
  |_ => FloverMap.find (elt:=mType) e1 map1
  end.
Proof.
  rewrite FloverMapFacts.P.F.add_o.
  unfold FloverMapFacts.P.F.eq_dec.
  unfold Q_orderedExps.compare.
  destruct (Q_orderedExps.exprCompare e2 e1) eqn:?; congruence.
Qed.

Lemma map_mem_add e1 e2 m map1:
  FloverMap.mem e1 (FloverMap.add e2 m map1) =
  match Q_orderedExps.compare e2 e1 with
  |Eq => true
  | _ => FloverMap.mem (elt:=mType) e1 map1
  end.
Proof.
  rewrite FloverMapFacts.P.F.mem_find_b.
  rewrite map_find_add.
  destruct (Q_orderedExps.compare e2 e1) eqn:?; try auto;
    rewrite FloverMapFacts.P.F.mem_find_b; auto.
Qed.

248
Definition toRExpMap (tMap:FloverMap.t mType) : expr R -> option mType :=
249
  let elements := FloverMap.elements (elt:=mType) tMap in
250
  fun (e:expr R) =>
251 252 253 254 255
    olet p := findA
                (fun p => match R_orderedExps.compare e (toRExp p) with
                       | Eq => true |_ => false end)
                elements
      in
Heiko Becker's avatar
Heiko Becker committed
256
        Some p.
257

258 259 260 261 262 263 264 265 266 267 268
Definition toRTMap (Gamma:expr R -> option mType) :expr R -> option mType :=
  fun (e:expr R) =>
    match e with
    | Var _ _ =>
     match Gamma e with
     |Some m => Some REAL
     | _ => None
     end
    | _ => Some REAL
    end.

269 270 271 272 273 274 275
Definition updDefVars  (e:expr R) (m:mType) Gamma :=
  fun eNew =>
    match R_orderedExps.compare eNew e with
    |Eq => Some m
    |_ => Gamma eNew
    end.

276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301
Lemma findA_find A B (f:A -> bool) (l:list (A * B)) r:
  findA f l = Some r ->
  exists k,
  find (fun p => f (fst p)) l = Some (k,r) /\ f k = true.
Proof.
  induction l.
  - intros; simpl in *; congruence.
  - intros findA_top.
    simpl in *.
    destruct a; simpl in *.
    destruct (f a) eqn:?; try auto.
    exists a; split; congruence.
Qed.

Lemma find_swap A (f1:A -> bool) f2 l r:
  (forall k, f1 k = f2 k) ->
  find f1 l = Some r ->
  find f2 l = Some r.
Proof.
  induction l; intros f_eq find1; simpl in *; try congruence.
  destruct (f1 a) eqn:?.
  - rewrite <- f_eq; rewrite Heqb; congruence.
  - rewrite <- f_eq; rewrite Heqb.
    apply IHl; auto.
Qed.

Heiko Becker's avatar
Heiko Becker committed
302 303 304 305 306 307 308 309
Lemma findA_swap (A B:Type) (f1:A -> bool) f2 (l: list (A*B)) r:
  (forall k, f1 k = f2 k) ->
  findA f1 l = Some r ->
  findA f2 l = Some r.
Proof.
  induction l; intros f_eq find1; simpl in *; try congruence.
  destruct a.
  destruct (f1 a) eqn:?.
310
  - rewrite <- f_eq; rewrite Heqb0; auto.
Heiko Becker's avatar
Heiko Becker committed
311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
  - rewrite <- f_eq; rewrite Heqb0.
    apply IHl; auto.
Qed.

Lemma findA_swap2 (A B:Type) (f1:A -> bool) f2 (l: list (A*B)):
  (forall k, f1 k = f2 k) ->
  findA f1 l = findA f2 l.
Proof.
  induction l; intros f_eq; simpl in *; try congruence.
  destruct a.
  destruct (f1 a) eqn:?.
  - rewrite <- f_eq; rewrite Heqb0; congruence.
  - rewrite <- f_eq; rewrite Heqb0.
    apply IHl; auto.
Qed.

327
Lemma toRExpMap_some tMap e e2 m:
Heiko Becker's avatar
Heiko Becker committed
328
  e2 = toRExp e ->
329
  FloverMap.find e tMap = Some m ->
330
  toRExpMap tMap e2 = Some m.
331
Proof.
Heiko Becker's avatar
Heiko Becker committed
332
  intros ? find_Q; subst.
333
  rewrite  FloverMapFacts.P.F.elements_o in find_Q.
334
  unfold toRExpMap.
335
  unfold optionBind.
Heiko Becker's avatar
Heiko Becker committed
336 337 338 339 340 341 342 343 344
  erewrite <- findA_swap2 with (f1 := FloverMapFacts.P.F.eqb e).
  - rewrite find_Q; auto.
  - unfold R_orderedExps.compare.
    intros.
    rewrite <- QcompareExp_RcompareExp.
    unfold FloverMapFacts.P.F.eqb, FloverMapFacts.P.F.eq_dec.
    destruct (Q_orderedExps.exprCompare e k) eqn:q_comp; auto.
Qed.

345 346
Lemma toRExpMap_find_map tMap e m:
  toRExpMap tMap (toRExp e) = Some m ->
Heiko Becker's avatar
Heiko Becker committed
347 348 349
  FloverMap.find e tMap = Some m.
Proof.
  intros RTMap_def.
350
  unfold toRExpMap, optionBind in *.
Heiko Becker's avatar
Heiko Becker committed
351 352 353 354 355 356 357 358 359 360 361
  Flover_compute.
  inversion RTMap_def; subst.
  rewrite FloverMapFacts.P.F.elements_o.
  erewrite <- findA_swap2 with
      (f1 := fun p => match R_orderedExps.compare (toRExp e) (toRExp p) with
             |Eq => true |_ => false end); try auto.
  intros. unfold R_orderedExps.compare; rewrite <- QcompareExp_RcompareExp.
  unfold FloverMapFacts.P.F.eqb, FloverMapFacts.P.F.eq_dec.
  destruct (Q_orderedExps.exprCompare e k) eqn:q_comp; auto.
Qed.

362 363 364
Lemma toRExpMap_some_cases tMap e1 e2 m1 m2:
  toRExpMap (FloverMap.add e1 m1 tMap) (toRExp e2) = Some m2 ->
  (R_orderedExps.exprCompare (toRExp e1) (toRExp e2) = Eq /\ m1 = m2) \/ toRExpMap tMap (toRExp e2) = Some m2.
Heiko Becker's avatar
Heiko Becker committed
365 366
Proof.
  intros map_def.
367
  apply toRExpMap_find_map in map_def.
Heiko Becker's avatar
Heiko Becker committed
368 369 370 371
  rewrite FloverMapFacts.P.F.add_o in map_def.
  destruct (FloverMap.E.eq_dec e1 e2) eqn:?.
  - left. inversion map_def; split; try auto.
    rewrite <- QcompareExp_RcompareExp; auto.
372 373 374 375 376 377 378 379 380 381
  - right. eauto using toRExpMap_some.
Qed.

Lemma eqb_cmp_eq e1 e2:
  FloverMapFacts.P.F.eqb e1 e2 = match Q_orderedExps.exprCompare e1 e2 with
                                 | Eq => true
                                 | _ => false end.
Proof.
  unfold FloverMapFacts.P.F.eqb, FloverMapFacts.P.F.eq_dec.
  destruct (Q_orderedExps.exprCompare e1 e2) eqn:q_comp; auto.
382 383
Qed.

384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406
Lemma Q_compare_eq_Rcompare_eq e1 e2:
  Q_orderedExps.exprCompare e1 e2 = Eq ->
  R_orderedExps.exprCompare (toREval (toRExp e1)) (toREval (toRExp e2)) = Eq.
Proof.
  functional induction (Q_orderedExps.exprCompare e1 e2);
    simpl in *; try congruence;
      intros;
      try eauto.
  - rewrite <- Qcompare_Rcompare; auto.
  - apply Pos.compare_eq in e6; subst.
    apply N.compare_eq in H; subst.
    rewrite Pos.eqb_refl, N.eqb_refl in e3; simpl in *; congruence.
  - rewrite IHc, e5; auto.
  - rewrite IHc; auto.
  - rewrite IHc, IHc0; auto.
  - rewrite IHc, IHc0; auto.
  - rewrite IHc, IHc0; auto.
  - rewrite IHc, IHc0; auto.
  - apply Pos.compare_eq in e8; subst.
    apply N.compare_eq in H; subst.
    rewrite Pos.eqb_refl, N.eqb_refl in e5; simpl in *; congruence.
Qed.

407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466
Lemma no_cycle_unop e:
  forall u, Q_orderedExps.exprCompare e (Unop u e) <> Eq.
  induction e; intros *;  cbn in *; try congruence.
  destruct (unopEq u u0) eqn:?; try auto.
  destruct (unopEq u Neg); congruence.
Qed.

Lemma no_cycle_cast e:
  forall m, Q_orderedExps.exprCompare e (Downcast m e) <> Eq.
  induction e; intros *;  cbn in *; try congruence.
  destruct (mTypeEq m m0) eqn:?; try auto.
  destruct m; destruct m0; type_conv; try congruence;
    cbn; hnf; intros; try congruence.
  destruct (w ?= w0)%positive eqn:?; try congruence.
  apply Pos.compare_eq in Heqc.
  apply N.compare_eq in H; subst; congruence.
Qed.

Lemma no_cycle_binop_left e1:
  forall b e2, Q_orderedExps.exprCompare e1 (Binop b e1 e2) <> Eq.
  induction e1; intros *;  cbn in *; try congruence.
  pose (bOp := b);
    destruct b; destruct b0;
      try (hnf; intros; congruence);
          destruct (Q_orderedExps.exprCompare e1_1 (Binop bOp e1_1 e1_2)) eqn:case_comp;
                   subst bOp; rewrite case_comp in *;
          congruence.
Qed.

Lemma no_cycle_binop_right e2:
  forall b e1, Q_orderedExps.exprCompare e2 (Binop b e1 e2) <> Eq.
  induction e2; intros *;  cbn in *; try congruence.
  pose (bOp := b);
    destruct b; destruct b0;
      try (hnf; intros; congruence);
      destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; congruence.
Qed.

Lemma no_cycle_fma_left e1:
  forall e2 e3, Q_orderedExps.exprCompare e1 (Fma e1 e2 e3) <> Eq.
Proof.
  induction e1; intros *; cbn in *; try congruence;
    destruct (Q_orderedExps.exprCompare e1_1 (Fma e1_1 e1_2 e1_3)) eqn:?; congruence.
Qed.

Lemma no_cycle_fma_center e2:
  forall e1 e3, Q_orderedExps.exprCompare e2 (Fma e1 e2 e3) <> Eq.
Proof.
  induction e2; intros *; cbn in *; try congruence.
  destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; try congruence.
    destruct (Q_orderedExps.exprCompare e2_2 (Fma e2_1 e2_2 e2_3)) eqn:?; congruence.
Qed.

Lemma no_cycle_fma_right e3:
  forall e1 e2, Q_orderedExps.exprCompare e3 (Fma e1 e2 e3) <> Eq.
Proof.
  induction e3; intros *; cbn in *; try congruence.
  destruct (Q_orderedExps.exprCompare e3_1 e1) eqn:?; try congruence.
  destruct (Q_orderedExps.exprCompare e3_2 e2) eqn:?; try congruence.
Qed.
467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487
(*
Lemma toRExpMap_toRTMap e Gamma m:
  toRExpMap Gamma (toRExp e) = Some m ->
  toRTMap Gamma (toREval (toRExp e)) = Some REAL.
Proof.
  intros map_def.
  unfold toRTMap.
  apply toRExpMap_find_map in map_def.
  Flover_compute.
  rewrite FloverMapFacts.P.F.elements_o in map_def.
  erewrite findA_swap2 with
      (f2 := FloverMapFacts.P.F.eqb e) in Heqo; try congruence.
  intros. unfold R_orderedExps.compare.
  rewrite eqb_cmp_eq.
  clear map_def Heqo.
  destruct (Q_orderedExps.exprCompare e k) eqn:?.
  unfold FloverMapFacts.P.F.eqb, FloverMapFacts.P.F.eq_dec.
  rewrite <- QcompareExp_RcompareExp.
  destruct (Q_orderedExps.exprCompare e k) eqn:q_comp; auto.
*)

488
(**
489
We treat a function mapping an exprression arguing on fractions as value type
490 491
to pairs of intervals on rationals and rational errors as the analysis result
**)
492
(* Definition analysisResult :Type := expr Q -> intv * error. *)