Environments.v 4.75 KB
Newer Older
1 2
(**
Environment library.
3
Defines the environment type for the Flover framework and a simulation relation between environments.
4
 **)
5
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
6
Require Import Flover.Infra.ExpressionAbbrevs Flover.Infra.RationalSimps Flover.Commands.
7 8 9 10 11 12 13 14

(**
Define an approximation relation between two environments.
We use this relation for the soundness proofs.
It is necessary to have this relation, since two evaluations of the very same
expression may yield different values for different machine epsilons
(or environments that already only approximate each other)
 **)
15
Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
='s avatar
= committed
16 17
|approxRefl defVars A:
   approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv
18 19
|approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
   approxEnv E1 defVars A fVars dVars E2 ->
20
   (Rabs (v1 - v2) <= (Rabs v1) * Q2R (mTypeToQ m))%R ->
21
   NatSet.mem x (NatSet.union fVars dVars) = false ->
22
   approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
Heiko Becker's avatar
Heiko Becker committed
23
|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m iv err:
24
   approxEnv E1 defVars A fVars dVars E2 ->
25
   FloverMap.find (Var Q x) A = Some (iv, err) ->
Heiko Becker's avatar
Heiko Becker committed
26
   (Rabs (v1 - v2) <= Q2R err)%R ->
27
   NatSet.mem x (NatSet.union fVars dVars) = false ->
28
   approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
29

30 31
Section RelationProperties.

32 33
  Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType)
           (A:analysisResult) (fVars dVars: NatSet.t).
34 35 36

  Hypothesis approxEnvs: approxEnv E1 Gamma A fVars dVars E2.

37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
  Lemma approxEnv_gives_value:
    E1 x = Some v ->
    NatSet.In x (NatSet.union fVars  dVars) ->
    exists v',
      E2 x = Some v'.
  Proof.
    induction approxEnvs;
      intros E1_def x_valid.
    - unfold emptyEnv in E1_def; simpl in E1_def. congruence.
    - unfold updEnv in *.
      case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
      + eexists; eauto.
      + eapply IHa; eauto.
        set_tac.
        destruct x_valid; set_tac.
        destruct H1 as [? | [? ?]]; subst; try auto.
        rewrite Nat.eqb_refl in eq_case; congruence.
    - unfold updEnv in *.
      case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
      + eexists; eauto.
      + eapply IHa; auto.
        set_tac.
        destruct x_valid; set_tac.
        destruct H2 as [? | [ ? ?]]; subst; try auto.
        rewrite Nat.eqb_refl in eq_case; congruence.
  Qed.
63

64
  Arguments mTypeToQ _ : simpl nomatch.
65

66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
  Lemma approxEnv_fVar_bounded v2 m:
    E1 x = Some v ->
    E2 x = Some v2 ->
    NatSet.In x fVars ->
    Gamma x = Some m ->
    (Rabs (v - v2) <= (Rabs v) * Q2R (mTypeToQ m))%R.
  Proof.
    induction approxEnvs;
      intros E1_def E2_def x_free x_typed.
    - unfold emptyEnv in *; simpl in *; congruence.
    - set_tac.
      destruct x_free as [x_x0 | [x_neq x_free]]; subst.
      + unfold updEnv in *;
          rewrite Nat.eqb_refl in *; simpl in *.
        unfold updDefVars in x_typed.
        rewrite Nat.eqb_refl in x_typed.
        inversion x_typed; subst.
        inversion E1_def; inversion E2_def; subst; auto.
      + unfold updEnv in *; simpl in *.
        rewrite <- Nat.eqb_neq in x_neq.
        rewrite x_neq in *; simpl in *.
        unfold updDefVars in x_typed; rewrite x_neq in x_typed.
        apply IHa; auto.
    - assert (x =? x0 = false) as x_x0_neq.
      { rewrite Nat.eqb_neq; hnf; intros; subst.
        set_tac.
        apply H1.
        set_tac. }
      unfold updEnv in *; rewrite x_x0_neq in *.
95
      apply IHa; auto.
96 97 98
      unfold updDefVars in x_typed;
        rewrite x_x0_neq in x_typed; auto.
  Qed.
99

100 101 102 103 104
  Lemma approxEnv_dVar_bounded v2 m iv e:
    E1 x = Some v ->
    E2 x = Some v2 ->
    NatSet.In x dVars ->
    Gamma x = Some m ->
105
    FloverMap.find (Var Q x) A = Some (iv, e) ->
106 107 108 109 110 111 112 113 114 115 116 117
    (Rabs (v - v2) <= Q2R e)%R.
  Proof.
    induction approxEnvs;
      intros E1_def E2_def x_def x_typed A_e; subst.
    - unfold emptyEnv in *; simpl in *; congruence.
    - assert (x =? x0 = false) as x_x0_neq.
      { rewrite Nat.eqb_neq; hnf; intros; subst.
        set_tac.
        apply H0; set_tac.
      }
      unfold updEnv in *; rewrite x_x0_neq in *.
      unfold updDefVars in x_typed; rewrite x_x0_neq in x_typed.
118
      apply IHa; auto.
119 120 121 122 123 124 125 126 127 128 129 130
    - set_tac.
      destruct x_def as [x_x0 | [x_neq x_def]]; subst.
      + unfold updEnv in *;
          rewrite Nat.eqb_refl in *; simpl in *.
        inversion E1_def; inversion E2_def; subst.
        rewrite A_e in *; inversion H; auto.
      + unfold updEnv in *; simpl in *.
        rewrite <- Nat.eqb_neq in x_neq.
        rewrite x_neq in *; simpl in *.
        unfold updDefVars in x_typed; rewrite x_neq in x_typed.
        apply IHa; auto.
  Qed.
131 132

End RelationProperties.