ExpressionSemantics.v 17 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 Nov 26, 2018 37 `````` (DeltaMap: expr 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 Sep 19, 2018 43 ``````| Const_dist m n delta: `````` Nikita Zyuzin committed Nov 26, 2018 44 `````` DeltaMap (Const m n) m = Some delta -> `````` 45 `````` Rabs delta <= mTypeToR m -> `````` Nikita Zyuzin committed Nov 26, 2018 46 `````` eval_expr E Gamma DeltaMap (Const m n) (perturb n 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 Nov 26, 2018 54 `````` DeltaMap (Unop Inv f1) 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 Nov 26, 2018 62 `````` DeltaMap (Downcast m f1) 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 Nov 26, 2018 69 `````` DeltaMap (Binop op f1 f2) 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 Nov 26, 2018 78 `````` DeltaMap (Fma f1 f2 f3) 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 86 `````` 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. Definition DeltaMapR: expr 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 Nov 26, 2018 95 ``````Lemma Const_dist' DeltaMap m n delta v m' E Gamma: `````` 96 `````` Rle (Rabs delta) (mTypeToR m') -> `````` Nikita Zyuzin committed Nov 26, 2018 97 `````` DeltaMap (Const m n) m = Some delta -> `````` 98 99 `````` v = perturb n m delta -> m' = m -> `````` Nikita Zyuzin committed Nov 26, 2018 100 `````` eval_expr E Gamma DeltaMap (Const m n) 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 123 `````` eval_expr E Gamma DeltaMap f1 v1 m -> DeltaMap (Unop Inv f1) 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 140 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> DeltaMap (Downcast m f1) 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 155 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> eval_expr E Gamma DeltaMap f2 v2 m2 -> DeltaMap (Binop op f1 f2) 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 173 `````` eval_expr E Gamma DeltaMap f1 v1 m1 -> eval_expr E Gamma DeltaMap f2 v2 m2 -> eval_expr E Gamma DeltaMap f3 v3 m3 -> DeltaMap (Fma f1 f2 f3) 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 Nov 26, 2018 296 297 298 299 `````` DeltaMap (Binop b f1 f2) m = Some delta -> 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 303 304 305 `````` (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 Gamma))) (fun x m => if R_orderedExps.eq_dec x (Binop b (Var R 1) (Var R 2)) then Some delta else None) (Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) m delta) m. `````` 306 ``````Proof. `````` Nikita Zyuzin committed Nov 26, 2018 307 `````` intros no_div_zero err_v delta_map eval_f1 eval_f2 eval_float. `````` 308 `````` inversion eval_float; subst. `````` Heiko Becker committed Jul 27, 2018 309 `````` rewrite H2 in *. `````` Heiko Becker committed Jul 27, 2018 310 311 `````` repeat (match goal with `````` Nikita Zyuzin committed Nov 26, 2018 312 313 `````` | [H1: eval_expr ?E ?Gamma ?DeltaMap ?f ?v1 ?m1, H2: eval_expr ?E ?Gamma ?DeltaMap ?f ?v2 ?m2 |- _] => `````` Heiko Becker committed Jul 27, 2018 314 315 316 317 `````` assert (m1 = m2) by (eapply Gamma_det; eauto); revert H1 H2 end); intros; subst. `````` Heiko Becker committed Jul 27, 2018 318 `````` eapply Binop_dist' with (v1:=v1) (v2:=v2) (delta:=delta); try eauto. `````` Heiko Becker committed Jul 27, 2018 319 320 `````` - eapply Var_load; eauto. - eapply Var_load; eauto. `````` Nikita Zyuzin committed Nov 26, 2018 321 322 `````` - destruct R_orderedExps.eq_dec as [?|H]; auto. exfalso; apply H; apply R_orderedExps.eq_refl. `````` Heiko Becker committed Jul 27, 2018 323 324 `````` - unfold updDefVars. unfold R_orderedExps.compare; rewrite R_orderedExps.exprCompare_refl; auto. `````` Heiko Becker committed Jul 27, 2018 325 ``````Qed. `````` 326 `````` `````` Nikita Zyuzin committed Nov 26, 2018 327 ``````Lemma fma_unfolding f1 f2 f3 E v1 v2 v3 m1 m2 m3 m Gamma DeltaMap delta: `````` 328 `````` (Rabs delta <= mTypeToR m)%R -> `````` Nikita Zyuzin committed Nov 26, 2018 329 330 331 332 333 `````` DeltaMap (Fma f1 f2 f3) m = Some delta -> 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 -> `````` 334 `````` eval_expr (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv))) `````` Heiko Becker committed Jul 27, 2018 335 `````` (updDefVars (Fma (Var R 1) (Var R 2) (Var R 3) ) m `````` Nikita Zyuzin committed Nov 26, 2018 336 337 338 339 340 `````` (updDefVars (Var R 3) m3 (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 Gamma)))) (fun x m => if R_orderedExps.eq_dec x (Fma (Var R 1) (Var R 2) (Var R 3)) then Some delta else None) (Fma (Var R 1) (Var R 2) (Var R 3)) (perturb (evalFma v1 v2 v3) m delta) m. `````` 341 ``````Proof. `````` Nikita Zyuzin committed Nov 26, 2018 342 `````` intros err_v delta_map eval_f1 eval_f2 eval_f3 eval_float. `````` Heiko Becker committed Jul 27, 2018 343 344 345 `````` inversion eval_float; subst. repeat (match goal with `````` Nikita Zyuzin committed Nov 26, 2018 346 347 `````` | [H1: eval_expr ?E ?Gamma ?DeltaMap ?f ?v1 ?m1, H2: eval_expr ?E ?Gamma ?DeltaMap ?f ?v2 ?m2 |- _] => `````` Heiko Becker committed Jul 27, 2018 348 `````` assert (m1 = m2) `````` Heiko Becker committed Jul 27, 2018 349 `````` by (eapply Gamma_det; eauto); `````` Heiko Becker committed Jul 27, 2018 350 351 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. - cbn; auto. Qed. `````` 360 361 `````` Lemma eval_eq_env e: `````` Nikita Zyuzin committed Nov 26, 2018 362 `````` forall E1 E2 Gamma DeltaMap v m, `````` 363 `````` (forall x, E1 x = E2 x) -> `````` Nikita Zyuzin committed Nov 26, 2018 364 365 `````` eval_expr E1 Gamma DeltaMap e v m -> eval_expr E2 Gamma DeltaMap e v m. `````` 366 367 ``````Proof. induction e; intros; `````` Nikita Zyuzin committed Nov 26, 2018 368 `````` (match_pat (eval_expr _ _ _ _ _ _) (fun H => inversion H; subst; simpl in H)); `````` 369 370 371 372 373 374 `````` try eauto. eapply Var_load; auto. rewrite <- (H n); auto. Qed. Lemma eval_expr_ignore_bind e: `````` Nikita Zyuzin committed Nov 26, 2018 375 376 `````` forall x v m Gamma DeltaMap E, eval_expr E Gamma DeltaMap e v m -> `````` 377 `````` ~ NatSet.In x (usedVars e) -> `````` Heiko Becker committed Aug 02, 2018 378 `````` forall v_new, `````` Nikita Zyuzin committed Nov 26, 2018 379 `````` eval_expr (updEnv x v_new E) Gamma DeltaMap e v m. `````` 380 381 382 383 384 385 386 387 ``````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 388 389 390 `````` cbn. apply beq_nat_false in H. destruct (n ?= x)%nat eqn:?; try auto. `````` 391 392 393 394 395 396 397 `````` + 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 398 `````` - eapply Fma_dist'; eauto; `````` 399 400 401 `````` [eapply IHe1 | eapply IHe2 | eapply IHe3]; eauto; hnf; intros; eapply no_usedVar; `````` Heiko Becker committed Jul 27, 2018 402 403 `````` set_tac. Qed. `````` 404 `````` `````` Nikita Zyuzin committed Nov 26, 2018 405 ``````Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2 DeltaMap: `````` Heiko Becker committed Aug 16, 2018 406 `````` (forall e, Gamma1 e = Gamma2 e) -> `````` Nikita Zyuzin committed Nov 26, 2018 407 408 `````` eval_expr E Gamma1 DeltaMap e vR m -> eval_expr E Gamma2 DeltaMap e vR m. `````` Heiko Becker committed Jul 26, 2018 409 ``````Proof. `````` Nikita Zyuzin committed Nov 26, 2018 410 `````` revert E vR Gamma1 Gamma2 DeltaMap m; `````` Heiko Becker committed Jul 26, 2018 411 412 413 414 415 416 417 418 419 420 421 422 `````` 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. `````` 423 424 425 426 427 428 ``````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 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 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 ``````Qed. Lemma eval_expr_fixed_DeltaMap_functional E Gamma DeltaMap e v1 v2 m: 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. + replace delta with delta0 by congruence. f_equal; f_equal; eapply IHe; eauto. erewrite Gamma_det; eauto. - inversion Heval1; inversion Heval2; subst. replace delta with delta0 by congruence. f_equal; f_equal; [eapply IHe1 | eapply IHe2]; eauto; erewrite Gamma_det; eauto. - inversion Heval1; inversion Heval2; subst. replace delta with delta0 by congruence. f_equal; f_equal; [eapply IHe1 | eapply IHe2 | eapply IHe3]; eauto; erewrite Gamma_det; eauto. - inversion Heval1; inversion Heval2; subst. replace delta with delta0 by congruence. f_equal; f_equal; eapply IHe; eauto; erewrite Gamma_det; eauto. 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.``````