From c2fce16b71515557e204d798dfca705b3de94850 Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Sun, 21 Aug 2016 12:17:37 +0200 Subject: [PATCH] Proof draft for interval bounds correctness --- coq/ErrorValidation.v | 8 -- coq/Infra/RealRationalProps.v | 142 ++++++++++++++++++---------------- coq/IntervalValidation.v | 51 +++++++++++- 3 files changed, 124 insertions(+), 77 deletions(-) diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v index 8cad972..9d1b16b 100644 --- a/coq/ErrorValidation.v +++ b/coq/ErrorValidation.v @@ -8,14 +8,6 @@ Section ComputableErrors. Definition machineEpsilon := (1#(2^53)). - Fixpoint toRExp (e:exp Q) := - match e with - |Var v => Var R v - |Param v => Param R v - |Const n => Const (Q2R n) - |Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2) - end. - Fixpoint validErrorbound (e:exp Q) (env:analysisResult) := let (intv, err) := (env e) in match e with diff --git a/coq/Infra/RealRationalProps.v b/coq/Infra/RealRationalProps.v index bbfc9d8..0d3df54 100644 --- a/coq/Infra/RealRationalProps.v +++ b/coq/Infra/RealRationalProps.v @@ -1,73 +1,81 @@ Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals. Require Import Coq.Reals.Reals Coq.micromega.Psatz. -Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs. +Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions. - Definition RmaxAbsFun (iv:intv) := - Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))). +Fixpoint toRExp (e:exp Q) := + match e with + |Var v => Var R v + |Param v => Param R v + |Const n => Const (Q2R n) + |Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2) + end. - Lemma Q2R0_is_0: - Q2R 0 = 0%R. - Proof. - unfold Q2R; simpl; lra. - Qed. +Definition RmaxAbsFun (iv:intv) := + Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))). - Lemma Rabs_eq_Qabs: - forall x, Rabs (Q2R x) = Q2R (Qabs x). - Proof. - intro. - apply Qabs_case; unfold Rabs; destruct Rcase_abs; intros; try auto. - - apply Qle_Rle in H. exfalso. - apply Rle_not_lt in H; apply H. - assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra). - rewrite H0. - apply r. - - unfold Q2R. simpl. rewrite (Ropp_mult_distr_l). - f_equal. rewrite opp_IZR; auto. - - apply Qle_Rle in H. hnf in r; hnf in H. destruct r, H. - + exfalso. apply Rlt_not_ge in H. apply H; hnf. - left; rewrite Q2R0_is_0; auto. - + rewrite H in H0. - apply Rgt_not_le in H0. - exfalso; apply H0. - rewrite Q2R0_is_0. - hnf; right; auto. - + rewrite H0 in H. rewrite Q2R0_is_0 in H. - apply Rlt_not_ge in H; exfalso; apply H. - hnf; right; auto. - + unfold Q2R in *; simpl in *. - rewrite opp_IZR; lra. - Qed. +Lemma Q2R0_is_0: + Q2R 0 = 0%R. +Proof. + unfold Q2R; simpl; lra. +Qed. - Lemma maxAbs_impl_RmaxAbs (iv:intv): - RmaxAbsFun iv = Q2R (maxAbs iv). - Proof. - unfold RmaxAbsFun, maxAbs. - repeat rewrite Rabs_eq_Qabs. - apply Q.max_case_strong. - - intros x y x_eq_y Rmax_x. - rewrite Rmax_x. - unfold Q2R. rewrite <- RMicromega.Rinv_elim. - setoid_rewrite Rmult_comm at 1. - + rewrite <- Rmult_assoc. - rewrite <- RMicromega.Rinv_elim. - rewrite <- mult_IZR. - rewrite x_eq_y. - rewrite mult_IZR. - rewrite Rmult_comm; auto. - hnf; intros. - pose proof (pos_INR_nat_of_P (Qden y)). - simpl in H. - rewrite H in H0. - lra. - + simpl; hnf; intros. - pose proof (pos_INR_nat_of_P (Qden x)). - rewrite H in H0; lra. - - intros snd_le_fst. - apply Qle_Rle in snd_le_fst. - apply Rmax_left in snd_le_fst. - subst; auto. - - intros fst_le_snd. - apply Qle_Rle in fst_le_snd. - apply Rmax_right in fst_le_snd. - subst; auto. - Qed. \ No newline at end of file +Lemma Rabs_eq_Qabs: + forall x, Rabs (Q2R x) = Q2R (Qabs x). +Proof. + intro. + apply Qabs_case; unfold Rabs; destruct Rcase_abs; intros; try auto. + - apply Qle_Rle in H. exfalso. + apply Rle_not_lt in H; apply H. + assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra). + rewrite H0. + apply r. + - unfold Q2R. simpl. rewrite (Ropp_mult_distr_l). + f_equal. rewrite opp_IZR; auto. + - apply Qle_Rle in H. hnf in r; hnf in H. destruct r, H. + + exfalso. apply Rlt_not_ge in H. apply H; hnf. + left; rewrite Q2R0_is_0; auto. + + rewrite H in H0. + apply Rgt_not_le in H0. + exfalso; apply H0. + rewrite Q2R0_is_0. + hnf; right; auto. + + rewrite H0 in H. rewrite Q2R0_is_0 in H. + apply Rlt_not_ge in H; exfalso; apply H. + hnf; right; auto. + + unfold Q2R in *; simpl in *. + rewrite opp_IZR; lra. +Qed. + +Lemma maxAbs_impl_RmaxAbs (iv:intv): + RmaxAbsFun iv = Q2R (maxAbs iv). +Proof. + unfold RmaxAbsFun, maxAbs. + repeat rewrite Rabs_eq_Qabs. + apply Q.max_case_strong. + - intros x y x_eq_y Rmax_x. + rewrite Rmax_x. + unfold Q2R. rewrite <- RMicromega.Rinv_elim. + setoid_rewrite Rmult_comm at 1. + + rewrite <- Rmult_assoc. + rewrite <- RMicromega.Rinv_elim. + rewrite <- mult_IZR. + rewrite x_eq_y. + rewrite mult_IZR. + rewrite Rmult_comm; auto. + hnf; intros. + pose proof (pos_INR_nat_of_P (Qden y)). + simpl in H. + rewrite H in H0. + lra. + + simpl; hnf; intros. + pose proof (pos_INR_nat_of_P (Qden x)). + rewrite H in H0; lra. + - intros snd_le_fst. + apply Qle_Rle in snd_le_fst. + apply Rmax_left in snd_le_fst. + subst; auto. + - intros fst_le_snd. + apply Qle_Rle in fst_le_snd. + apply Rmax_right in fst_le_snd. + subst; auto. +Qed. \ No newline at end of file diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 0093cf2..729a6fe 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -1,5 +1,5 @@ -Require Import Coq.QArith.QArith. -Require Import Daisy.Expressions Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.IntervalArithQ Daisy.Infra.RationalConstruction. +Require Import Coq.QArith.QArith Coq.QArith.Qreals. +Require Import Daisy.Expressions Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.IntervalArithQ Daisy.Infra.RationalConstruction Daisy.Infra.RealRationalProps Daisy.IntervalArith. Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):= let (intv, _) := absenv e in @@ -33,6 +33,53 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):= andb rec opres end. +Lemma validIntervalbounds_correct (e:exp Q): + forall (absenv:analysisResult) (P:precond) cenv vR, + validIntervalbounds e absenv P = true -> + eval_exp 0%R cenv (toRExp e) vR -> + contained vR (Q2R (fst (fst(absenv e))), Q2R (snd (fst (absenv e)))). +Proof. + induction e. + - intros absenv P cenv vR valid_bounds eval_e. + unfold validIntervalbounds in valid_bounds. + destruct (absenv (Var Q n)) as [intv err]. + simpl. + (* needs that Precond approximates value *) + admit. + - intros absenv P cenv vR valid_bounds eval_e. + unfold validIntervalbounds in valid_bounds. + destruct (absenv (Param Q n)) as [intv err]. + (* same *) + admit. + - intros absenv P cenv vR valid_bounds eval_e. + unfold validIntervalbounds in valid_bounds. + destruct (absenv (Const v)) as [intv err]. + simpl. + apply Is_true_eq_left in valid_bounds. + apply andb_prop_elim in valid_bounds. + destruct valid_bounds. + unfold contained; simpl. + split. + + apply Is_true_eq_true in H. + unfold Qleb in *. + apply Qle_bool_iff in H. + admit. + + admit. + - destruct b. + + admit. + + admit. + + admit. + + intros absenv P cenv vR valid_bounds eval_e. + simpl in valid_bounds. + destruct (absenv (Binop Div e1 e2)); + destruct (absenv e1); + destruct (absenv e2). + apply Is_true_eq_left in valid_bounds. + apply andb_prop_elim in valid_bounds. + destruct valid_bounds. + unfold Is_true in *; simpl in *. contradiction. +Admitted. + Definition u:nat := 1. (** 1655/5 = 331; 0,4 = 2/5 **) Definition cst1:Q := 1657 # 5. -- GitLab