Environments.v 4.8 KB
Newer Older
1 2
(**
Environment library.
3 4
Defines the environment type for the Flover framework and a simulation relation
between environments.
5
 **)
6 7 8 9 10
From Coq
     Require Import Reals.Reals micromega.Psatz QArith.Qreals.

From Flover
     Require Import Infra.ExpressionAbbrevs Infra.RationalSimps Commands.
11 12 13 14 15

(**
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
16
exprression may yield different values for different machine epsilons
17 18
(or environments that already only approximate each other)
 **)
19 20
Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
                      -> NatSet.t -> env -> Prop :=
='s avatar
= committed
21 22
|approxRefl defVars A:
   approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv
23 24
|approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
   approxEnv E1 defVars A fVars dVars E2 ->
25
   (Rabs (v1 - v2) <= computeErrorR v1 m)%R ->
26
   NatSet.mem x (NatSet.union fVars dVars) = false ->
27 28 29
   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
30
|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m iv err:
31
   approxEnv E1 defVars A fVars dVars E2 ->
32
   FloverMap.find (Var Q x) A = Some (iv, err) ->
Heiko Becker's avatar
Heiko Becker committed
33
   (Rabs (v1 - v2) <= Q2R err)%R ->
34
   NatSet.mem x (NatSet.union fVars dVars) = false ->
35 36 37
   approxEnv (updEnv x v1 E1)
             (updDefVars x m defVars) A fVars (NatSet.add x dVars)
             (updEnv x v2 E2).
38

39 40
Section RelationProperties.

41 42
  Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType)
           (A:analysisResult) (fVars dVars: NatSet.t).
43 44 45

  Hypothesis approxEnvs: approxEnv E1 Gamma A fVars dVars E2.

46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
  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.
72

73
  Arguments mTypeToQ _ : simpl nomatch.
74

75 76 77 78 79
  Lemma approxEnv_fVar_bounded v2 m:
    E1 x = Some v ->
    E2 x = Some v2 ->
    NatSet.In x fVars ->
    Gamma x = Some m ->
80
    (Rabs (v - v2) <= computeErrorR v m)%R.
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
  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 *.
104
      apply IHa; auto.
105 106 107
      unfold updDefVars in x_typed;
        rewrite x_x0_neq in x_typed; auto.
  Qed.
108

109 110 111 112 113
  Lemma approxEnv_dVar_bounded v2 m iv e:
    E1 x = Some v ->
    E2 x = Some v2 ->
    NatSet.In x dVars ->
    Gamma x = Some m ->
114
    FloverMap.find (Var Q x) A = Some (iv, e) ->
115 116 117 118 119 120 121 122 123 124 125 126
    (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.
127
      apply IHa; auto.
128 129 130 131 132 133 134 135 136 137 138 139
    - 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.
140 141

End RelationProperties.