Commit ee0c7601 authored by Heiko Becker's avatar Heiko Becker

Remove residual admits from validErrorbound soundness proof for variables

parent 5aa957d0
......@@ -14,46 +14,53 @@ Require Import Daisy.Environments Daisy.IntervalValidation Daisy.ErrorBounds.
(** Error bound validator **)
Fixpoint validErrorbound (e:exp Q) (absenv:analysisResult) (dVars:NatSet.t):=
let (intv, err) := (absenv e) in
let errPos := Qleb 0 err in
let res :=
match e with
|Var _ v => if (NatSet.mem v dVars) then true else (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Const n => Qleb (maxAbs intv * RationalSimps.machineEpsilon) err
|Unop _ _ => false
|Binop b e1 e2 =>
let (ive1, err1) := absenv e1 in
let (ive2, err2) := absenv e2 in
let rec := andb (validErrorbound e1 absenv dVars) (validErrorbound e2 absenv dVars) in
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let theVal :=
match b with
| Plus => Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
| Sub => Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
| Mult => Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
| Div => let upperBoundInvE2 := maxAbs (invertIntv ive2) in
let nodiv0_fl := orb
(andb (Qleb (ivhi errIve2) 0) (negb (Qeq_bool (ivhi errIve2) 0)))
(andb (Qleb 0 (ivlo errIve2)) (negb (Qeq_bool (ivlo errIve2) 0))) in
if nodiv0_fl
then let minAbsIve2 := minAbs (errIve2) in
let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
else false
end
in andb rec theVal
end
in
andb errPos res.
if (Qleb 0 err)
then
match e with
|Var _ v =>
if (NatSet.mem v dVars)
then true
else (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Const n =>
Qleb (maxAbs intv * RationalSimps.machineEpsilon) err
|Unop _ _ => false
|Binop b e1 e2 =>
if ((validErrorbound e1 absenv dVars) && (validErrorbound e2 absenv dVars))
then
let (ive1, err1) := absenv e1 in
let (ive2, err2) := absenv e2 in
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
match b with
| Plus =>
Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * machineEpsilon) err
| Sub =>
Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * machineEpsilon) err
| Mult =>
Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * machineEpsilon) err
| Div =>
if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
then
let upperBoundInvE2 := maxAbs (invertIntv ive2) in
let minAbsIve2 := minAbs (errIve2) in
let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * machineEpsilon) err
else false
end
else false
end
else false.
(** Error bound command validator **)
Fixpoint validErrorboundCmd (f:cmd Q) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool :=
match f with
|Let x e g =>
(validErrorbound e env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q x)))) &&
validErrorboundCmd g env (NatSet.add x dVars)
if ((validErrorbound e env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q x)))))
then validErrorboundCmd g env (NatSet.add x dVars)
else false
|Ret e => validErrorbound e env dVars
end.
......@@ -81,85 +88,102 @@ Lemma validErrorboundCorrectVariable:
forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars,
approxEnv E1 absenv fVars dVars E2 ->
eval_exp 0%R E1 (toRExp (Var Q v)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) E2 (toRExp (Var Q v)) nF ->
eval_exp (Q2R machineEpsilon) E2 (toRExp (Var Q v)) nF ->
validIntervalbounds (Var Q v) absenv P dVars = true ->
validErrorbound (Var Q v) absenv dVars = true ->
(forall v : NatSet.elt,
(forall v,
NatSet.mem v dVars = true ->
exists vR0 : R,
E1 v = Some vR0 /\
(Q2R (fst (fst (absenv (Var Q v)))) <= vR0 <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
exists r : R,
E1 v = Some r /\
(Q2R (fst (fst (absenv (Var Q v)))) <= r <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
(forall v, NatSet.mem v fVars= true ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
absenv (Var Q v) = ((nlo,nhi),e) ->
exists r, E1 v = Some r /\
(Q2R (fst (P v)) <= r <= Q2R (snd (P v)))%R) ->
absenv (Var Q v) = ((nlo, nhi), e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros E1 E2 absenv v nR nF e nlo nhi P fVars dVars approxCEnv eval_real
eval_float bounds_valid error_valid dVars_sound P_valid absenv_var.
inversion eval_real; inversion eval_float; subst.
unfold validErrorbound in error_valid.
rewrite absenv_var in *; simpl in *.
rename H0 into E1_v;
rename H3 into E2_v.
simpl in error_valid.
rewrite absenv_var in error_valid; simpl in error_valid.
rewrite <- andb_lazy_alt in error_valid.
andb_to_prop error_valid.
rename R into error_valid.
rename L into error_pos.
rename R into error_valid.
(* induction on the approximation relation to do a case distinction on whether
we argue currently about a free or a let bound variable *)
induction approxCEnv.
(* empty environment case, contradiction *)
- unfold emptyEnv in *; simpl in *.
inversion H0.
congruence.
- unfold updEnv in *; simpl in *.
case_eq (v =? x); intros eq_case; rewrite eq_case in *.
+ rewrite Nat.eqb_eq in eq_case; subst.
assert (NatSet.mem x dVars = false).
assert (NatSet.mem x dVars = false) as x_not_bound.
* case_eq (NatSet.mem x dVars); intros case_mem; try auto.
rewrite NatSet.mem_spec in case_mem.
assert (NatSet.In x (NatSet.union fVars dVars)) by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in H2.
rewrite H2 in H1. inversion H1.
* rewrite H2 in error_valid.
inversion H0; inversion H3; subst.
eapply Rle_trans.
apply H.
repeat (rewrite delta_0_deterministic in H3; auto).
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
eapply Rle_trans.
Focus 2.
apply error_valid.
rewrite Q2R_mult.
apply Rmult_le_compat_r.
{ apply mEps_geq_zero. }
{ rewrite <- maxAbs_impl_RmaxAbs.
apply contained_leq_maxAbs_val.
unfold contained.
pose proof (validIntervalbounds_sound (Var Q x) A P dVars (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid) as valid_bounds_prf.
rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
simpl; apply valid_bounds_prf; auto.
admit. }
assert (NatSet.In x (NatSet.union fVars dVars))
as x_in_union by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in x_in_union.
rewrite x_in_union in *.
congruence.
* rewrite x_not_bound in error_valid.
inversion E1_v; inversion E2_v;
subst.
eapply Rle_trans; try eauto.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
eapply Rle_trans; eauto.
rewrite Q2R_mult.
apply Rmult_le_compat_r.
{ apply mEps_geq_zero. }
{ rewrite <- maxAbs_impl_RmaxAbs.
apply contained_leq_maxAbs_val.
unfold contained; simpl.
pose proof (validIntervalbounds_sound (Var Q x) A P dVars (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid) as valid_bounds_prf.
rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
apply valid_bounds_prf; try auto.
intros v v_mem_diff.
eapply P_valid.
rewrite NatSet.mem_spec, NatSet.add_spec.
rewrite NatSet.mem_spec, NatSet.diff_spec in v_mem_diff.
destruct v_mem_diff as [v_eq_x v_no_dVar].
rewrite NatSet.singleton_spec in v_eq_x.
auto. }
+ apply IHapproxCEnv; try auto.
{ constructor; auto. }
{ constructor; auto. }
intros v0 mem_dVars;
specialize (dVars_sound v0 mem_dVars).
destruct dVars_sound as [vR0 [val_def iv_sound_val]].
case_eq (v0 =? x); intros case_mem;
rewrite case_mem in val_def; simpl in val_def.
* rewrite Nat.eqb_eq in case_mem.
subst.
rewrite NatSet.mem_spec in mem_dVars.
assert (NatSet.In x (NatSet.union fVars dVars)) by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in H2;
rewrite H2 in H1; inversion H1.
* exists vR0; split; auto.
* admit.
- unfold updEnv in *; simpl in *.
* constructor; auto.
* constructor; auto.
* intros v0 mem_dVars;
specialize (dVars_sound v0 mem_dVars).
destruct dVars_sound as [vR0 [val_def iv_sound_val]].
case_eq (v0 =? x); intros case_mem;
rewrite case_mem in val_def; simpl in val_def.
{ rewrite Nat.eqb_eq in case_mem; subst.
rewrite NatSet.mem_spec in mem_dVars.
assert (NatSet.In x (NatSet.union fVars dVars))
as x_in_union by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in x_in_union;
rewrite x_in_union in *; congruence. }
{ exists vR0; split; auto. }
* intros v0 v0_fVar.
assert (NatSet.mem v0 (NatSet.add x fVars) = true)
as v0_in_add by (rewrite NatSet.mem_spec, NatSet.add_spec; rewrite NatSet.mem_spec in v0_fVar; auto).
specialize (P_valid v0 v0_in_add).
case_eq (v0 =? x); intros case_v0; rewrite case_v0 in *; try auto.
rewrite Nat.eqb_eq in case_v0; subst.
assert (NatSet.mem x (NatSet.union fVars dVars) = true)
as x_in_union
by (rewrite NatSet.mem_spec, NatSet.union_spec; rewrite NatSet.mem_spec in v0_fVar; auto).
rewrite x_in_union in *; congruence.
- unfold updEnv in E1_v, E2_v; simpl in *.
case_eq (v =? x); intros eq_case; rewrite eq_case in *.
+ rewrite Nat.eqb_eq in eq_case; subst.
symmetry in H0, H3;
inversion H0; inversion H3;
subst.
rewrite absenv_var in H; auto.
+ unfold updEnv in *; simpl in *.
apply IHapproxCEnv; try auto.
inversion E1_v; inversion E2_v; subst.
rewrite absenv_var in *; auto.
+ apply IHapproxCEnv; try auto.
* constructor; auto.
* constructor; auto.
* rewrite absenv_var.
......@@ -170,43 +194,52 @@ Proof.
intros case_add; rewrite case_add in *; simpl in *; try auto.
- rewrite NatSet.mem_spec in case_add.
rewrite NatSet.add_spec in case_add.
destruct case_add; subst.
destruct case_add as [v_eq_x | v_dVar]; subst.
+ rewrite Nat.eqb_neq in eq_case. exfalso; apply eq_case; auto.
+ rewrite <- NatSet.mem_spec in H2. rewrite H2 in case_dVars.
+ rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars.
inversion case_dVars. }
{ rewrite absenv_var in bounds_valid. rewrite not_in_add in bounds_valid.
auto. }
* admit.
* rewrite absenv_var in bounds_valid; simpl in *.
case_eq (NatSet.mem v dVars);
intros case_dVars; rewrite case_dVars in *; simpl in *; try auto.
assert (NatSet.mem v (NatSet.add x dVars) = false) as not_in_add.
{ case_eq (NatSet.mem v (NatSet.add x dVars));
intros case_add; rewrite case_add in *; simpl in *; try auto.
- rewrite NatSet.mem_spec in case_add.
rewrite NatSet.add_spec in case_add.
destruct case_add as [v_eq_x | v_dVar]; subst.
+ rewrite Nat.eqb_neq in eq_case. exfalso; apply eq_case; auto.
+ rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars.
inversion case_dVars. }
{ rewrite not_in_add in error_valid; auto. }
* intros v0 mem_dVars.
rewrite absenv_var in *; simpl in *.
rewrite NatSet.mem_spec in mem_dVars.
assert (NatSet.In v0 (NatSet.add x dVars)).
assert (NatSet.In v0 (NatSet.add x dVars)) as v0_in_add.
{ rewrite NatSet.add_spec. right; auto. }
{ rewrite <- NatSet.mem_spec in H2.
specialize (dVars_sound v0 H2).
{ rewrite <- NatSet.mem_spec in v0_in_add.
specialize (dVars_sound v0 v0_in_add).
destruct dVars_sound as [vR0 [val_def iv_sound_val]].
unfold updEnv in val_def; simpl in val_def.
case_eq (v0 =? x); intros case_mem;
rewrite case_mem in val_def; simpl in val_def.
rewrite Nat.eqb_eq in case_mem; subst.
- apply (NatSetProps.Dec.F.union_3 fVars) in mem_dVars.
- rewrite Nat.eqb_eq in case_mem; subst.
apply (NatSetProps.Dec.F.union_3 fVars) in mem_dVars.
rewrite <- NatSet.mem_spec in mem_dVars.
rewrite mem_dVars in H1; inversion H1.
rewrite mem_dVars in *; congruence.
- exists vR0; split; auto. }
* rewrite absenv_var in bounds_valid.
case_eq (NatSet.mem v dVars); intros case_mem; try auto.
case_eq (NatSet.mem v (NatSet.add x dVars));
intros case_add; rewrite case_add in *; simpl in *;
try auto.
rewrite NatSet.mem_spec in case_add.
rewrite NatSet.add_spec in case_add.
destruct case_add as [eq_x | in_dVars].
{ rewrite Nat.eqb_neq in eq_case.
exfalso; apply eq_case; auto. }
{ rewrite <- NatSet.mem_spec in in_dVars.
rewrite case_mem in in_dVars.
inversion in_dVars.
admit. }
Admitted.
intros v0 v0_fVar.
specialize (P_valid v0 v0_fVar).
unfold updEnv in P_valid; simpl in *.
case_eq (v0 =? x); intros case_v0; rewrite case_v0 in *; try auto.
rewrite Nat.eqb_eq in case_v0; subst.
assert (NatSet.mem x (NatSet.union fVars dVars) = true)
as x_in_union
by (rewrite NatSet.mem_spec, NatSet.union_spec; rewrite NatSet.mem_spec in v0_fVar; auto).
rewrite x_in_union in *; congruence.
Qed.
Lemma validErrorboundCorrectConstant:
forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars,
......
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