Commit 2fe03457 authored by Heiko Becker's avatar Heiko Becker

Fix admits in ExpressionSemantics.v

parent 5d673f75
......@@ -71,8 +71,7 @@ Inductive eval_expr (E:env)
eval_expr E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) m delta) m
| Fma_dist m1 m2 m3 m f1 f2 f3 v1 v2 v3 delta:
Gamma (Fma f1 f2 f3) = Some m ->
isJoin m1 m2 m = true ->
isJoin m2 m3 m = true ->
isJoin3 m1 m2 m3 m = true ->
Rabs delta <= mTypeToR m ->
eval_expr E Gamma f1 v1 m1 ->
eval_expr E Gamma f2 v2 m2 ->
......@@ -163,8 +162,7 @@ Lemma Fma_dist' m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma m:
eval_expr E Gamma f3 v3 m3 ->
v = perturb (evalFma v1 v2 v3) m' delta ->
Gamma (Fma f1 f2 f3) = Some m ->
isJoin m1 m2 m = true ->
isJoin m2 m3 m = true ->
isJoin3 m1 m2 m3 m = true ->
m = m' ->
eval_expr E Gamma (Fma f1 f2 f3) v m'.
Proof.
......@@ -173,6 +171,13 @@ Qed.
Hint Resolve Fma_dist'.
Lemma Gamma_def e E Gamma v m:
eval_expr E Gamma e v m ->
Gamma e = Some m.
Proof.
destruct e; intros * eval_e; inversion eval_e; subst; auto.
Qed.
Lemma toRMap_eval_REAL f:
forall v E Gamma m, eval_expr E (toRMap Gamma) (toREval f) v m -> m = REAL.
Proof.
......@@ -262,14 +267,15 @@ Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 m Gamma delta:
Proof.
intros no_div_zero err_v eval_f1 eval_f2 eval_float.
inversion eval_float; subst.
econstructor; try eauto.
- unfold updDefVars; simpl.
destruct b; auto.
- eapply Var_load; cbn; auto.
admit. admit.
- eapply Var_load; cbn; auto.
admit. admit.
Admitted.
rewrite H2 in *.
eapply Gamma_def in eval_f1; eapply Gamma_def in H6.
rewrite H6 in eval_f1; inversion eval_f1; subst.
eapply Gamma_def in eval_f2; eapply Gamma_def in H8;
rewrite H8 in eval_f2; inversion eval_f2; subst.
eapply Binop_dist' with (v1:=v1) (v2:=v2) (delta:=delta); try eauto.
unfold updDefVars.
unfold R_orderedExps.compare; rewrite R_orderedExps.exprCompare_refl; auto.
Qed.
Lemma fma_unfolding f1 f2 f3 E v1 v2 v3 m1 m2 m3 m Gamma delta:
(Rabs delta <= mTypeToR m)%R ->
......@@ -278,16 +284,29 @@ Lemma fma_unfolding f1 f2 f3 E v1 v2 v3 m1 m2 m3 m Gamma delta:
eval_expr E Gamma f3 v3 m3 ->
eval_expr E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m ->
eval_expr (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
(updDefVars (Fma (Var R 1) (Var R 2) (Var R 3) ) m
(updDefVars (Var R 3) m3 (updDefVars (Var R 2) m2
(updDefVars (Var R 1) m1 Gamma)))
(updDefVars (Var R 1) m1 Gamma))))
(Fma (Var R 1) (Var R 2) (Var R 3)) (perturb (evalFma v1 v2 v3) m delta) m.
Proof.
admit.
Admitted.
(*
econstructor; try eauto;
eapply Var_load; cbn; auto.
Qed.*)
intros err_v eval_f1 eval_f2 eval_f3 eval_float.
inversion eval_float; subst.
repeat
(match goal with
| [H1: eval_expr ?E ?Gamma ?f ?v1 ?m1, H2: eval_expr ?E ?Gamma ?f ?v2 ?m2 |- _] =>
assert (m1 = m2)
by (eapply Gamma_def in H1; eapply Gamma_def in H2;
rewrite H2 in H1; inversion H1; subst; auto);
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.
Lemma eval_eq_env e:
forall E1 E2 Gamma v m,
......@@ -316,8 +335,10 @@ Proof.
rewrite <- Nat.eqb_neq in H.
eapply Var_load.
+ unfold updDefVars.
cbn. admit.
(* rewrite H; auto. *)
cbn.
apply beq_nat_false in H.
destruct (n ?= x)%nat eqn:?; try auto.
apply Nat.compare_eq in Heqc; subst; congruence.
+ unfold updEnv.
rewrite H; auto.
- eapply Binop_dist'; eauto;
......@@ -325,13 +346,12 @@ Proof.
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
- eapply Fma_dist'; eauto; admit.
(*
- eapply Fma_dist'; eauto;
[eapply IHe1 | eapply IHe2 | eapply IHe3];
eauto;
hnf; intros; eapply no_usedVar;
set_tac. *)
Admitted.
set_tac.
Qed.
Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2:
(forall n, Gamma1 n = Gamma2 n) ->
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment