Commit c2fce4c8 authored by Heiko Becker's avatar Heiko Becker

Division with proof holes in Coq

parent 179823d5
......@@ -147,19 +147,17 @@ Proof.
eapply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (err1:R) (err2:R):
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env_ty) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp machineEpsilon cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp machineEpsilon cenv e2 e2F ->
eval_exp 0%R cenv (Binop Mult e1 e2) vR ->
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Mult (Var R 1) (Var R 2)) vF ->
(Rabs (e1R - e1F) <= err1)%R ->
(Rabs (e2R - e2F) <= err2)%R ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * machineEpsilon)%R.
Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
intros e1_real e1_float e2_real e2_float mult_real mult_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion mult_real; subst.
rewrite perturb_0_val in mult_real; auto.
rewrite perturb_0_val; auto.
......@@ -191,4 +189,47 @@ Proof.
eapply Rmult_le_compat_l; auto.
rewrite <- Rabs_mult.
apply Rabs_pos.
Qed.
\ No newline at end of file
Qed.
Lemma div_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env_ty) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp machineEpsilon cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
eval_exp machineEpsilon cenv e2 e2F ->
eval_exp 0%R cenv (Binop Div e1 e2) vR ->
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Div (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * machineEpsilon)%R.
Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion div_real; subst.
rewrite perturb_0_val in div_real; auto.
rewrite perturb_0_val; auto.
unfold eval_binop in *; simpl in *.
clear delta H2.
rewrite (eval_0_det H4 e1_real);
rewrite (eval_0_det H5 e2_real).
rewrite (eval_0_det H4 e1_real) in div_real.
rewrite (eval_0_det H5 e2_real) in div_real.
clear H4 H5 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion div_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
unfold updEnv; simpl.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear div_float H4 H5 div_real e1_real e1_float e2_real e2_float.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_plus_distr.
rewrite <- Rplus_assoc.
setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
eapply Rle_trans.
eapply Rabs_triang.
eapply Rplus_le_compat_l.
rewrite Rabs_Ropp.
repeat rewrite Rabs_mult.
eapply Rmult_le_compat_l; auto.
apply Rabs_pos.
Qed.
\ No newline at end of file
......@@ -13,7 +13,6 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
match e with
|Var v => false
|Param v => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
(* A constant will be a point intv. Take maxAbs never the less *)
|Const n => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Binop b e1 e2 =>
let (ive1, err1) := env e1 in
......@@ -28,7 +27,7 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
| 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 => false
| Div => Qleb ((maxAbs (subtractIntv (divideIntv ive1 ive2) (divideIntv errIve1 errIve2))) + (maxAbs (divideIntv errIve1 errIve2)) * RationalSimps.machineEpsilon) err
end
in andb (andb rec errPos) theVal
end.
......@@ -1035,6 +1034,108 @@ Proof.
repeat rewrite Q2R_plus; auto.
Qed.
Lemma validErrorboundCorrectDiv cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
eval_exp 0%R cenv (toRExp e2) nR2 ->
eval_exp 0%R cenv (toRExp (Binop Div e1 e2)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e1) nF1 ->
eval_exp (Q2R RationalSimps.machineEpsilon) cenv (toRExp e2) nF2 ->
eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 cenv)) (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF ->
validErrorbound (Binop Div e1 e2) absenv = true ->
validIntervalbounds (Binop Div e1 e2) absenv P = true ->
absenv e1 = ((e1lo,e1hi),err1) ->
absenv e2 = ((e2lo, e2hi),err2) ->
absenv (Binop Div e1 e2) = ((alo,ahi),e)->
(Rabs (nR1 - nF1) <= (Q2R err1))%R ->
(Rabs (nR2 - nF2) <= (Q2R err2))%R ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros p_valid e1_real e2_real eval_real e1_float e2_float eval_float
valid_error valid_intv absenv_e1 absenv_e2 absenv_div
err1_bounded err2_bounded.
pose proof (ivbounds_approximatesPrecond_sound (Binop Div e1 e2) absenv P valid_intv) as env_approx_p.
eapply Rle_trans.
eapply (div_abs_err_bounded (toRExp e1) _ _ (toRExp e2)); eauto.
rewrite <- mEps_eq_Rmeps.
apply e1_float.
rewrite <- mEps_eq_Rmeps.
apply e2_float.
rewrite <- mEps_eq_Rmeps.
apply eval_float.
rewrite <- mEps_eq_Rmeps.
unfold validErrorbound in valid_error at 1.
rewrite absenv_div, 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.
apply Is_true_eq_true in valid_error.
destruct valid_rec as [valid_rec le_0_e].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_err1 valid_err2].
apply Is_true_eq_true in valid_err1.
apply Is_true_eq_true in valid_err2.
assert (0 <= Q2R err1)%R as err1_pos by (apply (err_always_positive e1 absenv (e1lo,e1hi) err1); auto).
assert (0 <= Q2R err2)%R as err2_pos by (apply (err_always_positive e2 absenv (e2lo,e2hi) err2); auto).
clear valid_err1 valid_err2.
apply Qle_bool_iff in valid_error.
apply Qle_Rle in valid_error.
rewrite Q2R_plus, Q2R_mult in valid_error.
eapply Rle_trans.
Focus 2.
apply valid_error.
eapply Rplus_le_compat.
- (* Similar to other goal *)
remember
(subtractIntv (divideIntv (e1lo, e1hi) (e2lo, e2hi))
(divideIntv (widenIntv (e1lo, e1hi) err1)
(widenIntv (e2lo, e2hi) err2))) as iv.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
admit. (* By validity of IV, monotonicity *)
- apply Rmult_le_compat_r.
+ apply mEps_geq_zero.
+ remember (divideIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
admit. (*
assert (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1 by admit.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
pose proof (IntervalArith.interval_multiplication_valid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
unfold RmaxAbsFun.
apply Rmult_le_compat_r.
apply mEps_geq_zero.
apply RmaxAbs; subst; simpl in *.
- rewrite Q2R_min4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
- rewrite Q2R_max4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
Qed. *)
Admitted.
Lemma validErrorbound_sound (e:exp Q):
forall cenv absenv nR nF err P elo ehi,
precondValidForExec P cenv ->
......@@ -1139,5 +1240,21 @@ Proof.
{ apply andb_prop_intro.
split; apply Is_true_eq_left; auto. }
{ apply Is_true_eq_left; auto. }
+ inversion valid_error.
+ eapply (validErrorboundCorrectDiv 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; try auto.
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. }
Qed.
......@@ -85,6 +85,15 @@ Proof.
subst; auto.
Qed.
Definition Q2RP (iv:Q*Q) :=
let (lo,hi) := iv in (Q2R lo, Q2R hi).
Lemma maxAbs_impl_RmaxAbs_iv iv:
RmaxAbsFun (Q2RP iv) = Q2R (maxAbs iv).
Proof.
unfold Q2RP; destruct iv; apply maxAbs_impl_RmaxAbs.
Qed.
Lemma Q2R_max (a:Q) (b:Q) :
Rmax (Q2R a) (Q2R b) = Q2R (Qmax a b).
Proof.
......
(**
Interval arithmetic checker and its soundness proof
**)
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List.
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps.
......@@ -10,16 +10,16 @@ Import Lists.List.ListNotations.
Fixpoint freeVars (V:Type) (e:exp V) : list nat:=
match e with
|Const n => []
|Var v => []
|Param v => [v]
|Var _ v => []
|Param _ v => [v]
|Binop b e1 e2 => (freeVars V e1) ++ (freeVars V e2)
end.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
let (intv, _) := absenv e in
match e with
| Var v => false
| Param v =>
| Var _ v => false
| Param _ v =>
isSupersetIntv (P v) intv
| Const n =>
isSupersetIntv (n,n) intv
......@@ -259,5 +259,31 @@ Proof.
repeat rewrite <- Q2R_mult in valid_mul_hi.
rewrite <- Q2R_max4 in valid_mul_hi.
unfold absIvUpd; auto.
+ pose proof (divisionIsValid (Q2R v1) v2 (Q2R (fst iv1), Q2R (snd iv1)) (Q2R (fst iv2),Q2R (snd iv2))) as valid_div. contradiction.
Qed.
\ No newline at end of file
+ pose proof (divisionIsValid v1 v2 (Q2R (fst iv1), Q2R (snd iv1)) (Q2R (fst iv2),Q2R (snd iv2))) as valid_div.
unfold contained in valid_div.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_div as [valid_div_lo valid_div_hi]; try auto.
* admit.
* unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi.
simpl in *.
split.
{ eapply Rle_trans. apply valid_lo.
unfold ivlo. unfold multIntv.
simpl in valid_div_lo.
rewrite <- Q2R_inv in valid_div_lo; [ | admit].
rewrite <- Q2R_inv in valid_div_lo; [ | admit].
repeat rewrite <- Q2R_mult in valid_div_lo.
rewrite <- Q2R_min4 in valid_div_lo; auto. }
{ eapply Rle_trans.
Focus 2.
apply valid_hi.
simpl in valid_div_hi.
rewrite <- Q2R_inv in valid_div_hi; [ | admit].
rewrite <- Q2R_inv in valid_div_hi; [ | admit].
repeat rewrite <- Q2R_mult in valid_div_hi.
rewrite <- Q2R_max4 in valid_div_hi; auto. }
Admitted.
\ No newline at end of file
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