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

Heiko Becker's avatar
Heiko Becker committed
9 10 11 12

Module Q_orderedExps := ExpOrderedType (Q_as_OT).
Module legacy_OrderedQExps := Structures.OrdersAlt.Backport_OT (Q_orderedExps).

13 14
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
Module FloverMapFacts := OrdProperties (FloverMap).
Heiko Becker's avatar
Heiko Becker committed
15

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

Nikita Zyuzin's avatar
Nikita Zyuzin committed
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
Definition contained_flover_map V expmap1 expmap2 :=
  forall (e: exp Q) (v: V), FloverMap.find e expmap1 = Some v -> FloverMap.find e expmap2 = Some v.

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.
  destruct (Q_orderedExps.expCompare e e') eqn: Hcomp.
  - 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.

39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
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.
  destruct (Q_orderedExps.expCompare e e') eqn: Hcomp.
  - 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.

56 57 58 59
(**
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
**)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
60
(* Definition analysisResult :Type := exp Q -> intv * error. *)