Commit 6dac01f9 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix holes in correctness lemma. Only multiplication left

parent e8dca322
......@@ -397,6 +397,9 @@ Section ComputableErrors.
apply Rle_abs.
Qed.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
Lemma validErrorboundCorrect (e:exp Q):
forall cenv absenv nR nF err P elo ehi,
envApproximatesPrecond P absenv ->
......@@ -413,32 +416,73 @@ Section ComputableErrors.
rewrite H5 in H3; rewrite H5 in H4; inversion H3.
- intros; eapply validErrorboundCorrectParam; eauto.
- intros; eapply validErrorboundCorrectConstant; eauto.
- intros. destruct b.
+ inversion H1; subst.
apply existential_rewriting in H2.
destruct H2.
destruct H2.
destruct H2.
destruct H6.
eapply (validErrorboundCorrectAddition cenv absenv e1 e2); eauto.
destruct (absenv e1) as [iv1 err1]; destruct iv1; admit.
destruct (absenv e2) as [iv2 err2]; destruct iv2; admit.
eapply IHe1; auto.
apply H. apply H0. apply H11. apply H2. admit.
admit. admit.
eapply IHe2; auto.
apply H. apply H0.
apply H12. apply H6.
admit. admit. admit.
+ admit.
- intros cenv absenv nR nF err P elo ehi env_approx_p p_valid eval_real eval_float valid_error valid_intv absenv_eq.
simpl in valid_error.
env_assert absenv e1 absenv_e1.
env_assert absenv e2 absenv_e2.
destruct absenv_e1 as [iv1 [err1 absenv_e1]].
destruct absenv_e2 as [iv2 [err2 absenv_e2]].
iv_assert iv1 iv_e1.
destruct iv_e1 as [ivlo1 [ivhi1 iv_e1]].
rewrite iv_e1 in absenv_e1.
iv_assert iv2 iv_e2.
destruct iv_e2 as [ivlo2 [ivhi2 iv_e2]].
rewrite iv_e2 in absenv_e2.
rewrite absenv_eq, absenv_e1, absenv_e2 in valid_error.
apply Is_true_eq_left in valid_error.
apply andb_prop_elim in valid_error.
destruct valid_error as [valid_rec valid_error].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_err_e1 valid_err_e2].
apply Is_true_eq_true in valid_err_e1;
apply Is_true_eq_true in valid_err_e2.
apply Is_true_eq_true in valid_error.
simpl in valid_intv.
rewrite absenv_eq, absenv_e1, absenv_e2 in valid_intv.
apply Is_true_eq_left in valid_intv.
apply andb_prop_elim in valid_intv.
destruct valid_intv as [valid_rec valid_intv].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_intv_e1 valid_intv_e2].
apply Is_true_eq_true in valid_intv_e1;
apply Is_true_eq_true in valid_intv_e2.
apply Is_true_eq_true in valid_intv.
inversion eval_real; subst.
apply existential_rewriting in eval_float.
destruct eval_float as [v1F [v2F [eval_e1_float [eval_e2_float eval_float]]]].
destruct b.
+ eapply (validErrorboundCorrectAddition cenv absenv e1 e2); eauto.
simpl.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
* apply andb_prop_intro.
split; apply Is_true_eq_left; auto.
* apply Is_true_eq_left; auto.
* unfold validIntervalbounds.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
{ apply andb_prop_intro.
split; apply Is_true_eq_left; auto. }
{ apply Is_true_eq_left; auto. }
+ eapply (validErrorboundCorrectSubtraction cenv absenv e1 e2); eauto.
simpl.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
* apply andb_prop_intro.
split; apply Is_true_eq_left; auto.
* apply Is_true_eq_left; auto.
* unfold validIntervalbounds.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
{ apply andb_prop_intro.
split; apply Is_true_eq_left; auto. }
{ apply Is_true_eq_left; auto. }
+ admit.
+ simpl in H3.
rewrite H5 in H3.
apply Is_true_eq_left in H3.
destruct (absenv e1); destruct (absenv e2).
apply andb_prop_elim in H3.
destruct H3.
simpl in H6; contradiction.
+ inversion valid_error.
Admitted.
End ComputableErrors.
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