ExpressionSemantics.v 18.4 KB
 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 ``````From Coq Require Import Reals.Reals. From Flover.Infra Require Import RealRationalProps RationalSimps Ltacs. From Flover.Infra Require Export ExpressionAbbrevs. (** 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. **) Definition perturb (rVal:R) (m:mType) (delta:R) :R := match m with (* The Real-type has no error *) |REAL => rVal (* Fixed-point numbers have an absolute error *) |F w f => rVal + delta (* Floating-point numbers have a relative error *) | _ => rVal * (1 + delta) end. Hint Unfold perturb. (** Define expression evaluation relation parametric by an "error" epsilon. The result value exprresses float computations according to the IEEE standard, using a perturbation of the real valued computation by (1 + delta), where |delta| <= machine epsilon. **) Open Scope R_scope. Inductive eval_expr (E:env) (Gamma: expr R -> option mType) `````` Nikita Zyuzin committed Mar 15, 2019 37 `````` (DeltaMap: R -> mType -> option R) `````` Nikita Zyuzin committed Sep 19, 2018 38 39 `````` :(expr R) -> R -> mType -> Prop := | Var_load m x v: `````` 40 41 `````` Gamma (Var R x) = Some m -> E x = Some v -> `````` Nikita Zyuzin committed Nov 26, 2018 42 `````` eval_expr E Gamma DeltaMap (Var R x) v m `````` Nikita Zyuzin committed Mar 15, 2019 43 44 ``````| Const_dist m c delta: DeltaMap c m = Some delta -> `````` 45 `````` Rabs delta <= mTypeToR m -> `````` Nikita Zyuzin committed Mar 15, 2019 46 `````` eval_expr E Gamma DeltaMap (Const m c) (perturb c m delta) m `````` Nikita Zyuzin committed Sep 19, 2018 47 ``````| Unop_neg m mN f1 v1: `````` 48 49 `````` Gamma (Unop Neg f1) = Some mN -> isCompat m mN = true -> `````` Nikita Zyuzin committed Nov 26, 2018 50 51 `````` eval_expr E Gamma DeltaMap f1 v1 m -> eval_expr E Gamma DeltaMap (Unop Neg f1) (evalUnop Neg v1) mN `````` Nikita Zyuzin committed Sep 19, 2018 52 ``````| Unop_inv m mN f1 v1 delta: `````` 53 `````` Gamma (Unop Inv f1) = Some mN -> `````` Nikita Zyuzin committed Mar 15, 2019 54 `````` DeltaMap (evalUnop Inv v1) mN = Some delta -> `````` 55 56 `````` isCompat m mN = true -> Rabs delta <= mTypeToR mN -> `````` Nikita Zyuzin committed Nov 26, 2018 57 `````` eval_expr E Gamma DeltaMap f1 v1 m -> `````` 58 `````` (~ v1 = 0)%R -> `````` Nikita Zyuzin committed Nov 26, 2018 59 `````` eval_expr E Gamma DeltaMap (Unop Inv f1) (perturb (evalUnop Inv v1) mN delta) mN `````` Nikita Zyuzin committed Sep 19, 2018 60 ``````| Downcast_dist m m1 f1 v1 delta: `````` 61 `````` Gamma (Downcast m f1) = Some m -> `````` Nikita Zyuzin committed Mar 15, 2019 62 `````` DeltaMap v1 m = Some delta -> `````` 63 64 `````` isMorePrecise m1 m = true -> Rabs delta <= mTypeToR m -> `````` Nikita Zyuzin committed Nov 26, 2018 65 66 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> eval_expr E Gamma DeltaMap (Downcast m f1) (perturb v1 m delta) m `````` Nikita Zyuzin committed Sep 19, 2018 67 ``````| Binop_dist m1 m2 op f1 f2 v1 v2 delta m: `````` 68 `````` Gamma (Binop op f1 f2) = Some m -> `````` Nikita Zyuzin committed Mar 15, 2019 69 `````` DeltaMap (evalBinop op v1 v2) m = Some delta -> `````` 70 71 `````` isJoin m1 m2 m = true -> Rabs delta <= mTypeToR m -> `````` Nikita Zyuzin committed Nov 26, 2018 72 73 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> eval_expr E Gamma DeltaMap f2 v2 m2 -> `````` 74 `````` ((op = Div) -> (~ v2 = 0)%R) -> `````` Nikita Zyuzin committed Nov 26, 2018 75 `````` eval_expr E Gamma DeltaMap (Binop op f1 f2) (perturb (evalBinop op v1 v2) m delta) m `````` Nikita Zyuzin committed Sep 19, 2018 76 ``````| Fma_dist m1 m2 m3 m f1 f2 f3 v1 v2 v3 delta: `````` 77 `````` Gamma (Fma f1 f2 f3) = Some m -> `````` Nikita Zyuzin committed Mar 15, 2019 78 `````` DeltaMap (evalFma v1 v2 v3) m = Some delta -> `````` Heiko Becker committed Jul 27, 2018 79 `````` isJoin3 m1 m2 m3 m = true -> `````` 80 `````` Rabs delta <= mTypeToR m -> `````` Nikita Zyuzin committed Nov 26, 2018 81 82 83 84 85 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> eval_expr E Gamma DeltaMap f2 v2 m2 -> eval_expr E Gamma DeltaMap f3 v3 m3 -> eval_expr E Gamma DeltaMap (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m. `````` Nikita Zyuzin committed Mar 15, 2019 86 ``````Definition DeltaMapR: R -> mType -> option R := (fun x m => Some 0). `````` 87 88 89 90 91 92 93 94 `````` Close Scope R_scope. Hint Constructors eval_expr. (** *) (* Show some simpler (more general) rule lemmata *) (* **) `````` Nikita Zyuzin committed Mar 15, 2019 95 ``````Lemma Const_dist' DeltaMap m c delta v m' E Gamma: `````` 96 `````` Rle (Rabs delta) (mTypeToR m') -> `````` Nikita Zyuzin committed Mar 15, 2019 97 98 `````` DeltaMap c m = Some delta -> v = perturb c m delta -> `````` 99 `````` m' = m -> `````` Nikita Zyuzin committed Mar 15, 2019 100 `````` eval_expr E Gamma DeltaMap (Const m c) v m'. `````` 101 102 103 104 105 106 ``````Proof. intros; subst; auto. Qed. Hint Resolve Const_dist'. `````` Nikita Zyuzin committed Nov 26, 2018 107 108 ``````Lemma Unop_neg' DeltaMap m mN f1 v1 v m' E Gamma: eval_expr E Gamma DeltaMap f1 v1 m -> `````` 109 110 111 112 `````` v = evalUnop Neg v1 -> Gamma (Unop Neg f1) = Some mN -> isCompat m mN = true -> m' = mN -> `````` Nikita Zyuzin committed Nov 26, 2018 113 `````` eval_expr E Gamma DeltaMap (Unop Neg f1) v m'. `````` 114 115 116 117 118 119 ``````Proof. intros; subst; eauto. Qed. Hint Resolve Unop_neg'. `````` Nikita Zyuzin committed Nov 26, 2018 120 ``````Lemma Unop_inv' DeltaMap m mN f1 v1 delta v m' E Gamma: `````` 121 `````` Rle (Rabs delta) (mTypeToR m') -> `````` Nikita Zyuzin committed Nov 26, 2018 122 `````` eval_expr E Gamma DeltaMap f1 v1 m -> `````` Nikita Zyuzin committed Mar 15, 2019 123 `````` DeltaMap (evalUnop Inv v1) m' = Some delta -> `````` 124 125 126 127 128 `````` (~ v1 = 0)%R -> v = perturb (evalUnop Inv v1) mN delta -> Gamma (Unop Inv f1) = Some mN -> isCompat m mN = true -> m' = mN -> `````` Nikita Zyuzin committed Nov 26, 2018 129 `````` eval_expr E Gamma DeltaMap (Unop Inv f1) v m'. `````` 130 131 132 133 134 135 ``````Proof. intros; subst; eauto. Qed. Hint Resolve Unop_inv'. `````` Nikita Zyuzin committed Nov 26, 2018 136 ``````Lemma Downcast_dist' DeltaMap m m1 f1 v1 delta v m' E Gamma: `````` 137 138 `````` isMorePrecise m1 m = true -> Rle (Rabs delta) (mTypeToR m') -> `````` Nikita Zyuzin committed Nov 26, 2018 139 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> `````` Nikita Zyuzin committed Mar 15, 2019 140 `````` DeltaMap v1 m' = Some delta -> `````` 141 142 143 `````` v = (perturb v1 m delta) -> Gamma (Downcast m f1) = Some m -> m' = m -> `````` Nikita Zyuzin committed Nov 26, 2018 144 `````` eval_expr E Gamma DeltaMap (Downcast m f1) v m'. `````` 145 146 147 148 149 150 ``````Proof. intros; subst; eauto. Qed. Hint Resolve Downcast_dist'. `````` Nikita Zyuzin committed Nov 26, 2018 151 ``````Lemma Binop_dist' DeltaMap m1 m2 op f1 f2 v1 v2 delta v m m' E Gamma: `````` 152 `````` Rle (Rabs delta) (mTypeToR m') -> `````` Nikita Zyuzin committed Nov 26, 2018 153 154 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> eval_expr E Gamma DeltaMap f2 v2 m2 -> `````` Nikita Zyuzin committed Mar 15, 2019 155 `````` DeltaMap (evalBinop op v1 v2) m' = Some delta -> `````` 156 157 158 159 160 `````` ((op = Div) -> (~ v2 = 0)%R) -> v = perturb (evalBinop op v1 v2) m' delta -> Gamma (Binop op f1 f2) = Some m -> isJoin m1 m2 m = true -> m = m' -> `````` Nikita Zyuzin committed Nov 26, 2018 161 `````` eval_expr E Gamma DeltaMap (Binop op f1 f2) v m'. `````` 162 163 164 165 166 167 ``````Proof. intros; subst; eauto. Qed. Hint Resolve Binop_dist'. `````` Nikita Zyuzin committed Nov 26, 2018 168 ``````Lemma Fma_dist' DeltaMap m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma m: `````` 169 `````` Rle (Rabs delta) (mTypeToR m') -> `````` Nikita Zyuzin committed Nov 26, 2018 170 171 172 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> eval_expr E Gamma DeltaMap f2 v2 m2 -> eval_expr E Gamma DeltaMap f3 v3 m3 -> `````` Nikita Zyuzin committed Mar 15, 2019 173 `````` DeltaMap (evalFma v1 v2 v3) m' = Some delta -> `````` 174 175 `````` v = perturb (evalFma v1 v2 v3) m' delta -> Gamma (Fma f1 f2 f3) = Some m -> `````` Heiko Becker committed Jul 27, 2018 176 `````` isJoin3 m1 m2 m3 m = true -> `````` 177 `````` m = m' -> `````` Nikita Zyuzin committed Nov 26, 2018 178 `````` eval_expr E Gamma DeltaMap (Fma f1 f2 f3) v m'. `````` 179 180 181 182 183 184 ``````Proof. intros; subst; eauto. Qed. Hint Resolve Fma_dist'. `````` Nikita Zyuzin committed Nov 26, 2018 185 186 187 ``````Lemma Gamma_det e E1 E2 Gamma DeltaMap v1 v2 m1 m2: eval_expr E1 Gamma DeltaMap e v1 m1 -> eval_expr E2 Gamma DeltaMap e v2 m2 -> `````` Heiko Becker committed Jul 27, 2018 188 `````` m1 = m2. `````` Heiko Becker committed Jul 27, 2018 189 ``````Proof. `````` Heiko Becker committed Jul 27, 2018 190 191 192 193 194 195 196 197 `````` induction e; intros * eval_e1 eval_e2; inversion eval_e1; subst; inversion eval_e2; subst; try auto; match goal with | [H1: Gamma ?e = Some ?m1, H2: Gamma ?e = Some ?m2 |- _ ] => rewrite H1 in H2; inversion H2; subst end; auto. `````` Heiko Becker committed Jul 27, 2018 198 199 ``````Qed. `````` 200 ``````Lemma toRTMap_eval_REAL f: `````` Nikita Zyuzin committed Nov 26, 2018 201 `````` forall v E Gamma DeltaMap m, eval_expr E (toRTMap Gamma) DeltaMap (toREval f) v m -> m = REAL. `````` 202 ``````Proof. `````` Heiko Becker committed Jul 27, 2018 203 `````` induction f; intros * eval_f; inversion eval_f; subst. `````` 204 205 `````` repeat match goal with `````` Heiko Becker committed Jul 27, 2018 206 `````` | H: context[toRTMap _ _] |- _ => unfold toRTMap in H `````` 207 208 209 210 `````` | 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. `````` Heiko Becker committed Jul 27, 2018 211 `````` - auto. `````` Nikita Zyuzin committed Nov 26, 2018 212 `````` - rewrite (IHf _ _ _ _ _ H5) in H2. `````` Heiko Becker committed Jul 27, 2018 213 214 `````` unfold isCompat in H2. destruct m; type_conv; subst; try congruence; auto. `````` Nikita Zyuzin committed Nov 26, 2018 215 216 `````` - rewrite (IHf _ _ _ _ _ H5) in H3. unfold isCompat in H3. `````` Heiko Becker committed Jul 27, 2018 217 `````` destruct m; type_conv; subst; try congruence; auto. `````` Nikita Zyuzin committed Nov 26, 2018 218 219 220 `````` - rewrite (IHf1 _ _ _ _ _ H6) in H4. rewrite (IHf2 _ _ _ _ _ H9) in H4. unfold isJoin in H4; simpl in H4. `````` Heiko Becker committed Jul 27, 2018 221 `````` destruct m; try congruence; auto. `````` Nikita Zyuzin committed Nov 26, 2018 222 223 224 225 `````` - rewrite (IHf1 _ _ _ _ _ H6) in H4. rewrite (IHf2 _ _ _ _ _ H9) in H4. rewrite (IHf3 _ _ _ _ _ H10) in H4. unfold isJoin3 in H4; simpl in H4. `````` Heiko Becker committed Jul 27, 2018 226 227 `````` destruct m; try congruence; auto. - auto. `````` 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 ``````Qed. (** If |delta| <= 0 then perturb v delta is exactly v. **) Lemma delta_0_deterministic (v:R) m (delta:R): (Rabs delta <= 0)%R -> perturb v m delta = v. Proof. intros abs_0; apply Rabs_0_impl_eq in abs_0; subst. unfold perturb. destruct m; lra. Qed. (** Evaluation with 0 as machine epsilon is deterministic **) `````` Nikita Zyuzin committed Nov 26, 2018 244 ``````Lemma meps_0_deterministic (f:expr R) (E:env) Gamma DeltaMap: `````` 245 `````` forall v1 v2, `````` Nikita Zyuzin committed Nov 26, 2018 246 247 `````` eval_expr E (toRTMap Gamma) DeltaMap (toREval f) v1 REAL -> eval_expr E (toRTMap Gamma) DeltaMap (toREval f) v2 REAL -> `````` 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 `````` v1 = v2. Proof. induction f; intros v1 v2 ev1 ev2. - inversion ev1; inversion ev2; subst. rewrite H1 in H6. inversion H6; auto. - inversion ev1; inversion ev2; subst. simpl in *; subst; auto. - inversion ev1; inversion ev2; subst; try congruence. + rewrite (IHf v0 v3); [ auto | |]; destruct m, m0; cbn in *; congruence. + cbn in *. Flover_compute; rewrite (IHf v0 v3); [auto | | ]; destruct m, m0; cbn in *; congruence. - inversion ev1; inversion ev2; subst. `````` 263 264 265 266 `````` assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto). `````` 267 268 269 270 `````` subst. rewrite (IHf1 v0 v4); try auto. rewrite (IHf2 v3 v5); try auto. - inversion ev1; inversion ev2; subst. `````` 271 272 273 274 275 276 `````` assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m4 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m5 = REAL) by (eapply toRTMap_eval_REAL; eauto). `````` 277 278 279 280 281 `````` subst. rewrite (IHf1 v0 v5); try auto. rewrite (IHf2 v3 v6); try auto. rewrite (IHf3 v4 v7); try auto. - inversion ev1; inversion ev2; subst. `````` Nikita Zyuzin committed Nov 26, 2018 282 283 `````` apply REAL_least_precision in H3; apply REAL_least_precision in H11; subst. `````` 284 285 286 287 288 289 290 291 292 `````` rewrite (IHf v0 v3); try auto. Qed. (** Helping lemmas. Needed in soundness proof. For each evaluation of using an arbitrary epsilon, we can replace it by evaluating the subexprressions and then binding the result values to different variables in the Environment. **) `````` Nikita Zyuzin committed Nov 26, 2018 293 ``````Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 m Gamma DeltaMap delta: `````` 294 295 `````` (b = Div -> ~(v2 = 0 )%R) -> (Rabs delta <= mTypeToR m)%R -> `````` Nikita Zyuzin committed Mar 15, 2019 296 `````` DeltaMap (evalBinop b v1 v2) m = Some delta -> `````` Nikita Zyuzin committed Nov 26, 2018 297 298 299 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> eval_expr E Gamma DeltaMap f2 v2 m2 -> eval_expr E Gamma DeltaMap (Binop b f1 f2) (perturb (evalBinop b v1 v2) m delta) m -> `````` 300 301 `````` eval_expr (updEnv 2 v2 (updEnv 1 v1 emptyEnv)) (updDefVars (Binop b (Var R 1) (Var R 2)) m `````` Nikita Zyuzin committed Nov 26, 2018 302 `````` (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 Gamma))) `````` Nikita Zyuzin committed Mar 15, 2019 303 304 `````` (fun x _ => if Req_dec_sum x (evalBinop b v1 v2) then DeltaMap (evalBinop b v1 v2) m `````` Nikita Zyuzin committed Nov 27, 2018 305 `````` else None) `````` Nikita Zyuzin committed Nov 26, 2018 306 `````` (Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) m delta) m. `````` 307 ``````Proof. `````` Nikita Zyuzin committed Nov 26, 2018 308 `````` intros no_div_zero err_v delta_map eval_f1 eval_f2 eval_float. `````` 309 `````` inversion eval_float; subst. `````` Heiko Becker committed Jul 27, 2018 310 `````` rewrite H2 in *. `````` Heiko Becker committed Jul 27, 2018 311 312 `````` repeat (match goal with `````` Nikita Zyuzin committed Nov 26, 2018 313 314 `````` | [H1: eval_expr ?E ?Gamma ?DeltaMap ?f ?v1 ?m1, H2: eval_expr ?E ?Gamma ?DeltaMap ?f ?v2 ?m2 |- _] => `````` Heiko Becker committed Jul 27, 2018 315 316 317 318 `````` assert (m1 = m2) by (eapply Gamma_det; eauto); revert H1 H2 end); intros; subst. `````` Heiko Becker committed Jul 27, 2018 319 `````` eapply Binop_dist' with (v1:=v1) (v2:=v2) (delta:=delta); try eauto. `````` Heiko Becker committed Jul 27, 2018 320 321 `````` - eapply Var_load; eauto. - eapply Var_load; eauto. `````` Nikita Zyuzin committed Mar 15, 2019 322 323 `````` - destruct Req_dec_sum as [?|H]; auto. exfalso; now apply H. `````` Heiko Becker committed Jul 27, 2018 324 325 `````` - unfold updDefVars. unfold R_orderedExps.compare; rewrite R_orderedExps.exprCompare_refl; auto. `````` Heiko Becker committed Jul 27, 2018 326 ``````Qed. `````` 327 `````` `````` Nikita Zyuzin committed Nov 26, 2018 328 ``````Lemma fma_unfolding f1 f2 f3 E v1 v2 v3 m1 m2 m3 m Gamma DeltaMap delta: `````` 329 `````` (Rabs delta <= mTypeToR m)%R -> `````` Nikita Zyuzin committed Mar 15, 2019 330 `````` DeltaMap (evalFma v1 v2 v3) m = Some delta -> `````` Nikita Zyuzin committed Nov 26, 2018 331 332 333 334 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> eval_expr E Gamma DeltaMap f2 v2 m2 -> eval_expr E Gamma DeltaMap f3 v3 m3 -> eval_expr E Gamma DeltaMap (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m -> `````` 335 `````` eval_expr (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv))) `````` Heiko Becker committed Jul 27, 2018 336 `````` (updDefVars (Fma (Var R 1) (Var R 2) (Var R 3) ) m `````` Nikita Zyuzin committed Nov 26, 2018 337 338 `````` (updDefVars (Var R 3) m3 (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 Gamma)))) `````` Nikita Zyuzin committed Mar 15, 2019 339 340 `````` (fun x _ => if Req_dec_sum x (evalFma v1 v2 v3) then DeltaMap (evalFma v1 v2 v3) m `````` Nikita Zyuzin committed Nov 27, 2018 341 `````` else None) `````` Nikita Zyuzin committed Nov 26, 2018 342 `````` (Fma (Var R 1) (Var R 2) (Var R 3)) (perturb (evalFma v1 v2 v3) m delta) m. `````` 343 ``````Proof. `````` Nikita Zyuzin committed Nov 26, 2018 344 `````` intros err_v delta_map eval_f1 eval_f2 eval_f3 eval_float. `````` Heiko Becker committed Jul 27, 2018 345 346 347 `````` inversion eval_float; subst. repeat (match goal with `````` Nikita Zyuzin committed Nov 26, 2018 348 349 `````` | [H1: eval_expr ?E ?Gamma ?DeltaMap ?f ?v1 ?m1, H2: eval_expr ?E ?Gamma ?DeltaMap ?f ?v2 ?m2 |- _] => `````` Heiko Becker committed Jul 27, 2018 350 `````` assert (m1 = m2) `````` Heiko Becker committed Jul 27, 2018 351 `````` by (eapply Gamma_det; eauto); `````` Heiko Becker committed Jul 27, 2018 352 353 354 355 356 357 358 359 `````` revert H1 H2 end). intros; subst. rewrite H2. eapply Fma_dist' with (v1:=v1) (v2:=v2) (v3:=v3) (delta:=delta); try eauto. - eapply Var_load; eauto. - eapply Var_load; eauto. - eapply Var_load; eauto. `````` Nikita Zyuzin committed Mar 15, 2019 360 361 362 `````` - destruct Req_dec_sum as [? | Hneq]; auto. contradiction Hneq; auto. - now cbn. `````` Heiko Becker committed Jul 27, 2018 363 ``````Qed. `````` 364 365 `````` Lemma eval_eq_env e: `````` Nikita Zyuzin committed Nov 26, 2018 366 `````` forall E1 E2 Gamma DeltaMap v m, `````` 367 `````` (forall x, E1 x = E2 x) -> `````` Nikita Zyuzin committed Nov 26, 2018 368 369 `````` eval_expr E1 Gamma DeltaMap e v m -> eval_expr E2 Gamma DeltaMap e v m. `````` 370 371 ``````Proof. induction e; intros; `````` Nikita Zyuzin committed Nov 26, 2018 372 `````` (match_pat (eval_expr _ _ _ _ _ _) (fun H => inversion H; subst; simpl in H)); `````` 373 374 375 376 377 378 `````` try eauto. eapply Var_load; auto. rewrite <- (H n); auto. Qed. Lemma eval_expr_ignore_bind e: `````` Nikita Zyuzin committed Nov 26, 2018 379 380 `````` forall x v m Gamma DeltaMap E, eval_expr E Gamma DeltaMap e v m -> `````` 381 `````` ~ NatSet.In x (usedVars e) -> `````` Heiko Becker committed Aug 02, 2018 382 `````` forall v_new, `````` Nikita Zyuzin committed Nov 26, 2018 383 `````` eval_expr (updEnv x v_new E) Gamma DeltaMap e v m. `````` 384 385 386 387 388 389 390 391 ``````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. `````` Heiko Becker committed Jul 27, 2018 392 393 394 `````` cbn. apply beq_nat_false in H. destruct (n ?= x)%nat eqn:?; try auto. `````` 395 396 397 398 399 400 401 `````` + unfold updEnv. rewrite H; auto. - eapply Binop_dist'; eauto; [ eapply IHe1 | eapply IHe2]; eauto; hnf; intros; eapply no_usedVar; set_tac. `````` Heiko Becker committed Jul 27, 2018 402 `````` - eapply Fma_dist'; eauto; `````` 403 404 405 `````` [eapply IHe1 | eapply IHe2 | eapply IHe3]; eauto; hnf; intros; eapply no_usedVar; `````` Heiko Becker committed Jul 27, 2018 406 407 `````` set_tac. Qed. `````` 408 `````` `````` Nikita Zyuzin committed Nov 27, 2018 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 ``````Lemma eval_expr_det_ignore_bind2 e: forall x v v_new m Gamma E DeltaMap, eval_expr (updEnv x v_new E) Gamma DeltaMap e v m -> ~ NatSet.In x (usedVars e) -> eval_expr E Gamma DeltaMap e v m. 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. cbn. apply beq_nat_false in H. destruct (n ?= x)%nat eqn:?; try auto. + unfold updEnv. rewrite <- H1. unfold updEnv. now rewrite H. - 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. `````` Nikita Zyuzin committed Nov 26, 2018 441 ``````Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2 DeltaMap: `````` Heiko Becker committed Aug 16, 2018 442 `````` (forall e, Gamma1 e = Gamma2 e) -> `````` Nikita Zyuzin committed Nov 26, 2018 443 444 `````` eval_expr E Gamma1 DeltaMap e vR m -> eval_expr E Gamma2 DeltaMap e vR m. `````` Heiko Becker committed Jul 26, 2018 445 ``````Proof. `````` Nikita Zyuzin committed Nov 26, 2018 446 `````` revert E vR Gamma1 Gamma2 DeltaMap m; `````` Heiko Becker committed Jul 26, 2018 447 448 449 450 451 452 453 454 455 456 457 458 `````` induction e; intros * Gamma_eq eval_e; inversion eval_e; subst; simpl in *; [ eapply Var_load | eapply Const_dist' | eapply Unop_neg' | eapply Unop_inv' | eapply Binop_dist' | eapply Fma_dist' | eapply Downcast_dist' ]; try eauto; rewrite <- Gamma_eq; auto. Qed. `````` 459 460 461 462 463 464 ``````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 (R_orderedExps.compare x n); auto. `````` Nikita Zyuzin committed Nov 26, 2018 465 466 ``````Qed. `````` Nikita Zyuzin committed Nov 27, 2018 467 ``````Lemma eval_expr_functional E Gamma DeltaMap e v1 v2 m: `````` Nikita Zyuzin committed Nov 26, 2018 468 469 470 471 472 473 474 475 476 477 478 479 480 `````` eval_expr E Gamma DeltaMap e v1 m -> eval_expr E Gamma DeltaMap e v2 m -> v1 = v2. Proof. revert v1 v2 m. induction e; intros v1 v2 m__FP Heval1 Heval2. - inversion Heval1; inversion Heval2; subst. now replace v1 with v2 by congruence. - inversion Heval1; inversion Heval2; subst. now replace delta with delta0 by congruence. - destruct u; inversion Heval1; inversion Heval2; subst. + f_equal; eapply IHe; eauto. erewrite Gamma_det; eauto. `````` Nikita Zyuzin committed Mar 15, 2019 481 482 483 484 `````` + replace m0 with m in * by (eapply Gamma_det; eauto). replace v3 with v0 in * by (eapply IHe; eauto). replace delta with delta0 by congruence. reflexivity. `````` Nikita Zyuzin committed Nov 26, 2018 485 `````` - inversion Heval1; inversion Heval2; subst. `````` Nikita Zyuzin committed Mar 15, 2019 486 487 488 489 490 `````` replace m1 with m0 in * by (eapply Gamma_det; eauto). replace m3 with m2 in * by (eapply Gamma_det; eauto). replace v4 with v0 in * by (eapply IHe1; eauto). replace v5 with v3 in * by (eapply IHe2; eauto). now replace delta with delta0 by congruence. `````` Nikita Zyuzin committed Nov 26, 2018 491 `````` - inversion Heval1; inversion Heval2; subst. `````` Nikita Zyuzin committed Mar 15, 2019 492 493 494 495 496 497 498 `````` replace m1 with m0 in * by (eapply Gamma_det; eauto). replace m4 with m2 in * by (eapply Gamma_det; eauto). replace m5 with m3 in * by (eapply Gamma_det; eauto). replace v5 with v0 in * by (eapply IHe1; eauto). replace v6 with v3 in * by (eapply IHe2; eauto). replace v7 with v4 in * by (eapply IHe3; eauto). now replace delta with delta0 by congruence. `````` Nikita Zyuzin committed Nov 26, 2018 499 `````` - inversion Heval1; inversion Heval2; subst. `````` Nikita Zyuzin committed Mar 15, 2019 500 501 `````` replace m3 with m1 in * by (eapply Gamma_det; eauto). replace v3 with v0 in * by (eapply IHe; eauto). `````` Nikita Zyuzin committed Nov 26, 2018 502 `````` replace delta with delta0 by congruence. `````` Nikita Zyuzin committed Mar 15, 2019 503 `````` reflexivity. `````` Nikita Zyuzin committed Nov 26, 2018 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 ``````Qed. Lemma real_eval_expr_ignores_delta_map (f:expr R) (E:env) Gamma: forall v1 DeltaMap, eval_expr E (toRTMap Gamma) DeltaMap (toREval f) v1 REAL -> eval_expr E (toRTMap Gamma) DeltaMapR (toREval f) v1 REAL. Proof. induction f; unfold DeltaMapR; intros v1 DeltaMap ev1. - inversion ev1; subst. constructor; auto. - inversion ev1; subst. simpl in *; subst; auto. eapply Const_dist'; eauto. apply Rabs_0_impl_eq in H3; f_equal; now symmetry. - inversion ev1; subst; try congruence. + unfold isCompat in H2; destruct m; cbn in H2; try congruence; clear H2. specialize (IHf _ _ H5). eapply Unop_neg'; eauto. + unfold isCompat in H3; destruct m; cbn in H3; try congruence; clear H3. specialize (IHf _ _ H5). eapply Unop_inv'; eauto. apply Rabs_0_impl_eq in H4; f_equal; now symmetry. - inversion ev1; subst. assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto). subst. specialize (IHf1 _ _ H6). specialize (IHf2 _ _ H9). eapply Binop_dist'; eauto. apply Rabs_0_impl_eq in H5; f_equal; now symmetry. - inversion ev1; subst. assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto). assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto). subst. specialize (IHf1 _ _ H6). specialize (IHf2 _ _ H9). specialize (IHf3 _ _ H10). eapply Fma_dist'; eauto. apply Rabs_0_impl_eq in H5; f_equal; now symmetry. - inversion ev1; subst. apply REAL_least_precision in H3; subst. specialize (IHf _ _ H6). eapply Downcast_dist'; eauto. + trivial. + apply Rabs_0_impl_eq in H4; f_equal; now symmetry. Qed.``````