Commit 58137a95 authored by Joachim Bard's avatar Joachim Bard

fixing error validation proofs

parent 4e212b4d
......@@ -391,14 +391,20 @@ Proof.
repeat split; tauto.
}
intros vR (elo, ehi) err eval_real A_res.
assert (vR = vR1)
by (eapply (meps_0_deterministic (Let REAL n (toRExp e1) (toRExp e2))); eauto); subst.
inversion eval_real; subst.
apply validErrorBounds_single with (v__R := v1) (iv:= i1) (err:= e3) in Hsound.
destruct m2; try discriminate.
apply validErrorBounds_single with (v__R := v1) (iv:= i0) (err:= e0) in Hsound; auto.
destruct Hsound as [[ve1 [me1 evalExists]] evalHasError].
assert (validErrorBounds e2 (updEnv n v1 E1) (updEnv n ve1 E2) A Gamma DeltaMap)
as Hsound2.
{ eapply IHe2; eauto.
+ eapply approxUpdBound; try eauto; simpl in *.
eapply (toRExpMap_some _ (Var Q n)); eauto.
+ apply RMicromega.Qeq_true in L0.
eapply approxUpdBound; try eauto; simpl in *.
1: eapply (toRExpMap_some _ (Var Q n)); now eauto.
rewrite <- L0; auto.
eapply evalHasError; eauto.
+ eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
* rewrite NatSet.add_spec, NatSet.union_spec;
......@@ -415,33 +421,42 @@ Proof.
(* rewrite NatSet.diff_spec, NatSet.remove`_spec, NatSet.union_spec. *)
split; tauto.
}
eapply validErrorBounds_single in Hsound2; [ |eauto using H14| admit].
eapply validErrorBounds_single in Hsound2; eauto.
destruct Hsound2 as [[v2 [m2 eval_fixed]] ?].
destruct (deltas_matched (Let m n (toRExp e1) (toRExp e2)) m2).
destruct (deltas_matched (Let m n (toRExp e1) (toRExp e2)) m0).
destruct H2.
split; try auto.
+ exists v2, m2.
eapply Let_dist with (E:=E2); try eauto.
* apply toRExpMap_some with (e:= (Let m n e1 e2)); try auto.
admit. (* from validtypes' *)
* clear H3 H2.
assert (m = me1) by admit; subst. auto.
split.
assert (x = m2) by (eapply validTypes_exec; eauto).
assert (m = me1) by (eapply validTypes_exec; try exact evalExists; eauto).
injection find_me; intros Heq. subst.
+ exists v2, me.
eapply Let_dist with (E:=E2); try eassumption.
eapply toRExpMap_some; eauto. auto.
+ intros * eval_float.
clear H2 H3.
clear eval_fixed.
(* clear eval_fixed. *)
inversion eval_float; subst.
(* assert (m = me1) by (eapply validTypes_exec; try exact evalExists; eauto).
subst. *)
assert (Herr: Q2R err = Q2R e4).
{ apply RMicromega.Qeq_true in R1.
rewrite R1. congruence. }
rewrite Herr.
assert (validErrorBounds e2 (updEnv n v1 E1) (updEnv n v0 E2) A Gamma DeltaMap).
{ eapply IHe2; eauto.
admit.
admit.
admit. }
eapply validErrorBounds_single in H2; [ |eauto using H14 | admit].
- eapply approxUpdBound; eauto.
+ eapply (toRExpMap_some _ (Var Q n)); eauto.
+ apply RMicromega.Qeq_true in L0. rewrite <- L0. eapply evalHasError; eauto.
- eapply ssa_equal_set; eauto.
split; set_tac; tauto.
- intros a ?. apply fVars_subset. set_tac.
split; [right| intros ?; apply H3; set_tac].
split; auto.
intros ?; subst. apply H3. set_tac. }
eapply validErrorBounds_single in H2; eauto.
destruct H2. eapply H3; eauto.
+ auto.
+ canonize_hyps; subst.
admit.
- cbn in *. Flover_compute; congruence.
Admitted.
Qed.
(*
Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
......
......@@ -82,13 +82,13 @@ Inductive eval_expr (E:env)
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
| Let_dist m m1 x f1 f2 v1 v delta:
| Let_dist m1 m2 m x f1 f2 v1 v delta:
Gamma (Let m1 x f1 f2) = Some m ->
DeltaMap (Let m1 x f1 f2) m = Some delta ->
(* TODO: isCompat = true -> *)
isCompat m2 m = true ->
Rabs delta <= mTypeToR m ->
eval_expr E Gamma DeltaMap f1 v1 m1 ->
eval_expr (updEnv x v1 E) Gamma DeltaMap f2 v m ->
eval_expr (updEnv x v1 E) Gamma DeltaMap f2 v m2 ->
eval_expr E Gamma DeltaMap (Let m1 x f1 f2) v m
| Cond_then m1 m2 m3 m f1 f2 f3 v1 v delta:
Gamma (Cond f1 f2 f3) = Some m ->
......@@ -313,6 +313,8 @@ Proof.
rewrite (IHf E v0 v3); try auto.
- inversion ev1; inversion ev2.
assert (v0 = v3) by (eapply IHf1; eauto).
destruct m2; try discriminate.
destruct m4; try discriminate.
subst.
eapply IHf2; eauto.
- inversion ev1; inversion ev2; subst.
......@@ -594,6 +596,7 @@ Proof.
erewrite Gamma_det; eauto.
- inversion Heval1; inversion Heval2; subst.
replace v0 with v3 in * by (eapply IHe1; eauto).
assert (m2 = m4) by (eapply Gamma_det; eauto); subst.
eapply IHe2; eauto.
- inversion Heval1; inversion Heval2; subst.
+ eapply IHe2; erewrite Gamma_det; eauto.
......@@ -648,6 +651,7 @@ Proof.
+ trivial.
+ apply Rabs_0_impl_eq in H4; f_equal; now symmetry.
- inversion ev1; subst.
destruct m2; try discriminate.
econstructor; eauto. rewrite Rabs_R0. cbn. lra.
- inversion ev1; subst.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
......
......@@ -51,7 +51,7 @@ Lemma inlineLets_sound L E Gamma inVars outVars e v :
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (inlineLets L e))) v
REAL.
Proof.
induction e in L, E, inVars, v |- *; cbn; intros Lsound LfVars_valid ssa_e H.
induction e in E, inVars, v |- *; cbn; intros Lsound LfVars_valid ssa_e H.
- Flover_compute; eauto.
- auto.
- inversion H; subst; econstructor; eauto.
......@@ -85,7 +85,8 @@ Proof.
- inversion H; subst.
inversion ssa_e; subst.
econstructor; eauto.
eapply (IHe2 _ _ (NatSet.add n inVars)); eauto.
destruct m2; try discriminate.
eapply (IHe2 _ (NatSet.add n inVars)); eauto.
2: intros; set_tac; right; eapply LfVars_valid; eauto;
set_tac; tauto.
intros x e v'.
......@@ -93,7 +94,7 @@ Proof.
destruct (x =? n) eqn: Heq.
+ intros Hx He.
apply beq_nat_true in Heq; subst.
set_tac. exfalso. apply H11. eapply LfVars_valid; eauto.
set_tac. exfalso. apply H12. eapply LfVars_valid; eauto.
set_tac.
(*
inversion He; subst.
......@@ -116,7 +117,7 @@ Proof.
* eapply Lsound; eauto. now constructor.
* rewrite freeVars_toREval_toRExp_compat.
set_tac. intros ?.
apply H11. eapply LfVars_valid; eauto.
apply H12. eapply LfVars_valid; eauto.
set_tac.
- inversion H; subst.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
......@@ -131,8 +132,6 @@ Proof.
subst. eapply Cond_else; eauto.
Qed.
(* (forall x e, L x = Some e -> NatSet.Subset (freeVars e) (fVars dVars)) -> *)
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P L :=
match q with
| AndQ qP (AndQ (LessQ e' (ConstQ v)) TrueQ) =>
......
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