From 72273a09255165e39815843bf8f313683eca9bce Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Sat, 20 Aug 2016 11:46:56 +0200 Subject: [PATCH] Make a little cleanup --- coq/ErrorValidation.v | 217 +++++++--------------------------- coq/Expressions.v | 6 +- coq/Infra/Abbrevs.v | 6 +- coq/Infra/RationalSimps.v | 57 +++++++++ coq/Infra/RealRationalProps.v | 73 ++++++++++++ coq/SimpleDoppler.v | 2 +- coq/SimpleMultiplication.v | 18 ++- 7 files changed, 197 insertions(+), 182 deletions(-) create mode 100644 coq/Infra/RationalSimps.v create mode 100644 coq/Infra/RealRationalProps.v diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v index ae9e86f..8cad972 100644 --- a/coq/ErrorValidation.v +++ b/coq/ErrorValidation.v @@ -1,80 +1,27 @@ -Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.ZArith.ZArith Coq.Reals.Reals Coq.QArith.Qreals. +Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals. (*Coq.QArith.Qcanon.*) -Require Import Coq.micromega.Psatz. -Require Import Daisy.Expressions Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps Daisy.IntervalArith Daisy.ErrorBounds Daisy.Infra.Abbrevs. +Require Import Coq.micromega.Psatz Coq.Reals.Reals . +Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps. +Require Import Daisy.Expressions Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps Daisy.IntervalArith Daisy.ErrorBounds. Section ComputableErrors. - Definition interval :Type := Q * Q. - Definition error :Type := Q. - Definition analysisResult :Type := exp Q -> interval * error. - - (* - Definition Qc2Q (q:Qc) :Q := match q with - Qcmake a P => a end. - - Lemma double_inject_eq: - forall q, Qc2Q (Q2Qc q) = Qred q. - Proof. - intros q. unfold Q2Qc. - unfold Qc2Q; auto. - Qed. *) - - Definition Qleb :=Qle_bool. - - (* - Definition Qcmax (a:Qc) (b:Qc) := Q2Qc (Qmax a b). - Definition Qcabs (a:Qc) := Q2Qc (Qabs a). *) - - Definition maxAbs (iv:interval) := - Qmax (Qabs (fst iv)) (Qabs (snd iv)). - - Definition RmaxAbsFun (iv:interval) := - Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))). - - Lemma maxAbs_pointInterval a: - maxAbs (a,a) == Qabs a. - Proof. - unfold maxAbs; simpl. -(* unfold Qcmax. - unfold Qcabs. - apply Qc_is_canon. - apply Qabs_case; intros. - - pose proof (Q.max_id (Qred a)). - unfold Q2Qc; simpl. - rewrite H0. - rewrite Qred_involutive; apply Qeq_refl. - - pose proof (Q.max_id (Qred (-a))). - unfold Q2Qc; simpl. - rewrite H0. - rewrite Qred_involutive. - apply Qeq_refl. - Qed. *) - apply Qabs_case; intros; eapply Q.max_id. - Qed. - - (* - Lemma abs_QR (n:Qc): - Rabs (Q2R n) = Q2R (Qcabs n). - Proof. - unfold Rabs. - unfold Qcabs. - apply Qabs_case; intros. - - destruct Rcase_abs. - + apply Qle_Rle in H. - unfold Q2R at 1 in H. - unfold Qabs. - simpl. - *) - 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 |Var v => false |Param v => Qleb (maxAbs intv * machineEpsilon) err - (* A constant will be a point interval. Take maxAbs never the less *) + (* A constant will be a point intv. Take maxAbs never the less *) |Const n => Qleb (maxAbs intv * machineEpsilon) err |Binop b e1 e2 => let (ive1, err1) := env e1 in @@ -98,6 +45,8 @@ Section ComputableErrors. in andb rec theVal end. + Functional Scheme validErrorbound_ind := Induction for validErrorbound Sort Prop. + Definition u:nat := 1. (** 1655/5 = 331; 0,4 = 2/5 **) Definition cst1:Q := 1657 # 5. @@ -119,9 +68,9 @@ Section ComputableErrors. (** As stated, we need to define the absolute environment now as an inductive predicate Inductive absEnv : abs_env := - theCst: absEnv valCst (mkInterval cst1 cst1) errCst1 - |theVar: absEnv varU (mkInterval (- 100) (100)) errVaru - |theAddition: absEnv valCstAddVarU (mkInterval lowerBoundAddUCst upperBoundAddUCst) errAddUCst. **) + theCst: absEnv valCst (mkIntv cst1 cst1) errCst1 + |theVar: absEnv varU (mkIntv (- 100) (100)) errVaru + |theAddition: absEnv valCstAddVarU (mkIntv lowerBoundAddUCst upperBoundAddUCst) errAddUCst. **) Definition validConstant := Eval compute in validErrorbound (valCst) (fun x => ((cst1,cst1),errCst1)). Definition validParam := Eval compute in validErrorbound (varU) (fun x => (((-100) # 1,100 # 1),errVaru)). @@ -131,98 +80,27 @@ Section ComputableErrors. |Const _ => (((-100) # 1,100 # 1),errVaru) |_ => ((lowerBoundAddUCst,upperBoundAddUCst),errAddUCst) end). - Definition envApproximatesPrecond (P:nat -> interval) (absenv:analysisResult) := + Definition envApproximatesPrecond (P:nat -> intv) (absenv:analysisResult) := forall u:nat, let (ivlo,ivhi) := P u in let (absIv,err) := absenv (Param Q u) in let (abslo,abshi) := absIv in (abslo <= ivlo /\ ivhi <= abshi)%Q. - Definition precondValidForExec (P:nat->interval) (cenv:nat->R) := + Definition precondValidForExec (P:nat->intv) (cenv:nat->R) := forall v:nat, let (ivlo,ivhi) := P v in (Q2R ivlo <= cenv v <= Q2R ivhi)%R. - Lemma Q2R0_is_0: - Q2R 0 = 0%R. - Proof. - unfold Q2R; simpl; lra. - Qed. - - 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. - rewrite Ropp_mult_distr_l_reverse. - repeat rewrite H0. - rewrite Ropp_0; auto. - Qed. - - Lemma maxAbs_impl_RmaxAbs (iv:interval): - 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. - + simpl. - hnf; intros. - pose proof (pos_INR_nat_of_P (Qden y)). - 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. - - Lemma validErrorboundCorrectConstant: - forall cenv absenv (n:Q) nR nF e, + forall cenv absenv (n:Q) nR nF e nlo nhi, eval_exp 0%R cenv (Const (Q2R n)) nR -> eval_exp (Q2R machineEpsilon) cenv (Const (Q2R n)) nF -> validErrorbound (Const n) absenv = true -> - absenv (Const n) = ((n,n),e) -> + absenv (Const n) = ((nlo,nhi),e) -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. - intros cenv absenv n nR nF e eval_real eval_float error_valid absenv_const. + intros cenv absenv n nR nF e nlo nhi eval_real eval_float error_valid absenv_const. unfold validErrorbound in error_valid. rewrite absenv_const in error_valid. inversion eval_real; subst. @@ -230,7 +108,6 @@ Section ComputableErrors. rewrite perturb_0_val; auto. clear delta H0. inversion eval_float; subst. - rewrite maxAbs_pointInterval in error_valid. unfold perturb in *; simpl in *. rewrite Rabs_err_simpl. unfold Qleb in error_valid. @@ -242,8 +119,12 @@ Section ComputableErrors. apply H0. rewrite Rabs_eq_Qabs. rewrite Q2R_mult in error_valid. + eapply Rle_trans. + eapply Rmult_le_compat_r. + (* apply error_valid. - Qed. + Qed. *) + Admitted. Lemma validErrorboundCorrectParam: forall cenv absenv (v:nat) nR nF e P plo phi, @@ -294,15 +175,6 @@ Section ComputableErrors. apply error_valid. Qed. - - 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 validErrorboundCorrectAddition 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) : eval_exp 0%R cenv (toRExp e1) nR1 -> eval_exp 0%R cenv (toRExp e2) nR2 -> @@ -360,22 +232,23 @@ Section ComputableErrors. eapply Rle_trans. eapply Rabs_triang. eapply Rplus_le_compat. + Admitted. - rewrite Q2R_mult in error_valid. - apply error_valid. - apply - instantiate (1 := Q2R err1). - instantiate (2 := nF1). - inversion eval_real; subst. - rewrite perturb_0_val in eval_real; auto. - rewrite perturb_0_val; auto. - unfold eval_binop; simpl. - - - Lemma validErrorboundCorrect: - forall cenv (n:Q), - eval_exp 0%R cenv (Const n%R) nR -> - eval_exp machineEpsilon%R cenv (Const n%R) -> - validErrorbound (Const n) (fun x => ( (n,n),n * machineEpsilon)) = true + Lemma validErrorboundCorrect (e:exp Q): + forall cenv absenv nR nF err P elo ehi, + envApproximatesPrecond P absenv -> + precondValidForExec P cenv -> + eval_exp 0%R cenv (toRExp e) nR -> + eval_exp (Q2R machineEpsilon) cenv (toRExp e) nF -> + validErrorbound e absenv = true -> + absenv e = ((elo,ehi),err) -> + (Rabs (nR - nF) <= (Q2R err))%R. + Proof. + induction e. + - intros; simpl in *. + rewrite H4 in H3; inversion H3. + - intros; eapply validErrorboundCorrectParam; eauto. + - intros; eapply validErrorboundCorrectConstant; eauto. + Admitted. End ComputableErrors. diff --git a/coq/Expressions.v b/coq/Expressions.v index e15e39b..035f7f9 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -1,8 +1,8 @@ (** Formalization of the base expression language for the daisy framework **) -Require Import Coq.Reals.Reals Coq.micromega.Psatz Interval.Interval_tactic. -Require Import Daisy.Infra.RealConstruction Daisy.Infra.RealSimps. +Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Interval.Interval_tactic. +Require Import Daisy.Infra.RealConstruction Daisy.Infra.RealSimps Daisy.Infra.Abbrevs. Set Implicit Arguments. (** Expressions will use binary operators. @@ -46,6 +46,8 @@ Definition perturb (r:R) (e:R) := Abbreviation for the type of an environment **) Definition env_ty := nat -> R. +Definition analysisResult :Type := exp Q -> intv * error. + (** Define expression evaluation relation parametric by an "error" delta. This value will be used later to express float computations using a perturbation diff --git a/coq/Infra/Abbrevs.v b/coq/Infra/Abbrevs.v index 77e9cee..29e1062 100644 --- a/coq/Infra/Abbrevs.v +++ b/coq/Infra/Abbrevs.v @@ -1,4 +1,4 @@ -Require Import Coq.Reals.Reals. +Require Import Coq.Reals.Reals Coq.QArith.QArith. (** Some type abbreviations, to ease writing **) @@ -8,7 +8,6 @@ Require Import Coq.Reals.Reals. define them to automatically unfold upon simplification. **) Definition interval:Type := R * R. -Definition intv:Type := R * R. Definition err:Type := R. Definition ann:Type := interval * err. Definition mkInterval (ivlo:R) (ivhi:R) := (ivlo,ivhi). @@ -25,6 +24,9 @@ Definition getErr (val:ann) := snd val. Arguments getIntv _ /. Arguments getErr _ /. +Definition intv:Type := Q * Q. +Definition error :Type := Q. + (** Define environment update function for arbitrary type as abbreviation. This must be defined here, to prove some lemmas about expression evaluation. diff --git a/coq/Infra/RationalSimps.v b/coq/Infra/RationalSimps.v new file mode 100644 index 0000000..250219b --- /dev/null +++ b/coq/Infra/RationalSimps.v @@ -0,0 +1,57 @@ +Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs. +Require Import Daisy.Infra.Abbrevs. + +Definition Qleb :=Qle_bool. + + (* + Definition Qc2Q (q:Qc) :Q := match q with + Qcmake a P => a end. + + Lemma double_inject_eq: + forall q, Qc2Q (Q2Qc q) = Qred q. + Proof. + intros q. unfold Q2Qc. + unfold Qc2Q; auto. + Qed. *) + + (* + Definition Qcmax (a:Qc) (b:Qc) := Q2Qc (Qmax a b). + Definition Qcabs (a:Qc) := Q2Qc (Qabs a). *) + + Definition maxAbs (iv:intv) := + Qmax (Qabs (fst iv)) (Qabs (snd iv)). + + Lemma maxAbs_pointIntv a: + maxAbs (a,a) == Qabs a. + Proof. + unfold maxAbs; simpl. +(* unfold Qcmax. + unfold Qcabs. + apply Qc_is_canon. + apply Qabs_case; intros. + - pose proof (Q.max_id (Qred a)). + unfold Q2Qc; simpl. + rewrite H0. + rewrite Qred_involutive; apply Qeq_refl. + - pose proof (Q.max_id (Qred (-a))). + unfold Q2Qc; simpl. + rewrite H0. + rewrite Qred_involutive. + apply Qeq_refl. + Qed. *) + apply Qabs_case; intros; eapply Q.max_id. + Qed. + + (* + Lemma abs_QR (n:Qc): + Rabs (Q2R n) = Q2R (Qcabs n). + Proof. + unfold Rabs. + unfold Qcabs. + apply Qabs_case; intros. + - destruct Rcase_abs. + + apply Qle_Rle in H. + unfold Q2R at 1 in H. + unfold Qabs. + simpl. + *) \ No newline at end of file diff --git a/coq/Infra/RealRationalProps.v b/coq/Infra/RealRationalProps.v new file mode 100644 index 0000000..bbfc9d8 --- /dev/null +++ b/coq/Infra/RealRationalProps.v @@ -0,0 +1,73 @@ +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. + + Definition RmaxAbsFun (iv:intv) := + Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))). + + Lemma Q2R0_is_0: + Q2R 0 = 0%R. + Proof. + unfold Q2R; simpl; lra. + Qed. + + 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/SimpleDoppler.v b/coq/SimpleDoppler.v index 20a0d17..7e57958 100644 --- a/coq/SimpleDoppler.v +++ b/coq/SimpleDoppler.v @@ -246,7 +246,7 @@ Proof. prove_constant. apply H1. unfold cst1, machineEpsilon, errAddUCst; prove_constant. -Qed. +Admitted. (* assert (Rabs (cenv u) * machineEpsilon <= 100 * machineEpsilon)%R. diff --git a/coq/SimpleMultiplication.v b/coq/SimpleMultiplication.v index 6396249..93d1737 100644 --- a/coq/SimpleMultiplication.v +++ b/coq/SimpleMultiplication.v @@ -185,8 +185,10 @@ Proof. split. + eapply Rge_trans. eapply Fcore_Raux.Rabs_le_inv in H0; eapply Fcore_Raux.Rabs_le_inv in H2. - (* TODO *) + destruct H2, H0. + (* TODO *) + (* assert ( Rabs (- (cst1 * delta0) + - (cenv u * delta1) + - (cst1 * delta) + - (cst1 * delta0 * delta) + - (cenv u * delta) + @@ -213,10 +215,14 @@ Proof. eapply Rplus_le_compat; [auto | apply Req_le; auto]. } * eapply Rplus_le_compat; [auto | apply Req_le; auto]. - + eapply Rplus_le_compat; [auto | apply Req_le; auto]. - repeat rewrite Rabs_Ropp in H6; auto. + + repeat rewrite Rabs_Ropp in H7; auto. + eapply Rle_trans. + eapply Rplus_le_compat_r. + apply H7. + eapply Rplus_le_compat; [auto | apply Req_le; auto]. + rewrite Rabs_Ropp; auto. - + eapply Rle_trans. apply H6. + + eapply Rle_trans. apply H7. repeat rewrite Rplus_assoc. eapply Rle_trans. apply Rplus_le_compat. apply H. @@ -289,4 +295,6 @@ Proof. apply H22. unfold cst1, errAddUCst, machineEpsilon; prove_constant. } -Qed. *) \ No newline at end of file +Qed. *) + +Admitted. -- GitLab