Commit 2cf1ff57 authored by Heiko Becker's avatar Heiko Becker

Prove interval arithmetic on rationals

parent 72273a09
......@@ -27,6 +27,15 @@ Arguments getErr _ /.
Definition intv:Type := Q * Q.
Definition error :Type := Q.
Definition mkIntv (ivlo:Q) (ivhi:Q) := (ivlo,ivhi).
Definition ivlo (intv:intv) := fst intv.
Definition ivhi (intv:intv) := snd intv.
Arguments mkIntv _ _/.
Arguments ivlo _ /.
Arguments ivhi _ /.
Definition precond :Type := nat -> intv.
(**
Define environment update function for arbitrary type as abbreviation.
This must be defined here, to prove some lemmas about expression evaluation.
......
......@@ -2,7 +2,7 @@ Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs.
Require Import Daisy.Infra.Abbrevs.
Definition Qleb :=Qle_bool.
Definition Qeqb := Qeq_bool.
(*
Definition Qc2Q (q:Qc) :Q := match q with
Qcmake a P => a end.
......@@ -54,4 +54,25 @@ Definition Qleb :=Qle_bool.
unfold Q2R at 1 in H.
unfold Qabs.
simpl.
*)
\ No newline at end of file
*)
Lemma Qsub_eq_Qopp_Qplus (a:Q) (b:Q) :
(a - b = a + (- b))%Q.
Proof.
field_simplify; reflexivity.
Qed.
(* Based on stdlib proof of reals *)
Lemma Qmult_le_compat_neg_l (r r1 r2:Q) :
r <= 0 -> r1 <= r2 -> r * r2 <= r * r1.
Proof.
intros. rewrite <- (Qopp_involutive r).
apply Qopp_le_compat in H.
assert (-0 == 0) by field.
rewrite H1 in H.
assert (forall a b, - a*b == - (a * b)) by (intros; field).
setoid_rewrite H2 at 1 2.
apply Qopp_le_compat.
setoid_rewrite Qmult_comm at 1 2.
apply Qmult_le_compat_r; auto.
Qed.
(**
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 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.
Containement is defined such that if x is contained in the intv, it must lie between the lower and upper bound.
**)
Definition valid (iv:intv) :Prop :=
(ivlo iv <= ivhi iv)%Q.
Definition contained (x:Q) (iv:intv) :=
(ivlo iv <= x <= ivhi iv)%Q.
Lemma contained_implies_valid (x:Q) (iv:intv) :
contained x iv ->
valid iv.
Proof.
unfold contained, valid; intros inIv; apply (Qle_trans _ x _); destruct inIv; auto.
Qed.
(**
Subset definition; when an intv is a subintv of another
**)
Definition isSupersetIntv (iv1:intv) (iv2:intv) :=
(ivlo iv2 <= ivlo iv1)%Q /\ (ivhi iv1 <= ivhi iv2)%Q.
Definition pointIntv (x:Q) := mkIntv x x.
Lemma contained_implies_subset (x:Q) (iv:intv):
contained x iv ->
isSupersetIntv (pointIntv x) iv.
Proof.
intros containedIv.
unfold contained, isSupersetIntv, pointIntv in *; destruct containedIv; split; auto.
Qed.
(**
Definition of validity conditions for intv operations, Addition, Subtraction, Multiplication and Division
**)
Definition validIntvAdd (iv1:intv) (iv2:intv) (iv3:intv) :=
forall a b, contained a iv1 -> contained b iv2 ->
contained (a + b) iv3.
Definition validIntvSub (iv1:intv) (iv2:intv) (iv3:intv) :=
forall a b, contained a iv1 -> contained b iv2 ->
contained (a - b) iv3.
Definition validIntvMult (iv1:intv) (iv2:intv) (iv3:intv) :=
forall a b, contained a iv1 -> contained b iv2 ->
contained (a * b) iv3.
Definition validIntvDiv (iv1:intv) (iv2:intv) (iv3:intv) :=
forall a b, contained a iv1 -> contained b iv2 ->
contained (a / b) iv3.
Lemma validPointIntv (a:Q) :
contained a (pointIntv a).
Proof.
unfold contained; split; simpl; apply Qle_refl; auto.
Qed.
(**
Now comes the old part with the computational definitions.
Where possible within time, they are shown sound with respect to the definitions from before, where not, we leave this as proof obligation for daisy.
**)
(**
TODO: Refactor into a list manipulating function instead
**)
Definition min4 (a:Q) (b:Q) (c:Q) (d:Q) := Qmin a (Qmin b (Qmin c d)).
Definition max4 (a:Q) (b:Q) (c:Q) (d:Q) := Qmax a (Qmax b (Qmax c d)).
Ltac Qmin_l := intros; apply Q.min_le_iff; left; apply Qle_refl.
Ltac Qmin_r := intros; apply Q.min_le_iff; right; apply Qle_refl.
Lemma min4_correct (a b c d:Q) :
(let m := min4 a b c d in
m <= a /\ m <= b /\ m <= c /\ m <= d)%Q.
Proof.
intros m.
repeat split; unfold m, min4.
- Qmin_l.
- assert (forall c, Qmin b c <= b)%Q by Qmin_l.
apply (Qle_trans _ (Qmin b (Qmin c d)) _); auto.
Qmin_r.
- assert (Qmin c d <= c)%Q by Qmin_l.
assert (Qmin b (Qmin c d) <= c)%Q.
+ apply (Qle_trans _ (Qmin c d) _); auto. Qmin_r.
+ apply (Qle_trans _ (Qmin b (Qmin c d)) _); auto. Qmin_r.
- assert (Qmin c d <= d)%Q by Qmin_r.
assert (Qmin b (Qmin c d) <= d)%Q.
+ apply (Qle_trans _ (Qmin c d) _); auto. Qmin_r.
+ apply (Qle_trans _ (Qmin b (Qmin c d)) _); auto. Qmin_r.
Qed.
Ltac Qmax_l := intros; apply Q.max_le_iff; left; apply Qle_refl.
Ltac Qmax_r := intros; apply Q.max_le_iff; right; apply Qle_refl.
Lemma max4_correct (a b c d:Q) :
(let m := max4 a b c d in
a <= m /\ b <= m /\ c <= m /\ d <= m)%Q.
Proof.
intros m.
repeat split; unfold m, max4.
- Qmax_l.
- assert (forall c, b <= Qmax b c)%Q by Qmax_l.
apply (Qle_trans _ (Qmax b (Qmax c d)) _); auto.
Qmax_r.
- assert (c <= Qmax c d)%Q by Qmax_l.
assert (c <= Qmax b (Qmax c d))%Q.
+ apply (Qle_trans _ (Qmax c d) _); auto. Qmax_r.
+ apply (Qle_trans _ (Qmax b (Qmax c d)) _); auto. Qmax_r.
- assert (d <= Qmax c d)%Q by Qmax_r.
assert (d <= Qmax b (Qmax c d))%Q.
+ apply (Qle_trans _ (Qmax c d) _); auto. Qmax_r.
+ apply (Qle_trans _ (Qmax b (Qmax c d)) _); auto. Qmax_r.
Qed.
(**
Asbtract intv update function, parametric by actual operator applied.
**)
Definition absIvUpd (op:Q->Q->Q) (I1:intv) (I2:intv) :=
(
min4 (op (ivlo I1) (ivlo I2))
(op (ivlo I1) (ivhi I2))
(op (ivhi I1) (ivlo I2))
(op (ivhi I1) (ivhi I2)),
max4 (op (ivlo I1) (ivlo I2))
(op (ivlo I1) (ivhi I2))
(op (ivhi I1) (ivlo I2))
(op (ivhi I1) (ivhi I2))
).
Definition widenIntv (Iv:intv) (v:Q) := mkIntv (ivlo Iv - v) (ivhi Iv + v).
Definition negateIntv (iv:intv) := mkIntv (- ivhi iv) (- ivlo iv).
Lemma intv_negation_valid (iv:intv) (a:Q) :
contained a iv-> contained (- a) (negateIntv iv).
Proof.
unfold contained; destruct iv as [ivlo ivhi]; simpl; intros [ivlo_le_a a_le_ivhi].
split; apply Qopp_le_compat; auto.
Qed.
Definition invertIntv (iv:intv) := mkIntv (/ ivhi iv) (/ ivlo iv).
Definition addIntv (iv1:intv) (iv2:intv) :=
absIvUpd Qplus iv1 iv2.
Lemma additionIsValid iv1 iv2:
validIntvAdd iv1 iv2 (addIntv iv1 iv2).
Proof.
unfold validIntvAdd.
intros a b.
unfold contained, addIntv, absIvUpd, min4, max4.
intros [lo_leq_a a_leq_hi] [lo_leq_b b_leq_hi].
simpl; split.
(** Lower Bound **)
- assert ( fst iv1 + fst iv2 <= a + b)%Q as lower_bound by (apply Qplus_le_compat; auto).
apply (Qle_trans _ (fst iv1 + fst iv2) _); [Qmin_l | auto].
(** Upper Bound **)
- assert (a + b <= snd iv1 + snd iv2)%Q as upper_bound by (apply Qplus_le_compat; auto).
apply (Qle_trans _ (snd iv1 + snd iv2) _); [ auto | ].
apply (Qle_trans _ (Qmax (fst iv1 + snd iv2) (Qmax (snd iv1 + fst iv2) (snd iv1 + snd iv2))) _);
[ | Qmax_r].
apply (Qle_trans _ (Qmax (snd iv1 + fst iv2) (snd iv1 + snd iv2)) _ ); [ | Qmax_r].
apply (Qle_trans _ (snd iv1 + snd iv2) _); [ apply Qle_refl; auto | Qmax_r].
Qed.
Definition substractIntv (I1:intv) (I2:intv) :=
addIntv I1 (negateIntv I2).
Corollary subtractionIsValid iv1 iv2:
validIntvSub iv1 iv2 (substractIntv iv1 iv2).
Proof.
unfold substractIntv.
intros a b.
intros contained_1 contained_I2.
rewrite Qsub_eq_Qopp_Qplus.
apply additionIsValid; auto.
apply intv_negation_valid; auto.
Qed.
(*
FIXME: This needs to be beautified
*)
Definition intv_mult_err (I1:intv) (e1:error) (I2:intv) (e2:error) :=
addIntv
(addIntv
(addIntv
(absIvUpd Qmult I1 I2)
(absIvUpd Qmult I1 (e1,e1)))
(absIvUpd Qmult I2 (e2,e2)))
(Qmult e1 e2, Qmult e1 e2).
Definition multIntv (iv1:intv) (iv2:intv) :=
absIvUpd Qmult iv1 iv2.
(**
Prove validity of multiplication for the intv lattice.
Prove is structurally the same as the proof done Jourdan et al. in Verasco, in FloatIntvsForward.v
TODO: Credit
**)
Lemma intv_multiplication_valid (I1:intv) (I2:intv) (a:Q) (b:Q) :
contained a I1 ->
contained b I2 ->
contained (a * b) (multIntv I1 I2).
Proof.
unfold contained, multIntv, absIvUpd, 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 (Qlt_le_dec a 0).
+ apply Qlt_le_weak in q.
destruct (Qlt_le_dec ivhi2 0).
* apply Qlt_le_weak in q0.
pose proof (Qmult_le_compat_neg_l a b ivhi2 q b_leq_hi) as ahi2_leq_ab.
pose proof (Qmult_le_compat_neg_l ivhi2 a ivhi1 q0 a_leq_hi) as hihi_leq_ahi2.
eapply Qle_trans.
apply leq_hihi. rewrite Qmult_comm.
eapply Qle_trans. apply hihi_leq_ahi2.
rewrite Qmult_comm; auto.
* eapply Qle_trans.
apply leq_lohi.
setoid_rewrite Qmult_comm at 1 2.
pose proof (Qmult_le_compat_r ivlo1 a ivhi2 lo_leq_a q0).
rewrite Qmult_comm.
eapply (Qle_trans).
apply H; auto.
rewrite Qmult_comm.
setoid_rewrite Qmult_comm at 1 2.
eapply (Qmult_le_compat_neg_l a); auto.
+ destruct (Qlt_le_dec ivlo2 0).
* eapply Qle_trans.
apply leq_hilo.
rewrite Qmult_comm.
eapply Qle_trans.
apply Qlt_le_weak in q0.
apply (Qmult_le_compat_neg_l ivlo2 a ivhi1 q0 a_leq_hi).
rewrite Qmult_comm.
setoid_rewrite Qmult_comm at 1 2.
eapply (Qmult_le_compat_r _ _ a); auto.
* eapply Qle_trans.
apply leq_lolo.
rewrite Qmult_comm.
apply (Qle_trans _ (ivlo2 * a)).
setoid_rewrite Qmult_comm at 1 2.
eapply (Qmult_le_compat_r _ _ ivlo2 ); auto.
rewrite Qmult_comm.
setoid_rewrite Qmult_comm at 1 2.
eapply (Qmult_le_compat_r _ _ a); auto.
- destruct (Qlt_le_dec a 0).
+ apply Qlt_le_weak in q.
eapply Qle_trans.
apply (Qmult_le_compat_neg_l a ivlo2); auto.
destruct (Qlt_le_dec ivlo2 0).
* rewrite Qmult_comm.
eapply Qle_trans.
eapply (Qmult_le_compat_neg_l ivlo2 ivlo1); auto.
apply Qlt_le_weak; auto.
rewrite Qmult_comm; auto.
* eapply Qle_trans.
eapply (Qmult_le_compat_r _ _ ivlo2); auto.
apply a_leq_hi.
apply hilo_leq.
+ rewrite Qmult_comm.
eapply Qle_trans.
eapply (Qmult_le_compat_r); auto.
apply b_leq_hi.
destruct (Qlt_le_dec ivhi2 0).
* eapply Qle_trans.
eapply (Qmult_le_compat_neg_l); auto.
apply Qlt_le_weak; auto.
apply lo_leq_a.
rewrite Qmult_comm; auto.
* eapply Qle_trans.
rewrite Qmult_comm.
eapply (Qmult_le_compat_r); auto.
apply a_leq_hi.
apply hihi_leq.
Qed.
Definition divideIntv (I1:intv) (I2:intv) :=
multIntv I1 (mkIntv (/ (ivhi I2)) (/ (ivlo I2))).
(*
Corollary intv_divisision_valid (I1:intv) (I2:intv) :
validIntvDiv I1 I2 (divideIntv I1 I2).
Proof.
unfold validIntvDiv.
intros a b contained_a contained_b; unfold divideIntv.
apply intv_multiplication_valid; auto.
unfold contained in *; simpl.
split. *)
Definition iv_div_err (I1:intv) (e1:error) (I2:intv) (e2:error) :=
intv_mult_err I1 e1 ( (/ ivlo (I2))%Q, (/ ivhi (I2))%Q) 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