Commit 3e5c79e4 authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove multiplication bound

parent b07718c2
This diff is collapsed.
Require Import Coq.Reals.Reals Coq.QArith.QArith.
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
(**
Some type abbreviations, to ease writing
**)
......@@ -25,7 +25,11 @@ Arguments getIntv _ /.
Arguments getErr _ /.
Definition intv:Type := Q * Q.
(*
Record Qpos : Type := mkQPos {Qposval:> Q; QposGeq0: Qle_bool 0 Qposval = true}. *)
Definition error :Type := Q.
(*
Coercion IntvOfErrors (p:error*error) := (Qposval (fst p),Qposval (snd p)):intv. *)
Definition mkIntv (ivlo:Q) (ivhi:Q) := (ivlo,ivhi).
Definition ivlo (intv:intv) := fst intv.
......
......@@ -43,8 +43,8 @@ Proof.
rewrite opp_IZR; lra.
Qed.
Lemma maxAbs_impl_RmaxAbs (iv:intv):
RmaxAbsFun iv = Q2R (maxAbs iv).
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.
......@@ -70,10 +70,13 @@ Proof.
- 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.
......@@ -163,4 +166,17 @@ Proof.
unfold machineEpsilon.
apply Qle_bool_iff.
unfold Qle_bool; auto.
Qed.
\ No newline at end of file
Qed.
(*
Lemma errorIsPos:
forall e:error, (0 <= Q2R e)%R.
Proof.
intros e.
unfold error in e.
pose proof (QposGeq0 e).
apply Qle_bool_iff in H.
apply Qle_Rle in H.
rewrite Q2R0_is_0 in H; auto.
Qed.
*)
\ No newline at end of file
......@@ -164,13 +164,13 @@ Proof.
apply (Rle_trans _ (snd iv1 + snd iv2) _); [ apply Req_le; auto | apply Rmax_r].
Qed.
Definition substractInterval (I1:interval) (I2:interval) :=
Definition subtractInterval (I1:interval) (I2:interval) :=
addInterval I1 (negateInterval I2).
Corollary subtractionIsValid iv1 iv2:
validIntervalSub iv1 iv2 (substractInterval iv1 iv2).
validIntervalSub iv1 iv2 (subtractInterval iv1 iv2).
Proof.
unfold substractInterval.
unfold subtractInterval.
intros a b.
intros contained_1 contained_I2.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -287,12 +287,12 @@ Proof.
Definition intv_div_err (I1:interval) (e1:err) (I2:interval) (e2:err) :=
interval_mult_err I1 e1 ( (/ IVlo (I2))%R, (/ IVhi (I2))%R) e2.
Definition RmaxAbsFun (iv:intv) :=
Rmax (Rabs (Q2R (fst iv))) (Rabs (Q2R (snd iv))).
Definition RmaxAbsFun (iv:interval) :=
Rmax (Rabs (fst iv)) (Rabs (snd iv)).
Lemma contained_leq_maxAbs a ivlo ivhi:
contained a (Q2R ivlo, Q2R ivhi) ->
(Rabs a <= RmaxAbsFun (ivlo, ivhi))%R.
Lemma contained_leq_maxAbs a iv:
contained a iv ->
(Rabs a <= RmaxAbsFun iv)%R.
Proof.
intros contained_a.
unfold RmaxAbsFun.
......@@ -300,19 +300,75 @@ Proof.
eapply RmaxAbs; auto.
Qed.
Lemma Rabs_error_bounded_maxAbs a b eps ivlo ivhi:
Lemma contained_leq_maxAbs_val a iv:
contained a iv ->
(a <= RmaxAbsFun (iv))%R.
Proof.
intros contained_a; unfold RmaxAbsFun.
assert (Rabs a <= RmaxAbsFun iv)%R by (apply contained_leq_maxAbs; auto).
eapply Rle_trans.
apply Rle_abs.
auto.
Qed.
Lemma contained_leq_maxAbs_neg_val a iv:
contained a iv ->
(- a <= RmaxAbsFun (iv))%R.
Proof.
intros contained_a; unfold RmaxAbsFun.
assert (Rabs a <= RmaxAbsFun iv)%R by (apply contained_leq_maxAbs; auto).
eapply Rle_trans.
apply Rle_abs.
rewrite Rabs_Ropp.
auto.
Qed.
Lemma Rabs_error_bounded_maxAbs a b eps iv:
(Rabs (a - b) <= eps)%R ->
contained a (Q2R ivlo, Q2R ivhi) ->
(Rabs b <= Rabs (RmaxAbsFun (ivlo, ivhi) + eps))%R.
contained a iv ->
(Rabs b <= Rabs (RmaxAbsFun iv + eps))%R.
Proof.
intros Rabs_le_eps contained_a.
pose proof (contained_leq_maxAbs _ _ _ contained_a).
pose proof (contained_leq_maxAbs _ _ contained_a).
rewrite Rabs_minus_sym in Rabs_le_eps.
assert (Rabs b - Rabs a <= eps)%R.
- eapply Rle_trans; [apply Rabs_triang_inv | auto].
- assert (Rabs b <= Rabs a + eps)%R by lra.
assert (Rabs a + eps <= RmaxAbsFun (ivlo, ivhi) + eps)%R by (apply Rplus_le_compat_r; auto).
assert (Rabs a + eps <= RmaxAbsFun iv + eps)%R by (apply Rplus_le_compat_r; auto).
eapply Rle_trans; eauto.
eapply Rle_trans; eauto.
apply Rle_abs.
Qed.
\ No newline at end of file
Qed.
Lemma lowerbound_iv a ivlo ivhi:
contained a (ivlo, ivhi) ->
(a >= Rmin (ivlo) (ivhi))%R.
Proof.
intros contained_a.
unfold contained in contained_a; destruct contained_a.
assert (ivlo <= ivhi)%R by (eapply Rle_trans; eauto).
apply Rle_ge.
eapply Rle_trans.
apply Rmin_l.
auto.
Qed.
Lemma distance_gives_iv a b e iv:
contained a iv ->
(Rabs (a - b) <= e)%R ->
contained b (widenInterval iv e).
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.
Qed.
-R . Daisy
./IntervalValidation.v
./Expressions.v
./AbsoluteError.v
./Infra/RealSimps.v
./Infra/Abbrevs.v
./Infra/ExpressionAbbrevs.v
./Infra/RationalConstruction.v
./Infra/RealRationalProps.v
./Infra/RealConstruction.v
./Infra/RationalSimps.v
./Commands.v
./ErrorValidation.v
./IntervalArithQ.v
./IntervalArith.v
./ErrorBounds.v
./VerificationTests/SimpleDoppler.v
./VerificationTests/SimpleMultiplication.v
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