diff --git a/coq/Infra/RealRationalProps.v b/coq/Infra/RealRationalProps.v index 3530cc01bb983fefc7ec091129eeac1b2d9e3a1b..04eb4c78c974d4f92b5410e40b4976c31ecbbcce 100644 --- a/coq/Infra/RealRationalProps.v +++ b/coq/Infra/RealRationalProps.v @@ -9,8 +9,8 @@ Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions D Fixpoint toRExp (e:exp Q) := match e with - |Var v => Var R v - |Param v => Param R v + |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. diff --git a/coq/IntervalArith.v b/coq/IntervalArith.v index b98ad015e49a21fd34895948a049aa6ff0aee005..e8ab5b692d51f46ab6a2de11cf87f19223beb4a2 100644 --- a/coq/IntervalArith.v +++ b/coq/IntervalArith.v @@ -3,7 +3,6 @@ TODO: Package this into a class or module that depends only on proving the existence of basic operators instead **) Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals. -Require Import Coquelicot.Rcomplements. Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RealSimps. (** Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound. @@ -142,6 +141,29 @@ Qed. Definition invertInterval (intv:interval) := mkInterval (/ IVhi intv) (/ IVlo intv). +Lemma interval_inversion_valid (iv:interval) (a:R) : + (IVhi iv < 0 \/ 0 < IVlo iv -> contained a iv -> contained (/ a) (invertInterval iv))%R. +Proof. + unfold contained; destruct iv as [ivlo ivhi]; simpl; + intros [ivhi_lt_zero | zero_lt_ivlo]; intros [ivlo_le_a a_le_ivhi]; + assert (ivlo <= ivhi)%R by (eapply Rle_trans; eauto); + split. + - assert (- / a <= - / ivhi)%R. + + assert (0 < - ivhi)%R by lra. + repeat rewrite Ropp_inv_permute; try lra. + eapply RIneq.Rinv_le_contravar; try lra. + + apply Ropp_le_ge_contravar in H0; + repeat rewrite Ropp_involutive in H0; lra. + - assert (- / ivlo <= - / a)%R. + + repeat rewrite Ropp_inv_permute; try lra. + eapply RIneq.Rinv_le_contravar; try lra. + + apply Ropp_le_ge_contravar in H0; + repeat rewrite Ropp_involutive in H0; lra. + - eapply RIneq.Rinv_le_contravar; try lra. + - eapply RIneq.Rinv_le_contravar; try lra. +Qed. + + Definition addInterval (iv1:interval) (iv2:interval) := absIntvUpd Rplus iv1 iv2. @@ -263,6 +285,16 @@ Qed. Definition divideInterval (I1:interval) (I2:interval) := multInterval I1 (mkInterval (/ (IVhi I2)) (/ (IVlo I2))). +Corollary divisionIsValid a b I1 I2: + (IVhi I2 < 0 \/ 0 < IVlo I2 -> contained a I1 -> contained b I2 -> contained (a / b) (divideInterval I1 I2))%R. +Proof. + intros nodiv0 c_a c_b. + unfold divideInterval. + unfold Rdiv. + eapply interval_multiplication_valid; auto. + apply interval_inversion_valid; auto. +Qed. + (** Define the maxAbs function on R and prove some minor properties of it. **) Definition RmaxAbsFun (iv:interval) := Rmax (Rabs (fst iv)) (Rabs (snd iv)). @@ -338,14 +370,9 @@ Proof. intros contained_a abs_le; unfold contained in *; simpl in *. destruct contained_a as [lo_a a_hi]. rewrite Rabs_minus_sym in abs_le. - apply Rcomplements.Rabs_le_between' in abs_le. - destruct abs_le as [lo_le le_hi]. - split. - - eapply Rle_trans. - Focus 2. apply lo_le. - repeat rewrite Rsub_eq_Ropp_Rplus. - apply Rplus_le_compat_r; auto. - - eapply Rle_trans. - apply le_hi. - apply Rplus_le_compat_r; auto. + unfold Rabs in abs_le. + destruct Rcase_abs in abs_le. + - rewrite Ropp_minus_distr in abs_le. + split; lra. + - lra. Qed. diff --git a/coq/IntervalArithQ.v b/coq/IntervalArithQ.v index b8069f0469308f91ed1965b874f1f1ac0c7400e4..9f06338c4e3b4ecf804507138cce1d3552c742d4 100644 --- a/coq/IntervalArithQ.v +++ b/coq/IntervalArithQ.v @@ -2,7 +2,7 @@ Formalization of real valued intv arithmetic TODO: Package this into a class or module that depends only on proving the existence of basic operators instead **) -Require Import Coq.QArith.QArith Coq.QArith.Qminmax. +Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.micromega.Psatz. Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RationalSimps. (** Define validity of an intv, requiring that the lower bound is less than or equal to the upper bound. @@ -156,6 +156,65 @@ Qed. Definition invertIntv (iv:intv) := mkIntv (/ ivhi iv) (/ ivlo iv). +(* +Lemma zero_not_contained_cases (iv:intv) : + ivlo iv <= ivhi iv -> ~ contained 0 iv -> ivhi iv < 0 \/ 0 < ivlo iv. +Proof. + unfold contained; destruct iv as [lo hi]; simpl; intros. + hnf in H0; rewrite Decidable.not_and_iff in H0. + case_eq (lo ?= 0); case_eq (hi ?= 0); intros. + - exfalso. + rewrite <- Qeq_alt in H1, H2. + apply H0; [rewrite H2; auto | rewrite H1; auto]; apply Qle_refl. + - rewrite <- Qlt_alt in H1. + rewrite <- Qeq_alt in H2. + rewrite H2 in H. + exfalso. + apply Qle_not_lt in H; auto. + - rewrite <- Qgt_alt in H1. + rewrite <- Qeq_alt in H2. + *) +Lemma Qinv_Qopp_compat (a:Q) : + / - a = - / a. +Proof. + unfold Qinv. + case_eq (Qnum a); intros; unfold Qopp; rewrite H; simpl; auto. +Qed. + +Lemma intv_inversion_valid (iv:intv) (a:Q) : + ivhi iv < 0 \/ 0 < ivlo iv -> contained a iv -> contained (/ a) (invertIntv iv). +Proof. + unfold contained; destruct iv as [ivlo ivhi]; simpl; + intros [ivhi_lt_zero | zero_lt_ivlo]; intros [ivlo_le_a a_le_ivhi]; + assert (ivlo <= ivhi) by (eapply Qle_trans; eauto); + split. + - assert (- / a <= - / ivhi). + + assert (0 < - ivhi) by lra. + repeat rewrite <- Qinv_Qopp_compat. + eapply Qle_shift_inv_l; try auto. + assert (- ivhi <= - a) by lra. + apply (Qmult_le_r _ 1 (- a)); try lra. + rewrite Qmult_1_l. + setoid_rewrite Qmult_comm at 1. + rewrite Qmult_assoc. + rewrite Qmult_inv_r; lra. + + apply Qopp_le_compat in H0; + repeat rewrite Qopp_involutive in H0; auto. + - assert (- / ivlo <= - / a). + + repeat rewrite <- Qinv_Qopp_compat. + eapply Qle_shift_inv_l; try lra. + apply (Qmult_le_r _ _ (- ivlo)); try lra. + rewrite Qmult_comm, Qmult_assoc, Qmult_inv_r, Qmult_1_l; lra. + + apply Qopp_le_compat in H0. + repeat rewrite Qopp_involutive in H0; auto. + - apply Qle_shift_inv_l; try lra. + apply (Qmult_le_r _ _ (ivhi)); try lra. + rewrite Qmult_comm, Qmult_assoc, Qmult_inv_r, Qmult_1_l; lra. + - apply Qle_shift_inv_l; try lra. + apply (Qmult_le_r _ _ a); try lra. + rewrite Qmult_comm, Qmult_assoc, Qmult_inv_r, Qmult_1_l; lra. +Qed. + Definition addIntv (iv1:intv) (iv2:intv) := absIvUpd Qplus iv1 iv2. @@ -286,4 +345,13 @@ Proof. Qed. Definition divideIntv (I1:intv) (I2:intv) := - multIntv I1 (mkIntv (/ (ivhi I2)) (/ (ivlo I2))). \ No newline at end of file + multIntv I1 (mkIntv (/ (ivhi I2)) (/ (ivlo I2))). + +Corollary divisionIsValid a b (I1:intv) (I2:intv) : + ivhi I2 < 0 \/ 0 < ivlo I2 -> contained a I1 -> contained b I2 -> contained (a / b) (divideIntv I1 I2). +Proof. + intros nodiv0 c_a c_b. + pose proof (intv_inversion_valid I2 b nodiv0 c_b). + unfold divideIntv, Qdiv. + apply intv_multiplication_valid; auto. +Qed. \ No newline at end of file diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 1e650dcd8974b29acd2af768f58341b11501a6ab..7da212288be37b8b2d872054be1817e3fe23c245 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -38,7 +38,10 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):= | Mult => let new_iv := multIntv iv1 iv2 in isSupersetIntv new_iv intv - | Div => false + | Div => + let nodiv0 := orb (Qleb (ivhi iv2) 0) (Qleb 0 (ivlo iv2)) in + let new_iv := divideIntv iv1 iv2 in + isSupersetIntv new_iv intv end in andb rec opres @@ -75,7 +78,6 @@ Proof. apply Is_true_eq_true; auto. Qed. - Corollary Q2R_max4 a b c d: Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d). Proof. @@ -257,5 +259,5 @@ Proof. repeat rewrite <- Q2R_mult in valid_mul_hi. rewrite <- Q2R_max4 in valid_mul_hi. unfold absIvUpd; auto. - + contradiction. + + 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