Commit 139f71f7 authored by Heiko Becker's avatar Heiko Becker
Browse files

More work on Division. Can prove doppler bounds, proof somewhere in between

parent f09a169d
This diff is collapsed.
......@@ -65,33 +65,3 @@ Lemma equal_naming a b c d:
Proof.
unfold Qplus, Qeq; auto.
Qed.
(* TODO: Remove me
Lemma foo a b:
(a < b)%positive ->
(Z.neg a < ' b)%Z.
Proof.
intros.
rewrite <- Pos.ltb_lt in H.
rewrite Pos2Z.inj_ltb in H.
rewrite Z.ltb_lt in H.
apply (Z.lt_trans _ (' a)); try auto.
pose proof (Pos2Z.is_pos a).
apply (Z.lt_trans _ 0); try auto.
Qed.
*)
Lemma Qle_Qneq_equals_Qlt a b:
Qleb a b && (negb (Qeq_bool a b)) = true ->
(a < b).
Proof.
intros le_and_neq.
andb_to_prop le_and_neq.
apply Qle_bool_iff in L.
assert (Qeq_bool a b = false).
- case_eq (Qeq_bool a b); unfold negb in R; intros; try auto.
rewrite H in R. auto.
- apply Qeq_bool_neq in H.
apply Qle_lteq in L.
destruct L; firstorder.
Qed.
......@@ -25,7 +25,7 @@ Lemma Q2R1:
(Q2R 1 = 1)%R.
Proof.
unfold Q2R; simpl; lra.
Qed.
Qed.
Lemma Rabs_eq_Qabs:
forall x, Rabs (Q2R x) = Q2R (Qabs x).
......@@ -54,52 +54,6 @@ Proof.
rewrite opp_IZR; lra.
Qed.
Lemma maxAbs_impl_RmaxAbs (ivlo:Q) (ivhi:Q):
RmaxAbsFun (Q2R ivlo, Q2R ivhi) = Q2R (maxAbs (ivlo, ivhi)).
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.
simpl in *.
repeat rewrite Rabs_eq_Qabs.
subst; auto.
- intros fst_le_snd.
apply Qle_Rle in fst_le_snd.
apply Rmax_right in fst_le_snd.
simpl in *; repeat rewrite Rabs_eq_Qabs.
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.
......@@ -162,6 +116,37 @@ Proof.
rewrite H; auto.
Qed.
Lemma maxAbs_impl_RmaxAbs (ivlo:Q) (ivhi:Q):
RmaxAbsFun (Q2R ivlo, Q2R ivhi) = Q2R (maxAbs (ivlo, ivhi)).
Proof.
unfold RmaxAbsFun, maxAbs.
simpl; repeat rewrite Rabs_eq_Qabs.
rewrite Q2R_max; auto.
Qed.
Definition Q2RP (iv:Q*Q) :=
let (lo,hi) := iv in (Q2R lo, Q2R hi).
Corollary maxAbs_impl_RmaxAbs_iv iv:
RmaxAbsFun (Q2RP iv) = Q2R (maxAbs iv).
Proof.
unfold Q2RP; destruct iv; apply maxAbs_impl_RmaxAbs.
Qed.
Lemma minAbs_impl_RminAbs (ivlo ivhi:Q) :
RminAbsFun (Q2R ivlo, Q2R ivhi) = Q2R (minAbs (ivlo, ivhi)).
Proof.
unfold RminAbsFun, minAbs; simpl.
repeat rewrite Rabs_eq_Qabs.
rewrite Q2R_min; auto.
Qed.
Corollary minAbs_impl_RminAbs_iv iv:
RminAbsFun (Q2RP iv) = Q2R (minAbs iv).
Proof.
unfold Q2RP; destruct iv; apply minAbs_impl_RminAbs.
Qed.
Lemma mEps_eq_Rmeps:
Q2R RationalSimps.machineEpsilon = RealSimps.machineEpsilon.
Proof.
......@@ -196,44 +181,75 @@ Proof.
unfold Qle_bool; auto.
Qed.
Lemma equal_naming a b:
(a = 0 -> False)%R ->
(b = 0 -> False)%R ->
(1 / a - 1 / b = (b - a) / (a * b))%R.
Lemma positive_inversion_error_prop v err:
(0 <= err)%R ->
(0 < v)%R ->
(0 < (v - err))%R ->
( /(v - err) - (/v) <= (/ ((v - err) * (v - err))) * err)%R.
Proof.
intros.
rewrite Rdiv_minus_distr.
intros err_pos v_neq_0 verr_neq_0.
assert (v - err <= v)%R as verr_lt_v by lra.
rewrite Rsub_eq_Ropp_Rplus.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
rewrite <- Rsub_eq_Ropp_Rplus.
assert (v - err - v = - err)%R as v_simp by lra.
rewrite v_simp.
assert (0 < (v - err) * v)%R by (apply Rmult_0_lt_preserving; auto).
assert (0 < (v - err) * (v - err))%R by (apply Rmult_0_lt_preserving; auto).
unfold Rdiv.
rewrite Rinv_mult_distr; try auto.
setoid_rewrite Rmult_comm at 4.
repeat rewrite <- Rmult_assoc.
repeat rewrite <- Rinv_r_sym; try auto.
rewrite Rmult_comm.
repeat rewrite <- (Ropp_mult_distr_r).
rewrite <- Ropp_inv_permute; try lra.
rewrite <- (Ropp_mult_distr_l).
rewrite Ropp_involutive.
apply Rmult_le_compat_r; try lra.
apply Rinv_le_contravar; try lra.
apply Rmult_le_compat_l; lra.
Qed.
Lemma negative_inversion_error_prop v err:
(0 <= err)%R ->
(v < 0)%R ->
((v + err) < 0)%R ->
( / v - (/ (v + err)) <= (/ ((v + err) * (v + err))) * err)%R.
Proof.
intros err_pos v_neq_0 verr_neq_0.
assert (0 < - v)%R as opp_v by lra.
assert (0 < - v - err)%R as opp_verr by lra.
pose proof (positive_inversion_error_prop (- v) err err_pos opp_v opp_verr) as the_goal.
assert (/ (- v - err) - / - v = / v - / (v + err))%R as eq.
- setoid_rewrite Rsub_eq_Ropp_Rplus at 2; rewrite <- Ropp_plus_distr.
repeat (rewrite <- Ropp_inv_permute; try lra).
- rewrite eq in the_goal.
assert (- v - err = - (v + err))%R as v_err_opp by lra.
repeat rewrite v_err_opp in the_goal.
rewrite <- Ropp_mult_distr_r, <- Ropp_mult_distr_l in the_goal.
rewrite Ropp_involutive in the_goal.
assumption.
Qed.
Lemma minAbs_positive_iv_is_lo a b:
(0 < a)%R ->
(a <= b)%R ->
RminAbsFun (a,b) = a.
Proof.
intros; unfold RminAbsFun; simpl.
assert (0 < b)%R by lra.
assert (Rabs a = a)%R as Rabs_pos_a by (apply Rabs_right; lra).
assert (Rabs b = b)%R as Rabs_pos_b by (apply Rabs_right; lra).
rewrite Rabs_pos_a, Rabs_pos_b.
rewrite Rmin_left; lra.
Qed.
Lemma inv_err_prop vR vF err:
(Rabs (vR - vF) <= err)%R ->
(0 < vR)%R ->
(0 < vF)%R ->
(vF < vR)%R ->
(((/ vR) - (/ vF)) <= (/ (vF * vF)) * err)%R.
Lemma minAbs_negative_iv_is_hi a b:
(b < 0)%R ->
(a <= b)%R ->
(RminAbsFun (a,b) = - b)%R.
Proof.
intros err_diff vR_neq_0 nF_neq_0 vF_lt_vR.
assert (/ vR = 1 / vR)%R by lra.
assert (/ vF = 1/ vF)%R by lra.
rewrite H, H0.
rewrite equal_naming; try lra.
assert (0 < vF * vR)%R by admit.
pose proof (Rinv_lt_contravar vF vR H1 vF_lt_vR).
apply (Rle_trans _ (/ (vF * vF) * (vF - vR)))%R.
- unfold Rdiv. rewrite Rmult_comm.
apply Rmult_le_compat_r; try lra.
+ admit.
+ apply Rinv_le_contravar.
* admit.
* apply Rmult_le_compat_r; lra.
- apply Rmult_le_compat_l.
+ rewrite Rinv_mult_distr; try lra.
admit.
+ assert (- (vR - vF) < 0)%R by lra.
unfold Rabs in err_diff; destruct Rcase_abs in err_diff; try lra.
Admitted.
\ No newline at end of file
intros; unfold RminAbsFun; simpl.
assert (Rabs a = - a)%R as Rabs_neg_a by (apply Rabs_left; lra).
assert (Rabs b = - b)%R as Rabs_neg_b by (apply Rabs_left; lra).
rewrite Rabs_neg_a, Rabs_neg_b.
rewrite Rmin_right; lra.
Qed.
\ No newline at end of file
......@@ -86,4 +86,54 @@ Lemma RmaxAbs_peel_Rabs a b:
Rmax (Rabs a) (Rabs b) = Rabs (Rmax (Rabs a) (Rabs b)).
Proof.
apply Rmax_case_strong; intros; rewrite Rabs_Rabsolu; auto.
Qed.
Lemma equal_naming a b c d:
(b = 0 -> False)%R ->
(d = 0 -> False)%R ->
(a / b + c / d = (a * d + c * b) / (b * d))%R.
Proof.
intros b_neq_zero d_neq_zero.
rewrite Rdiv_plus_distr.
unfold Rdiv.
repeat (rewrite Rinv_mult_distr; try auto).
setoid_rewrite (Rmult_comm (/b) (/d)) at 1.
repeat rewrite <- Rmult_assoc.
repeat (rewrite Rinv_r_simpl_l; try auto).
Qed.
Lemma inv_eq_1_div a:
(/ a = 1 / a)%R.
Proof.
lra.
Qed.
Lemma equal_naming_inv a b:
(a = 0 -> False)%R ->
(b = 0 -> False)%R ->
(/ a + / b = (a + b) / (a * b))%R.
Proof.
repeat rewrite inv_eq_1_div.
intros; rewrite equal_naming; auto.
lra.
Qed.
Lemma Rmult_0_lt_preserving a b:
(0 < a)%R ->
(0 < b)%R ->
(0 < a * b)%R.
Proof.
intros; rewrite <- (Rmult_0_l 0); apply Rmult_le_0_lt_compat; lra.
Qed.
Lemma Rmult_lt_0_inverting a b:
(a < 0)%R ->
(b < 0)%R ->
(0 < a * b)%R.
Proof.
intros.
rewrite <- (Ropp_involutive (a * b)).
rewrite Ropp_mult_distr_r, Ropp_mult_distr_l.
rewrite <- (Rmult_0_l 0).
apply Rmult_le_0_lt_compat; lra.
Qed.
\ No newline at end of file
......@@ -299,6 +299,9 @@ Qed.
Definition RmaxAbsFun (iv:interval) :=
Rmax (Rabs (fst iv)) (Rabs (snd iv)).
Definition RminAbsFun (iv:interval) :=
Rmin (Rabs (fst iv)) (Rabs (snd iv)).
Lemma contained_leq_maxAbs a iv:
contained a iv ->
(Rabs a <= RmaxAbsFun iv)%R.
......@@ -375,4 +378,4 @@ Proof.
- rewrite Ropp_minus_distr in abs_le.
split; lra.
- lra.
Qed.
Qed.
\ No newline at end of file
......@@ -3,6 +3,7 @@
Used in soundness proofs and computations of range validator.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.micromega.Psatz.
Require Import Coq.ZArith.ZArith.
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.
......
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