Commit bf0162f3 authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove multiplication correct with help of Jaques Henri

parent 4795737c
......@@ -11,7 +11,7 @@ Definition abs_env:Type := exp R -> interval -> err -> Prop.
First define when given an interval and an error, when another error is sound overapproximation of the absolute error
**)
Definition isSoundErr (error:err) (iv:intv) (propagatedErr:err) :=
(error >= m_eps * Rmax (Rabs (IVlo(iv) - propagatedErr)) (Rabs (IVhi(iv) + propagatedErr)))%R.
(error >= machineEpsilon * Rmax (Rabs (IVlo(iv) - propagatedErr)) (Rabs (IVhi(iv) + propagatedErr)))%R.
Definition maxAbs (IV:intv) := Rmax (Rabs (IVlo IV)) (Rabs (IVhi IV)).
......@@ -52,11 +52,11 @@ end.
Inductive AbsErrExp : exp R -> abs_env -> err -> Prop :=
AbsErrConst n iv e (env:abs_env):
env (Const n) (iv) e ->
isSoundErr e iv m_eps ->
isSoundErr e iv machineEpsilon ->
AbsErrExp (Const n) env e
|AbsErrVar v iv e (env:abs_env):
env (Var R v) iv e ->
isSoundErr e iv m_eps ->
isSoundErr e iv machineEpsilon ->
AbsErrExp (Var R v) env e
|AbsErrBinop op e1 iv1 er1 e2 iv2 er2 iv eabs (env:abs_env):
env e1 iv1 er1 ->
......
......@@ -6,7 +6,8 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.abbrevs.
(**
Intervals are a type, consisting of a pair of two real numbers
Additionally add some constructing and destructing definitions for encapsulation and define them to automatically unfold upon simplification.
Additionally add some constructing and destructing definitions for encapsulation and
define them to automatically unfold upon simplification.
**)
Definition interval:Type := R * R.
Definition mkInterval (ivlo:R) (ivhi:R) := (ivlo,ivhi).
......@@ -36,7 +37,7 @@ Qed.
(**
Subset definition; when an interval is a subinterval of another
**)
**)
Definition isSupersetInterval (iv1:interval) (iv2:interval) :=
(IVlo iv2 <= IVlo iv1)%R /\ (IVhi iv1 <= IVhi iv2)%R.
......@@ -70,7 +71,7 @@ Definition validIntervalDiv (iv1:interval) (iv2:interval) (iv3:interval) :=
contained (a / b) iv3.
Lemma validPointInterval (a:R) :
contained a (mkInterval a a).
contained a (pointInterval a).
Proof.
unfold contained; split; simpl; apply Req_le; auto.
Qed.
......@@ -86,6 +87,46 @@ Qed.
Definition min4 (a:R) (b:R) (c:R) (d:R) := Rmin a (Rmin b (Rmin c d)).
Definition max4 (a:R) (b:R) (c:R) (d:R) := Rmax a (Rmax b (Rmax c d)).
Lemma min4_correct (a b c d:R) :
(let m := min4 a b c d in
m <= a /\ m <= b /\ m <= c /\ m <= d)%R.
Proof.
intros m.
repeat split; unfold m, min4.
- apply Rmin_l.
- assert (forall c, Rmin b c <= b)%R by (apply Rmin_l).
apply (Rle_trans _ (Rmin b (Rmin c d)) _); auto.
apply Rmin_r.
- assert (Rmin c d <= c)%R by (apply Rmin_l).
assert (Rmin b (Rmin c d) <= c)%R.
+ apply (Rle_trans _ (Rmin c d) _); auto. apply Rmin_r.
+ apply (Rle_trans _ (Rmin b (Rmin c d)) _); auto. apply Rmin_r.
- assert (Rmin c d <= d)%R by (apply Rmin_r).
assert (Rmin b (Rmin c d) <= d)%R.
+ apply (Rle_trans _ (Rmin c d) _); auto. apply Rmin_r.
+ apply (Rle_trans _ (Rmin b (Rmin c d)) _); auto. apply Rmin_r.
Qed.
Lemma max4_correct (a b c d:R) :
(let m := max4 a b c d in
a <= m /\ b <= m /\ c <= m /\ d <= m)%R.
Proof.
intros m.
repeat split; unfold m, max4.
- apply Rmax_l.
- assert (forall c, b <= Rmax b c)%R by (apply Rmax_l).
apply (Rle_trans _ (Rmax b (Rmax c d)) _); auto.
apply Rmax_r.
- assert (c <= Rmax c d)%R by (apply Rmax_l).
assert (c <= Rmax b (Rmax c d))%R.
+ apply (Rle_trans _ (Rmax c d) _); auto. apply Rmax_r.
+ apply (Rle_trans _ (Rmax b (Rmax c d)) _); auto. apply Rmax_r.
- assert (d <= Rmax c d)%R by (apply Rmax_r).
assert (d <= Rmax b (Rmax c d))%R.
+ apply (Rle_trans _ (Rmax c d) _); auto. apply Rmax_r.
+ apply (Rle_trans _ (Rmax b (Rmax c d)) _); auto. apply Rmax_r.
Qed.
(**
Asbtract interval update function, parametric by actual operator applied.
**)
......@@ -165,216 +206,84 @@ Definition interval_mult_err (I1:interval) (e1:err) (I2:intv) (e2:err) :=
Definition multInterval (iv1:interval) (iv2:interval) :=
absIntvUpd Rmult iv1 iv2.
Definition absOpMin (op:R -> R -> R) (I1:interval) (I2:interval) :=
min4 (op (IVlo I1) (IVlo I2))
(op (IVlo I1) (IVhi I2))
(op (IVhi I1) (IVlo I2))
(op (IVhi I1) (IVhi I2)).
Definition absOpMax (op:R -> R -> R) (I1:interval) (I2:interval) :=
max4 (op (IVlo I1) (IVlo I2))
(op (IVlo I1) (IVhi I2))
(op (IVhi I1) (IVlo I2))
(op (IVhi I1) (IVhi I2)).
Lemma min_gt_0 (iv1:interval) (iv2:interval) :
valid iv1 ->
valid iv2 ->
(0 <= IVlo iv1)%R ->
(0 <= IVlo iv2)%R ->
absOpMin (Rmult) iv1 iv2 = (IVlo iv1 * IVlo iv2)%R.
(**
Prove validity of multiplication for the interval lattice.
Prove is structurally the same as the proof done Jourdan et al. in Verasco, in FloatIntervalsForward.v
TODO: Credit
**)
Lemma multiplicationIsValid (I1:interval) (I2:interval) (a:R) (b:R) :
contained a I1 ->
contained b I2 ->
contained (a * b) (multInterval I1 I2).
Proof.
intros valid_iv1 valid_iv2 geq0_1 geq0_2.
unfold absOpMin, min4, Rmin; destruct Rle_dec; auto.
exfalso.
apply n.
destruct Rle_dec.
- apply Rmult_le_compat; auto.
apply Req_le; auto.
- destruct Rle_dec; apply Rmult_le_compat; auto.
apply Req_le; auto.
unfold contained, multInterval, absIntvUpd, IVlo, IVhi.
destruct I1 as [ivlo1 ivhi1]; destruct I2 as [ivlo2 ivhi2]; simpl.
intros [lo_leq_a a_leq_hi] [lo_leq_b b_leq_hi].
pose proof (min4_correct (ivlo1 * ivlo2) (ivlo1 * ivhi2) (ivhi1 * ivlo2) (ivhi1 * ivhi2))
as [leq_lolo [leq_lohi [leq_hilo leq_hihi]]];
pose proof (max4_correct (ivlo1 * ivlo2) (ivlo1 * ivhi2) (ivhi1 * ivlo2) (ivhi1 * ivhi2))
as [lolo_leq [lohi_leq [hilo_leq hihi_leq]]].
split.
(* Lower Bound *)
- destruct (Rle_lt_dec a 0).
+ destruct (Rle_lt_dec ivhi2 0).
* pose proof (Rmult_le_compat_neg_l a b ivhi2 r b_leq_hi) as ahi2_leq_ab.
pose proof (Rmult_le_compat_neg_l ivhi2 a ivhi1 r0 a_leq_hi) as hihi_leq_ahi2.
eapply Rle_trans.
apply leq_hihi. rewrite Rmult_comm.
eapply Rle_trans. apply hihi_leq_ahi2.
rewrite Rmult_comm; auto.
* eapply Rle_trans.
apply leq_lohi.
apply Rlt_le in r0.
pose proof (Rmult_le_compat_l ivhi2 ivlo1 a).
rewrite Rmult_comm.
eapply (Rle_trans). apply H; auto.
rewrite Rmult_comm.
eapply (Rmult_le_compat_neg_l a); auto.
+ destruct (Rle_lt_dec ivlo2 0).
* eapply Rle_trans.
apply leq_hilo.
rewrite Rmult_comm.
eapply Rle_trans.
apply (Rmult_le_compat_neg_l ivlo2 a ivhi1 r0 a_leq_hi).
rewrite Rmult_comm.
eapply (Rmult_le_compat_l a); auto.
exact (Rlt_le _ _ r).
* eapply Rle_trans.
apply leq_lolo.
apply Rlt_le in r; apply Rlt_le in r0.
rewrite Rmult_comm.
apply (Rle_trans _ (ivlo2 * a)).
eapply (Rmult_le_compat_l ivlo2 ); auto.
rewrite Rmult_comm.
eapply (Rmult_le_compat_l a); auto.
- destruct (Rle_lt_dec a 0).
+ eapply Rle_trans.
apply (Rmult_le_compat_neg_l a ivlo2); auto.
destruct (Rle_lt_dec ivlo2 0).
* rewrite Rmult_comm.
eapply Rle_trans.
eapply (Rmult_le_compat_neg_l ivlo2 ivlo1); auto.
rewrite Rmult_comm; auto.
* rewrite Rmult_comm.
eapply Rle_trans.
eapply (Rmult_le_compat_l ivlo2 a ivhi1); auto.
apply Rlt_le; auto.
rewrite Rmult_comm; auto.
+ eapply Rle_trans.
apply (Rmult_le_compat_l) with (r2 := ivhi2); auto.
apply Rlt_le; auto.
destruct (Rle_lt_dec ivhi2 0).
* rewrite Rmult_comm. eapply Rle_trans.
eapply (Rmult_le_compat_neg_l) with (r1:= ivlo1); auto.
rewrite Rmult_comm; auto.
* rewrite Rmult_comm; eapply Rle_trans.
apply (Rmult_le_compat_l) with (r2 := ivhi1); auto.
apply Rlt_le; auto.
rewrite Rmult_comm; auto.
Qed.
Lemma max_gt_0 (iv1:interval) (iv2:interval) :
valid iv1 ->
valid iv2 ->
(0 <= IVlo iv1)%R ->
(0 <= IVlo iv2)%R ->
absOpMax (Rmult) iv1 iv2 = (IVhi iv1 * IVhi iv2)%R.
Proof.
intros valid_iv1 valid_iv2 geq0_1 geq0_2.
unfold absOpMax, max4, Rmax; destruct Rle_dec.
- destruct Rle_dec.
+ destruct Rle_dec; auto.
exfalso.
apply n.
apply Rmult_le_compat; auto.
* apply (Rle_trans _ (IVlo iv1) _); auto.
* apply Req_le; auto.
+ exfalso; apply n.
destruct Rle_dec.
* apply Rmult_le_compat; auto; [apply (Rle_trans _ (IVlo iv2) _); auto | apply Req_le; auto].
* exfalso; apply n0; apply Rmult_le_compat; auto; [ apply (Rle_trans _ (IVlo iv1) _); auto | apply Req_le; auto].
- exfalso.
apply n.
destruct Rle_dec.
+ destruct Rle_dec.
* apply Rmult_le_compat; auto.
* apply Rmult_le_compat; auto.
apply Req_le; auto.
+ apply Rmult_le_compat; auto.
apply Req_le; auto.
Qed.
Definition intv_div_err (I1:interval) (e1:err) (I2:interval) (e2:err) :=
interval_mult_err I1 e1 ( (/ IVlo (I2))%R, (/ IVhi (I2))%R) e2.
(**
Useful Lemmata:
Rinv_mult_simpl:
forall r1 r2 r3 : R,
r1 <> 0%R -> (r1 * / r2 * (r3 * / r1))%R = (r3 * / r2)%R
Rmult_lt_compat_r:
forall r r1 r2 : R, (0 < r)%R -> (r1 < r2)%R -> (r1 * r < r2 * r)%R
Rmult_gt_compat_r:
forall r r1 r2 : R, (r > 0)%R -> (r1 > r2)%R -> (r1 * r > r2 * r)%R
Rmult_gt_compat_l:
forall r r1 r2 : R, (r > 0)%R -> (r1 > r2)%R -> (r * r1 > r * r2)%R
Rmult_le_compat_l:
forall r r1 r2 : R, (0 <= r)%R -> (r1 <= r2)%R -> (r * r1 <= r * r2)%R
Rmult_le_compat_r:
forall r r1 r2 : R, (0 <= r)%R -> (r1 <= r2)%R -> (r1 * r <= r2 * r)%R
Rmult_ge_compat_l:
forall r r1 r2 : R, (r >= 0)%R -> (r1 >= r2)%R -> (r * r1 >= r * r2)%R
Rmult_ge_compat_r:
forall r r1 r2 : R, (r >= 0)%R -> (r1 >= r2)%R -> (r1 * r >= r2 * r)%R
Rmult_le_compat:
forall r1 r2 r3 r4 : R,
(0 <= r1)%R ->
(0 <= r3)%R -> (r1 <= r2)%R -> (r3 <= r4)%R -> (r1 * r3 <= r2 * r4)%R
Rmult_ge_compat:
forall r1 r2 r3 r4 : R,
(r2 >= 0)%R ->
(r4 >= 0)%R -> (r1 >= r2)%R -> (r3 >= r4)%R -> (r1 * r3 >= r2 * r4)%R
Rmult_gt_0_lt_compat:
forall r1 r2 r3 r4 : R,
(r3 > 0)%R ->
(r2 > 0)%R -> (r1 < r2)%R -> (r3 < r4)%R -> (r1 * r3 < r2 * r4)%R
Rmult_le_0_lt_compat:
forall r1 r2 r3 r4 : R,
(0 <= r1)%R ->
(0 <= r3)%R -> (r1 < r2)%R -> (r3 < r4)%R -> (r1 * r3 < r2 * r4)%R
Rmult_lt_0_compat:
forall r1 r2 : R, (0 < r1)%R -> (0 < r2)%R -> (0 < r1 * r2)%R
Rmult_gt_0_compat:
forall r1 r2 : R, (r1 > 0)%R -> (r2 > 0)%R -> (r1 * r2 > 0)%R
Rmult_le_compat_neg_l:
forall r r1 r2 : R, (r <= 0)%R -> (r1 <= r2)%R -> (r * r2 <= r * r1)%R
Rmult_le_ge_compat_neg_l:
forall r r1 r2 : R, (r <= 0)%R -> (r1 <= r2)%R -> (r * r1 >= r * r2)%R
Rmult_lt_gt_compat_neg_l:
forall r r1 r2 : R, (r < 0)%R -> (r1 < r2)%R -> (r * r1 > r * r2)%R
**)
(**
Lemma IntervalMultMono (I1:interval) (I2:interval) (a:R) (b:R) :
contained I1 a ->
contained I2 b ->
contained (interval_mult I1 I2) (a * b).
Proof.
unfold contained, interval_mult, absIntervalUpd, IVlo, IVhi;
destruct I1 as [ivlo1 ivhi1]; destruct I2 as [ivlo2 ivhi2]; simpl.
intros [ lo_leq_a a_leq_hi] [lo_leq_b b_leq_hi].
assert (ivlo1 <= ivhi1)%R by (apply (Rle_trans _ a _); auto).
assert (ivlo2 <= ivhi2)%R by (apply (Rle_trans _ b _); auto).
destruct (Rle_dec ivhi1 0); destruct (Rle_dec ivhi2 0);
[(* Both less do no further case distinction *)
assert (ivlo1 <= 0)%R by (apply (Rle_trans _ (ivhi1) _); auto);
assert (ivlo2 <= 0)%R by (apply (Rle_trans _ (ivhi2) _); auto)
| (* Fst one less, destruct second one *)
assert (ivlo1 <= 0)%R by (apply (Rle_trans _ (ivhi1) _); auto);
destruct (Rle_dec ivlo2 0)
| (* Opposite case *)
assert (ivlo2 <= 0)%R by (apply (Rle_trans _ (ivhi2) _); auto);
destruct (Rle_dec ivlo1 0)
| (* Both greater -> both destruct *)
destruct (Rle_dec ivlo2 0); destruct (Rle_dec ivlo1 0) ].
-
(*
First subcase, all intervals negative --> ivhi1 * ivhi2 is maximum
Rmult_le_compat_neg_l b a ivhi1
Rmult_le_compat_neg_l ivlo1 b ivhi2
*)
assert (b <= 0)%R as b_leq_0 by (apply (Rle_trans _ (ivhi2) _); auto).
split.
+ pose proof (Rmult_le_compat_neg_l b a ivhi1 b_leq_0 a_leq_hi).
pose proof (Rmult_le_compat_neg_l ivhi1 b ivhi2 r b_leq_hi).
rewrite Rmult_comm in H3.
pose proof (Rle_trans _ _ _ H4 H3).
rewrite (Rmult_comm a b).
unfold min4.
assert
(Rmin (ivlo1 * ivlo2)
(Rmin (ivlo1 * ivhi2) (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2))) <= ivhi1 * ivhi2)%R.
* assert (Rmin (ivlo1 * ivhi2) (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2)) <= ivhi1 * ivhi2)%R.
{
assert (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2) <= ivhi1 * ivhi2)%R by apply Rmin_r.
apply (Rle_trans _ (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2)) _); auto.
apply Rmin_r.
}
{
apply (Rle_trans _ (Rmin (ivlo1 * ivhi2) (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2))) _); auto.
apply Rmin_r.
}
* apply (Rle_trans _ (ivhi1 * ivhi2) _); auto.
+ unfold max4.
apply Rge_le.
pose proof (Rmult_le_ge_compat_neg_l ivlo1 ivlo2 b H1 lo_leq_b).
pose proof (Rmult_le_ge_compat_neg_l b ivlo1 a b_leq_0 lo_leq_a).
rewrite Rmult_comm in H4.
pose proof (Rge_trans _ _ _ H3 H4).
rewrite (Rmult_comm a b).
apply (Rge_trans _ (ivlo1 * ivlo2) _); auto.
apply Rle_ge, Rmax_l.
- assert (a <= 0)%R as a_leq_0 by (apply (Rle_trans _ (ivhi1) _); auto).
split.
+ apply Rnot_le_gt in n.
apply Rgt_ge in n.
pose proof (Rmult_le_compat_neg_l a b ivhi2).
pose proof (Rmult_le_compat_neg_l ivhi1).
rewrite Rmult_comm in H3.
pose proof (Rle_trans _ _ _ H4 H3).
rewrite (Rmult_comm a b).
unfold min4.
assert
(Rmin (ivlo1 * ivlo2)
(Rmin (ivlo1 * ivhi2) (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2))) <= ivhi1 * ivhi2)%R.
* assert (Rmin (ivlo1 * ivhi2) (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2)) <= ivhi1 * ivhi2)%R.
{
assert (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2) <= ivhi1 * ivhi2)%R by apply Rmin_r.
apply (Rle_trans _ (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2)) _); auto.
apply Rmin_r.
}
{
apply (Rle_trans _ (Rmin (ivlo1 * ivhi2) (Rmin (ivhi1 * ivlo2) (ivhi1 * ivhi2))) _); auto.
apply Rmin_r.
}
* apply (Rle_trans _ (ivhi1 * ivhi2) _); auto.
+ unfold max4.
apply Rge_le.
pose proof (Rmult_le_ge_compat_neg_l ivlo1 ivlo2 b H1 lo_leq_b).
pose proof (Rmult_le_ge_compat_neg_l b ivlo1 a b_leq_0 lo_leq_a).
rewrite Rmult_comm in H4.
pose proof (Rge_trans _ _ _ H3 H4).
rewrite (Rmult_comm a b).
apply (Rge_trans _ (ivlo1 * ivlo2) _); auto.
apply Rle_ge, Rmax_l.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
**)
\ No newline at end of file
interval_mult_err I1 e1 ( (/ IVlo (I2))%R, (/ IVhi (I2))%R) e2.
\ No newline at end of file
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