Add LoadPath "./interval". Require Import Fourier Rdefinitions Raxioms RIneq Rbasic_fun R_Ifp. Require Import ssreflect ssrbool eqtype ssrfun seq fintype bigops ssralg. Require Import Rstruct min_max. Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. Open Scope ring_scope. Open Scope R_scope. Delimit Scope R_scope with Re. (* - defintion of an interval structure; - closed intervals are a pair inf, sup with inf <= sup ; this inequality is in bool to benefit from proof irrelevance; - operations on intervals and their properties *) Section IntervalDef. Definition open_pred a b : pred R := fun x => Rltb a x && Rltb x b. Definition closed_pred a b: pred R := fun x => Rleb a x && Rleb x b. (* this definition should work with intervals of other kinds (integer, float, or infinite intervals) *) Record interval: Type := Interval { intset :> pred R; _ : forall a b, a \in intset -> b \in intset -> a < b -> {subset (open_pred a b) <= intset} }. Structure closedInt: Type := ClosedInt { inf : R; sup: R; _ : Rleb inf sup}. End IntervalDef. Notation "[ 'int' a b ]" := (closedInt a b _) (at level 0, a at level 69, b at level 69, format "[ 'int' a b ]"). Notation Local pred_of_int_def := (fun (i : closedInt) => closed_pred (inf i) (sup i) : _ -> _). Module Type IntDefSig. Parameter pred_of_int : closedInt -> pred_sort (predPredType R). (* This lets us use subtypes of set, like grosup or coset_of, as predicates. *) Coercion pred_of_int : closedInt >-> pred_class. Axiom pred_of_intE : pred_of_int = pred_of_int_def. End IntDefSig. Module IntDef : IntDefSig. Definition pred_of_int := pred_of_int_def. Lemma pred_of_intE : pred_of_int = pred_of_int_def. Proof. by []. Qed. End IntDef. Notation pred_of_int := IntDef.pred_of_int. Canonical Structure pred_of_int_unlock := Unlockable IntDef.pred_of_intE. Lemma Rleb_refl : forall x, Rleb x x. move=> x; apply/RleP; apply: Rle_refl. Qed. Lemma thin: forall x:R, closedInt . move=> x; exact (ClosedInt (Rleb_refl x)). Defined. Coercion thin: R >-> closedInt. Section IntervalProp. Lemma closed_eq: forall (cint: closedInt), cint =i [pred x | Rleb (inf cint) x && Rleb x (sup cint)]. by case; rewrite IntDef.pred_of_intE /closed_pred /=. Qed. Lemma in_intb: forall (X: closedInt) x, (x \in X) = (Rleb (inf X) x && Rleb x (sup X)). by move=> cint x; rewrite closed_eq -topredE /=. Qed. Lemma in_int: forall (cint: closedInt) x, (x \in cint) <-> (Rle (inf cint) x /\ Rle x (sup cint)). move=> cint x; rewrite in_intb; split => H. by move/andP :H => [H1 H2]; move/RleP: H1 => H1; move/RleP: H2=> H2; split. by apply/andP; split; apply/RleP; elim H. Qed. Lemma in_intP: forall (cint: closedInt) x, reflect (Rle (inf cint) x /\ Rle x (sup cint)) (x \in cint). Proof. move=> ci x. apply: (iffP idP); rewrite in_intb. by move/andP => [H1 H2]; move/RleP: H1 => H1; move/RleP: H2=> H2; split. by move=> H; apply/andP; split; apply/RleP; elim H. Qed. Lemma cint_axiom: forall (cint: closedInt) a0 b0, a0 \in cint -> b0 \in cint -> a0 < b0 -> {subset (open_pred a0 b0) <= cint}. Proof. move=> cint x y Hx Hy Hxy z Hz. rewrite ->in_int in Hx; rewrite ->in_int in Hy. rewrite in_int. rewrite -topredE /= /open_pred in Hz. move/andP: Hz => [Hz1 Hz2]; move/RltP: Hz1 => Hz1; move/RltP : Hz2 => Hz2. elim Hx => Hx1 Hx2; elim Hy => Hy1 Hy2. by split; left; [apply Rle_lt_trans with x| apply Rlt_le_trans with y]. Qed. Lemma cint_to_int: closedInt -> interval. move=> cint; apply (Interval (@cint_axiom cint) ). Qed. Coercion cint_to_int: closedInt >-> interval. Definition eqInt (ci1 ci2: closedInt) : bool := ((inf ci1) == (inf ci2)) && ((sup ci1) == (sup ci2)). Lemma eqIntP : Equality.axiom eqInt. Proof. move=> [i1 s1 H1] [i2 s2 H2]; rewrite /eqInt. apply: (iffP idP) => [/= H12|<-]; last by rewrite !eq_refl. move: H1 H2; case/andP: H12; move/eqP->; move/eqP=> -> H1 H2. congr ClosedInt. (*rewrite /is_true . have bi:= @bool_irrelevance (Rleb i2 s2) true H1 H2. *) apply bool_irrelevance. Qed. Lemma int_le: forall ci, inf ci <= sup ci. Proof. by move=> [i s H] /=; apply: RleP. Qed. Lemma inf_in_int: forall ci, inf ci \in ci. Proof. by move=> [i s H] /=; rewrite in_int /=; split; [right| apply: RleP]. Qed. Lemma sup_in_int: forall ci, sup ci \in ci. Proof. by move=> [i s H] /=; rewrite in_int /=; split; [apply: RleP| right]. Qed. Lemma in_singleton: forall x:R, x \in x. by move=>*; rewrite in_int /=; split; right. Qed. Lemma singleton_eq: forall (x y:R), x \in y <-> x = y. Proof. move=> x y; rewrite in_int /=; split=> H; last by rewrite H; split; right. by apply Rle_antisym; elim H. Qed. End IntervalProp. Canonical Structure cinterval_eqMixin := EqMixin eqIntP. Canonical Structure cinterval_eqType := Eval hnf in EqType closedInt cinterval_eqMixin. (* Section Hull. (*convex hull for a set A included in R; it's all we need for dealing with intervals *) Definition convexHull1 (A: R -> Prop) (x:R) : Prop := exists y, exists z, A y /\ A z /\ y <= x <= z. End Hull. *) Section IntervalOps. Lemma eq_interval: forall (ci1 ci2: closedInt), ((inf ci1) == (inf ci2)) && ((sup ci1) == (sup ci2)) = (ci1 == ci2). by done. Qed. Lemma eq_intervalP: forall (ci1 ci2: closedInt) , (ci1 = ci2) <-> ((inf ci1) = (inf ci2)) /\ ((sup ci1) = (sup ci2)) . Proof. move=> ci1 ci2; split => H; [by rewrite H; split|]. by apply/eqIntP ; rewrite /eqInt; apply/andP; split; elim H => H1 H2; apply/eqP. Qed. (*****************************************************************************) Definition mid x := (inf x + sup x) / 2. (* midpoint *) Definition rad x := (sup x - inf x) / 2. (* radius *) Definition mag x := Rmax (Rabs (inf x)) (Rabs (sup x)). (* magnitude *) Definition mig (x: closedInt) := if (0 \in x) then 0 else (Rmin (Rabs (inf x)) (Rabs (sup x))). (* mignitude *) (*Properties for the above defined concepts*) Lemma mid_in_int: forall ci, mid ci \in ci. move=> [i s H] //=. have Hcool: i <= s by apply/RleP. rewrite in_int /mid; split; rewrite //=; apply Rmult_le_reg_l with 2; [fourier| | fourier|]; field_simplify; rewrite /Rdiv Rinv_1; ring_simplify. replace (2*i) with (i + i); last by ring. by apply Rplus_le_compat_l. replace (2*s) with (s+s); last by ring. by apply Rplus_le_compat_r. Qed. Lemma inf_le_sup: forall (ci: closedInt) x, x \in ci -> inf ci <= sup ci. Proof. by move=> ci x; rewrite in_int; move=> [H1 H2]; apply Rle_trans with x. Qed. Theorem Rabs_le_le_eq : forall x y, Rabs x <= y <-> -y <= x <= y. Proof. intros x y; unfold Rabs; split; elim Rcase_abs; intros H1 H2. split; fourier. split; fourier. elim H2; intros; fourier. elim H2; intros; fourier. Qed. Lemma Rle_Rle_minus: forall x y z, - y <= x - z <= y <-> - y + z <= x <= y + z. move=> x y z; split; move=> [H1 H2]; split; fourier. Qed. Lemma in_mid_rad: forall (ci: closedInt) x, x \in ci <-> Rabs (x - mid ci) <= rad ci. Proof. move=> ci x; split => Hcix. rewrite /mid /rad; move/in_intP: Hcix => [Hcixl Hcixu]. rewrite Rabs_minus_sym. replace ((inf ci + sup ci) / 2 - x) with ((inf ci - x) / 2 + (sup ci - x) / 2); [|field]. apply Rle_trans with (Rabs ((inf ci - x) / 2) + Rabs((sup ci - x) / 2)); [apply Rabs_triang|] . rewrite Rabs_left1; [rewrite Rabs_right|]; [right; field| |]; unfold Rdiv; ring_simplify; fourier. move: Hcix; rewrite Rabs_le_le_eq Rle_Rle_minus /rad /mid ; move=> Hcix. replace (- ((sup ci - inf ci) / 2) + (inf ci + sup ci) / 2) with (inf ci) in Hcix; [|field]. replace ((sup ci - inf ci) / 2 + (inf ci + sup ci) / 2) with (sup ci) in Hcix; [|field]. by apply/in_intP. Qed. Lemma rad_pos x: 0 <= rad x. move=> [i s H]. have Hc: i <= s by apply: RleP. rewrite /rad /=. have H1: 0 <= s - i; first by fourier. move: H1; move: (s - i) => t H1; fourier. Qed. Lemma inf_mid_rad x: inf x = mid x - rad x. move=> *; rewrite /mid /rad; field. Qed. Lemma sup_mid_rad x: sup x = mid x + rad x. move=> *; rewrite /mid /rad; field. Qed. Lemma intersect_int: forall i1 i2, Rabs (mid i1 - mid i2) <= rad i1 +rad i2 -> {r| r \in i1 /\ r \in i2}. move=> i1 i2 H. (*case (Rle_dec (mid i1) (mid i2)) => Hineq.*) case (Rle_dec (inf i1) (inf i2)) => Hi2. exists (inf i2); split; last by apply inf_in_int. rewrite in_int; split; first by done. rewrite inf_mid_rad sup_mid_rad. apply Rplus_le_reg_l with (rad i2); ring_simplify. apply Rplus_le_reg_l with (-mid i1)%Re; ring_simplify. apply Rle_trans with (Rabs (mid i1 - mid i2)). rewrite Rabs_minus_sym Rplus_comm /Rminus; apply RRle_abs. by rewrite Rplus_comm. exists (inf i1); split; first by apply inf_in_int. rewrite in_int; split. by left; apply Rnot_le_lt. rewrite inf_mid_rad sup_mid_rad. apply Rplus_le_reg_l with (rad i1); ring_simplify. apply Rplus_le_reg_l with (-mid i2)%Re; ring_simplify. apply Rle_trans with (Rabs (mid i1 - mid i2)); last by done. rewrite Rplus_comm /Rminus; apply RRle_abs. Qed. Lemma inf_2rad_sup: forall i, inf i + 2*rad i = sup i. by move=>*; rewrite /rad; field. Qed. Lemma mid_rad_wd: forall x, Rleb (mid x - rad x) (mid x + rad x). Proof. move=> x. rewrite /mid /rad; apply/RleP. have Hile:= int_le x. field_simplify. by rewrite /Rdiv; rewrite !(Rinv_r_simpl_m); [|apply Rgt_not_eq; fourier|apply Rgt_not_eq; fourier] . Qed. Lemma eq_int_bound_mid: forall x, x = @ClosedInt (mid x - rad x) (mid x + rad x) (mid_rad_wd _ ). by move=> x; rewrite eq_intervalP //=; split; [apply inf_mid_rad| apply sup_mid_rad]. Qed. (**********************************************************************) (*Operations*) Lemma add_i_wd : forall ci1 ci2, Rleb (inf ci1 + inf ci2) (sup ci1 + sup ci2). Proof. move=> ci1 ci2; case ci1=> i1 s1 /=; move/RleP=>H1. case ci2=> i2 s2 /=; move/RleP=>H2. apply/RleP. fourier. Qed. Definition add_i (ci1 ci2: closedInt): closedInt := @ClosedInt (inf ci1 + inf ci2) (sup ci1 + sup ci2) (add_i_wd _ _). Lemma opp_i_wd: forall ci, Rleb (-sup ci) (-inf ci). Proof. move=> ci; case ci=> i1 s1 /=; move/RleP=>H1. apply/RleP; fourier. Qed. Definition opp_i ci := @ClosedInt (-sup ci) (-inf ci) (opp_i_wd ci). Lemma Rmin_le_Rmax: forall x y, Rmin x y <= Rmax x y. Proof. move=> x y; rewrite /Rmin /Rmax; case (Rle_dec x y); first by done. move=> H; apply Rnot_lt_le; intuition . Qed. Lemma muls_i_wd: forall r ci, Rleb (Rmin (r * inf ci) (r * sup ci)) (Rmax (r * inf ci) (r * sup ci)). Proof. move=> r ci; case ci=> i1 s1 /=; move/RleP=>H1. apply/RleP; apply Rmin_le_Rmax. Qed. (* multiplication by a scalar can also be achieved via the singleton coercion for the multiplication on intervals ? the extra definition simplifies work *) Definition muls_i r ci := @ClosedInt (Rmin (r * inf ci) (r * sup ci)) (Rmax (r * inf ci) (r * sup ci)) (muls_i_wd _ _). Lemma muls_i_s0: forall ci, muls_i 0 ci = 0. move=> ci; rewrite eq_intervalP /= !Rmult_0_l. rewrite Rmax_right; last by right. rewrite Rmin_right; last by right. by done. Qed. Definition seqe ci1 ci2 := inf ci1*inf ci2 :: inf ci1*sup ci2 :: sup ci1 *inf ci2 :: sup ci1 * sup ci2 :: nil. Lemma seqe_not_nil: forall x y, seqe x y != [::]. move=>*; by done. Qed. Lemma mul_i_wd: forall ci1 ci2, Rleb (\big[Rmin/last 0 (seqe ci1 ci2)]_(i <- seqe ci1 ci2) i) (\big[Rmax/last 0 (seqe ci1 ci2)]_(i <- seqe ci1 ci2) i). Proof. move=> ci1 ci2. apply/RleP. have Hmm:= @big_min_max_le (seqe ci1 ci2) (fun x => x) . by apply Hmm; rewrite /seqe; done. Qed. Definition mul_i ci1 ci2 := ClosedInt (mul_i_wd ci1 ci2). Lemma comm_add_i: commutative add_i. move=> *; rewrite eq_intervalP; rewrite /add_i /=; split; ring. Qed. Lemma assoc_add_i: associative add_i. move=> *; rewrite eq_intervalP; rewrite /add_i /=; split; ring. Qed. Lemma ne_add_i: forall ci, add_i ci 0 = ci. move=> ci; rewrite eq_intervalP; rewrite /add_i /=; split; rewrite //=; ring. Qed. Lemma left_id_add_i: left_id (0:closedInt) add_i. move=> *; rewrite eq_intervalP; rewrite /add_i /=; split; rewrite //=; ring. Qed. Lemma right_id_add_i: right_id (0:closedInt) add_i. move=> *; rewrite eq_intervalP; rewrite /add_i /=; split; rewrite //=; ring. Qed. Lemma left_zero_mul_i: left_zero (0:closedInt) mul_i. move=> X; rewrite eq_intervalP /=. split. have Hr: seqe R0 X != [::] by rewrite /seqe. elim (big_min_exists (fun x => x) Hr); rewrite /= => x [Hxin Hx]; rewrite Hx. rewrite /seqe /= !Rmult_0_l in Hxin. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. by rewrite mem_seq1 in Hxin; apply/eqP. have Hr: seqe R0 X != [::] by rewrite /seqe. elim (big_max_exists (fun x => x) Hr); rewrite /= => x [Hxin Hx]; rewrite Hx. rewrite /seqe /= !Rmult_0_l in Hxin. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. by rewrite mem_seq1 in Hxin; apply/eqP. Qed. Lemma right_zero_mul_i: right_zero (0:closedInt) mul_i. move=> X; rewrite eq_intervalP /=. split. have Hr: seqe X R0 != [::] by rewrite /seqe. elim (big_min_exists (fun x => x) Hr); rewrite /= => x [Hxin Hx]; rewrite Hx. rewrite /seqe /= !Rmult_0_r in Hxin. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. by rewrite mem_seq1 in Hxin; apply/eqP. have Hr: seqe X R0 != [::] by rewrite /seqe. elim (big_max_exists (fun x => x) Hr); rewrite /= => x [Hxin Hx]; rewrite Hx. rewrite /seqe /= !Rmult_0_r in Hxin. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. rewrite in_cons in Hxin; move/orP: Hxin => Hxin; elim Hxin; clear Hxin => Hxin; first by apply/eqP. by rewrite mem_seq1 in Hxin; apply/eqP. Qed. Lemma add_i_correct: forall (ci1 ci2: closedInt) x y, x \in ci1 -> y \in ci2 -> (x+y) \in (add_i ci1 ci2). Proof. move=> [ix sx HX] [iy sy HY] x y HxX HyY. rewrite in_int //=. have HX1: ix <= sx by apply: RleP. have HY1: iy <= sy by apply: RleP. move: HxX; rewrite in_int /=; move => [HxX1 HxX2]. move: HyY; rewrite in_int /=; move => [HyY1 HyY2]. split; fourier. Qed. Lemma opp_i_correct: forall (ci1: closedInt) x, x \in ci1 -> (-x) \in (opp_i ci1). Proof. move=> [ix sx HX] x Hx. rewrite in_int //=. have HX1: ix <= sx by apply: RleP. move: Hx; rewrite in_int /=; move => [HxX1 HxX2]. split;fourier. Qed. Lemma muls_i_correct: forall r (ci1: closedInt) x, x \in ci1 -> (r*x) \in (muls_i r ci1). Proof. move=> r [ix sx HX] x Hx. rewrite in_int //=. have HX1: ix <= sx by apply: RleP. move: Hx; rewrite in_int /=; move => [HxX1 HxX2]. case (Rle_lt_dec 0 r) => Hdec. have Hin: r*ix <= r*sx by apply Rmult_le_compat_l. rewrite Rmin_left; last by done. rewrite Rmax_right; last by done. by split; apply Rmult_le_compat_l. have Hin: r*sx <= r*ix by (apply Rmult_le_compat_neg_l; intuition). rewrite Rmin_right; last by done. rewrite Rmax_left; last by done. by split; apply Rmult_le_compat_neg_l; intuition. Qed. Lemma Rmult_le_compat_neg: forall a b c d, 0 <= c -> c <= a -> b <= 0 -> b <= d -> a*b <= c*d. move=> a b c d Ha0 Hac Hb0 Hdb. case (Rle_dec 0 d) => Hd0. apply Rle_trans with (a*0). by apply Rmult_le_compat_l; [apply Rle_trans with c|]. by rewrite Rmult_0_r -(Rmult_0_r 0); apply Rmult_le_compat; [right|right| |]. have H1 := Ropp_le_contravar _ _ Hdb. rewrite -(Ropp_involutive (a*b)) -(Ropp_involutive (c*d)). apply Ropp_le_contravar. replace (-(c*d)) with (c * (-d)); last by ring. replace (-(a*b)) with (a * (-b)); last by ring. apply Rmult_le_compat; [done| | done| done]. have H2 := Rnot_le_lt _ _ Hd0. by left; apply Ropp_0_gt_lt_contravar. Qed. Lemma Rmult_pos_neg: forall a b, a <= 0 -> 0 <= b -> a*b <= 0. move=> a b Ha Hb. replace 0 with (0*b) by ring. by apply Rmult_le_compat_r. Qed. Lemma Rmult_neg_neg: forall a b, a <=0 -> b <= 0 -> 0 <= a*b. move=> a b Ha Hb. rewrite -(Ropp_involutive (_*_)) -Ropp_0. apply Ropp_le_contravar. rewrite -Ropp_mult_distr_r_reverse . apply Rmult_pos_neg. done. by rewrite -Ropp_0; apply Ropp_le_contravar. Qed. Lemma mul_i_correct: forall (ci1 ci2: closedInt) x y, x \in ci1-> y \in ci2 -> (x*y) \in (mul_i ci1 ci2). Proof. move=> [ix sx HX] [iy sy HY] x y Hx Hy. rewrite in_int //=. set r := (seqe (ClosedInt HX) (ClosedInt HY)). have HX1: ix <= sx by apply: RleP. have HY1: iy <= sy by apply: RleP. move: Hx; rewrite in_int /=; move => [HxX1 HxX2]. move: Hy; rewrite in_int /=; move => [HyY1 HyY2]. have H4 : sx * sy \in seqe (ClosedInt HX) (ClosedInt HY) . rewrite /seqe /= mem_seq4. by apply/orP; right; apply/orP; right; apply/orP; right; apply/eqP. have H3 : sx * iy \in seqe (ClosedInt HX) (ClosedInt HY) . rewrite /seqe /= mem_seq4. by apply/orP; right; apply/orP; right; apply/orP; left; apply/eqP. have H2 : ix * sy \in seqe (ClosedInt HX) (ClosedInt HY) . rewrite /seqe /= mem_seq4. by apply/orP; right; apply/orP; left; apply/eqP. have H1 : ix * iy \in seqe (ClosedInt HX) (ClosedInt HY) . by rewrite /seqe /= in_cons; apply/orP; left; apply/eqP. (* 0 <= x, 0 <= y *) elim (Rle_dec 0 ix); elim (Rle_dec 0 iy)=> Hy0 Hx0. split. apply Rle_trans with (ix*iy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id (ix*iy) H1). by rewrite /= in Hle; rewrite /r . by apply Rmult_le_compat. apply Rle_trans with (sx*sy). by apply Rmult_le_compat;[apply Rle_trans with ix|apply Rle_trans with iy| |]. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id (sx*sy) H4). by rewrite /= in Hle; rewrite /r . (*0<=x, ... *) split. apply Rle_trans with (sx*iy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id (sx*iy) H3). by rewrite /= in Hle; rewrite /r . have H01 := Rnot_le_lt _ _ Hy0. by apply Rmult_le_compat_neg ;[apply Rle_trans with ix | | left |]. case (Rle_dec 0 sy) => Hsy0. apply Rle_trans with (sx*sy). case (Rle_dec 0 y) => Hy. by apply Rmult_le_compat; [apply Rle_trans with ix| | |]. apply Rle_trans with 0. by rewrite Rmult_comm; apply Rmult_pos_neg; [left; apply Rnot_le_lt| apply Rle_trans with ix]. by apply Rmult_le_pos; [apply Rle_trans with ix|]. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id (sx*sy) H4). by rewrite /= in Hle; rewrite /r . apply Rle_trans with (ix*sy). by apply Rmult_le_compat_neg;[| |apply Rle_trans with sy; [|left; apply Rnot_le_lt] |]. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H2). by rewrite /= in Hle; rewrite /r . have H01 := Rnot_le_lt _ _ Hx0. split. apply Rle_trans with (ix*sy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H2). by rewrite /= in Hle; rewrite /r . rewrite (Rmult_comm ix sy) (Rmult_comm x y). by apply Rmult_le_compat_neg; [apply Rle_trans with iy | | left |]. case (Rle_dec 0 sx) => Hsx0. apply Rle_trans with (sx*sy). case (Rle_dec 0 x) => Hx. by apply Rmult_le_compat; [ | apply Rle_trans with iy| |]. apply Rle_trans with 0. by apply Rmult_pos_neg ; [left; apply Rnot_le_lt| apply Rle_trans with iy]. by apply Rmult_le_pos; [|apply Rle_trans with iy]. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H4). by rewrite /= in Hle; rewrite /r . apply Rle_trans with (sx*iy). rewrite (Rmult_comm sx iy) (Rmult_comm x y). by apply Rmult_le_compat_neg; [ | | apply Rle_trans with sx; [ |left; apply Rnot_le_lt ] |]. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H3). by rewrite /= in Hle; rewrite /r . case (Rle_dec 0 sx) => Hsx0; last first. split. case (Rle_dec 0 sy) => Hsy0. apply Rle_trans with (ix*sy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H2). by rewrite /= in Hle; rewrite /r . rewrite (Rmult_comm ix) (Rmult_comm x). case (Rle_dec 0 y) => Hy. by apply Rmult_le_compat_neg; [ | |left; apply Rnot_le_lt |]. apply Rle_trans with 0. by rewrite (Rmult_comm); apply Rmult_pos_neg;[left; apply Rnot_le_lt |]. apply Rmult_neg_neg. by left; apply Rnot_le_lt. by apply Rle_trans with sx; [|left; apply Rnot_le_lt]. apply Rle_trans with (sx*sy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H4). by rewrite /= in Hle; rewrite /r . rewrite -(Ropp_involutive (sx*sy)) -(Ropp_involutive (x*y)). apply Ropp_le_contravar. rewrite -!Ropp_mult_distr_l_reverse. apply Rmult_le_compat_neg. by apply Ropp_0_ge_le_contravar; left; apply Rnot_le_lt . by apply Ropp_le_contravar. by apply Rle_trans with sy; [|left; apply Rnot_le_lt]. done. apply Rle_trans with (ix*iy). case (Rle_dec 0 y) => Hy. apply Rle_trans with 0. by apply Rmult_pos_neg; [apply Rle_trans with sx; [|left; apply Rnot_le_lt]|]. by apply Rmult_neg_neg; left; apply Rnot_le_lt. rewrite -(Rmult_opp_opp x) -(Rmult_opp_opp ix). apply Rmult_le_compat. apply Ropp_0_ge_le_contravar; apply Rle_ge. by apply Rle_trans with sx; [|left; apply Rnot_le_lt]. by apply Ropp_0_ge_le_contravar; apply Rle_ge; left; apply Rnot_le_lt. by apply Ropp_le_contravar. by apply Ropp_le_contravar. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H1). by rewrite /= in Hle; rewrite /r . case (Rle_dec 0 sy) => Hy; last first. split. apply Rle_trans with (sx*iy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H3). by rewrite /= in Hle; rewrite /r . case (Rle_dec 0 x) => Hx. by apply Rmult_le_compat_neg; [| |left; apply Rnot_le_lt |]. apply Rle_trans with 0. by rewrite Rmult_comm; apply Rmult_pos_neg; [left; apply Rnot_le_lt|]. by apply Rmult_neg_neg; [left; apply Rnot_le_lt|apply Rle_trans with sy; [|left; apply Rnot_le_lt]]. apply Rle_trans with (ix*iy). case (Rle_dec 0 x) => hx. apply Rle_trans with 0. rewrite Rmult_comm; apply Rmult_pos_neg; last by done. by apply Rle_trans with sy;[|left; apply Rnot_le_lt]. by apply Rmult_neg_neg; left; apply Rnot_le_lt. rewrite -(Rmult_opp_opp x) -(Rmult_opp_opp ix). apply Rmult_le_compat. by apply Ropp_0_ge_le_contravar; apply Rle_ge; left; apply Rnot_le_lt. by apply Ropp_0_ge_le_contravar; apply Rle_ge; apply Rle_trans with sy; [|left; apply Rnot_le_lt]. by apply Ropp_le_contravar. by apply Ropp_le_contravar. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H1). by rewrite /= in Hle; rewrite /r . case (Rle_dec 0 x) => Hx; case (Rle_dec 0 y) => H0y. split. apply Rle_trans with (ix*sy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H2). by rewrite /= in Hle; rewrite /r . apply Rle_trans with 0. by apply Rmult_pos_neg; [left; apply Rnot_le_lt|]. by apply Rmult_le_pos. apply Rle_trans with (sx*sy). by apply Rmult_le_compat. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H4). by rewrite /= in Hle; rewrite /r . split. apply Rle_trans with (sx*iy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H3). by rewrite /= in Hle; rewrite /r . by apply Rmult_le_compat_neg; [| |left; apply Rnot_le_lt|]. apply Rle_trans with (sx*sy). apply Rle_trans with 0. by rewrite Rmult_comm; apply Rmult_pos_neg; [left; apply Rnot_le_lt|]. by apply Rmult_le_pos. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H4). by rewrite /= in Hle; rewrite /r . split. apply Rle_trans with (ix*sy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H2). by rewrite /= in Hle; rewrite /r . rewrite (Rmult_comm ix) (Rmult_comm x). by apply Rmult_le_compat_neg; [| |left; apply Rnot_le_lt|]. apply Rle_trans with (sx*sy). apply Rle_trans with 0. by apply Rmult_pos_neg; [left; apply Rnot_le_lt|]. by apply Rmult_le_pos. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H4). by rewrite /= in Hle; rewrite /r . split. apply Rle_trans with (sx*iy). have Hle := (@big_min_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H3). by rewrite /= in Hle; rewrite /r. apply Rle_trans with 0. by rewrite Rmult_comm; apply Rmult_pos_neg; [left; apply Rnot_le_lt|]. by apply Rmult_neg_neg; left; apply Rnot_le_lt. apply Rle_trans with (ix*iy). rewrite -(Ropp_involutive (x*_)) -(Ropp_involutive (ix*_)) . apply Ropp_le_contravar. rewrite -(Ropp_mult_distr_l_reverse ix) -(Ropp_mult_distr_l_reverse x). apply Rmult_le_compat_neg. by apply Ropp_0_ge_le_contravar; left; apply Rnot_le_lt . by apply Ropp_le_contravar. by left; apply Rnot_le_lt. done. have Hle := (@big_max_le (seqe (ClosedInt HX) (ClosedInt HY)) id _ H1). by rewrite /= in Hle; rewrite /r. Qed. Lemma Rmult_pos: forall r1 r2, 0<=r1 -> 0<=r2-> 0<=r1*r2. Proof. intros r1 r2 Hr1 Hr2. replace 0 with (0*r2) ; last by ring. auto with real. Qed. (* Lemma Int_part_pos: forall r, 0 <= r -> 0 <= IZR (Int_part r). Proof. move=> r Hrpos. rewrite /Int_part -Z_R_minus. case: (archimed r)=> H1 Ha. Admitted. *) Lemma add_i_compl: forall ci1 ci2 r, r \in (add_i ci1 ci2) -> {ar | ar.1 \in ci1 /\ ar.2 \in ci2 /\ r = ar.1+ar.2}. Proof. move=> [ix sx HX] [iy sy HY] s Hs. have HX1: ix <= sx by apply: RleP. have HY1: iy <= sy by apply: RleP. move: Hs; rewrite (in_intb ) /=; move/andP => [Hsi Hss]. have HSi: ix + iy <= s by apply: RleP. have HSs: s <= sx + sy by apply: RleP. (* move: Hx; rewrite in_int /=; move => [HxX1 HxX2]. move: Hy; rewrite in_int /=; move => [HyY1 HyY2]. *) case (Rle_dec s (ix + sy)) => Hsint. exists ( ix , s - ix ); rewrite /=. split; first by rewrite /=; apply inf_in_int. split; last by ring. rewrite in_int /=; split. apply Rplus_le_reg_l with ix; fourier. apply Rplus_le_reg_l with ix; fourier. exists (s - sy, sy); rewrite /=. split. rewrite in_int /=; split. by apply Rplus_le_reg_l with sy; ring_simplify; rewrite Rplus_comm; left; apply Rnot_le_lt. apply Rplus_le_reg_l with sy; fourier. split; [apply sup_in_int |ring]. Qed. (* (* non degenerated intervals *) case (Rle_lt_or_eq_dec 0 (rad I) (rad_pos I)) => Hdec. (* all the sum, except for the last bit *) case (Rle_dec x (inf I + sup J)) => Hdecx. set q:= (x - (inf I + inf J) ) / (2* rad I). exists ((inf I + 2*rad I* frac_part q), (inf J + 2* rad I * IZR (Int_part q))). rewrite //=; split. (* inf I + 2*r1*{q} \in I *) rewrite in_int; split. rewrite -{1}(Rplus_0_r (inf I)); apply Rplus_le_compat_l. apply: Rmult_pos; [apply Rmult_pos ; [fourier |apply rad_pos]|]. by apply Rge_le; elim (base_fp q). apply Rle_trans with (inf I + 2* rad I); last by (right; apply inf_2rad_sup). apply Rplus_le_compat_l. rewrite Rmult_assoc; apply Rmult_le_compat_l; [fourier|]. rewrite -{2}(Rmult_1_r (rad I)); apply Rmult_le_compat_l; [apply rad_pos|by left; elim (base_fp q)]. split. (* inf J + 2*r1*[q] \in J *) rewrite in_int; split. rewrite -{1}(Rplus_0_r (inf J)); apply Rplus_le_compat_l. apply: Rmult_pos; [apply Rmult_pos ; [fourier |apply rad_pos]|]. apply Int_part_pos; rewrite /q /Rdiv; apply Rmult_pos. move: Hx; rewrite in_int /add_i /= => Hx; case Hx=> hx1 hx2. by apply Rplus_le_reg_l with (inf I + inf J); ring_simplify. left; apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; fourier. rewrite -inf_2rad_sup; apply Rplus_le_compat_l. rewrite Rmult_assoc; apply Rmult_le_compat_l; first by fourier. apply Rle_trans with (rad I * q). apply Rmult_le_compat_l; first by apply rad_pos. by elim (base_Int_part q). rewrite /q; apply Rmult_le_reg_l with 2; [fourier|]. field_simplify; [|apply Rgt_not_eq; apply: Hdec]. rewrite /Rdiv Rinv_1 !Rmult_1_r. apply Rplus_le_reg_l with (inf I); apply Rplus_le_reg_l with (inf J); ring_simplify; apply Rle_trans with (1:= Hdecx); rewrite -inf_2rad_sup; right; ring. (* equality*) transitivity (inf I + inf J + 2 * rad I * (frac_part q + IZR (Int_part q))); last by ring. by rewrite /frac_part /q; field; apply Rgt_not_eq. (* last bit*) exists ((x - sup J), sup J); rewrite /=; split. rewrite in_int; split. by apply Rplus_le_reg_l with (sup J); ring_simplify; left; rewrite Rplus_comm; apply Rnot_le_lt. apply Rplus_le_reg_l with (sup J); ring_simplify. move: Hx; rewrite in_int => Hx; elim Hx => _ hx2. apply Rle_trans with (1:= hx2); right; rewrite /add_i //=; ring. split; [apply sup_in_int | ring]. (* degenarate interval *) exists ( inf I , (x - inf I)); rewrite /=. split; first by apply inf_in_int. split. move: Hx ; rewrite in_int => Hx; elim Hx => hx1 hx2. rewrite in_int; split; apply Rplus_le_reg_l with (inf I); ring_simplify. apply Rle_trans with (2:= hx1); rewrite /add_i /=; by right. apply Rle_trans with (1:= hx2); rewrite /add_i /=. apply Rplus_le_compat_r; right. rewrite /rad /Rdiv in Hdec. apply Rplus_eq_reg_l with (-inf I); ring_simplify. apply Rmult_eq_reg_l with (/2); last by apply Rgt_not_eq; fourier. rewrite Rmult_0_r Hdec; ring. ring. Qed. *) Lemma opp_i_compl: forall ci1 r, r \in (opp_i ci1) -> {r1| r1 \in ci1 /\ r = - r1}. Proof. move=> [ix sx Hx] r Hr. exists (-r); split; last by (symmetry; apply: Ropp_involutive). move: Hr; rewrite !in_int /=; move=> [Hr1 Hr2]. split; fourier. Qed. Lemma Rmult_le_reg_neg_l: forall r p q, r < 0 -> r*p <= r*q -> q <= p. Proof. move=> r p q Hr Hrpq. apply Rmult_le_reg_l with (-r); first by apply Ropp_gt_lt_0_contravar. by apply Ropp_le_cancel; rewrite !Ropp_mult_distr_l_reverse !Ropp_involutive. Qed. Lemma muls_i_compl: forall r k ci1, r \in (muls_i k ci1) -> {r1 | r1 \in ci1 /\ r = k*r1}. Proof. move=>r k [ix sx Hx] Hr. case (total_order_T 0 k); [case => Hdec |move=> Hdec]. have Hx1: ix <= sx by apply: RleP. have Hin: k*ix <= k*sx by (apply Rmult_le_compat_l; intuition). have Heq: r = k*(r/k) by (field; apply Rgt_not_eq; exact: Hdec). exists (r/k); split; last by done. move: Hr; rewrite in_int /=; move=> [Hr1 Hr2]. rewrite Rmin_left in Hr1; last by done. rewrite Rmax_right in Hr2; last by done. rewrite in_int /=; split. apply Rmult_le_reg_l with k; first by done. by rewrite -Heq. apply Rmult_le_reg_l with k; first by done. by rewrite -Heq. exists ix; split; first by apply inf_in_int. move: Hr; rewrite -Hdec muls_i_s0 singleton_eq => ->; ring. have Hx1: ix <= sx by apply: RleP. have Hin: k*sx <= k*ix. apply: Rmult_le_compat_neg_l; intuition. have Heq: r = k*(r/k) by (field; apply Rlt_not_eq; exact: Hdec). exists (r/k); split; last by done. move: Hr; rewrite in_int /=; move=> [Hr1 Hr2]. rewrite Rmin_right in Hr1; last by done. rewrite Rmax_left in Hr2; last by done. rewrite in_int /=; split. apply Rmult_le_reg_neg_l with k; first by done. by rewrite -Heq. apply Rmult_le_reg_neg_l with k; first by done. by rewrite -Heq. Qed. Lemma mid_mul: forall ci r, mid ci * r = mid (muls_i r ci). Proof. move=> [i s H] r; rewrite /mid /= /Rmin /Rmax. case (Rle_dec (r*i) (r*s))=>*; field. Qed. Lemma mid_add: forall ci1 ci2, mid (add_i ci1 ci2) = mid ci1 + mid ci2. Proof. move=> ci1 ci2; rewrite /mid /add_i /=; field. Qed. Lemma Rle_compat_R0: forall x y r, x <= y -> r*x <= r*y -> 0 <= r \/ x = y. move=> x y r H J. case: (Rtotal_order 0 r) => [H1 | [H2 | H3]]; [left; by left|left; by right|]. elim H=> H4. have H5: ~ r * x <= r * y. apply Rlt_not_le. by apply Rmult_lt_gt_compat_neg_l. by left; elim H5. by right. Qed. Lemma Rlt_compat_R0: forall x y r, x <= y -> r*y < r*x -> r < 0 . move=> x y r H J. case: (Rtotal_order r 0) => [H1 | [H2 | H3]]; [ by done| |]. rewrite H2 !Rmult_0_l in J. elim (Rlt_irrefl _ J). elim H => H4. have H5: ~ r * y < r * x. apply Rle_not_lt; left. by apply Rmult_gt_compat_l. by elim H5. rewrite H4 in J. elim (Rlt_irrefl _ J). Qed. Lemma rad_mul: forall ci r, rad ci * Rabs r = rad (muls_i r ci). Proof. move=> [i s H] r; rewrite /rad /= /Rmin /Rmax. case (Rle_dec (r*i) (r*s))=>H1. case: (Req_dec i s) => [-> |Heq]; first by field_simplify. rewrite Rabs_right; first by field. move/RleP: H => H. by case: (Rle_compat_R0 H H1) => H2; [apply Rle_ge|]. rewrite Rabs_left; first by field. by apply Rlt_compat_R0 with i s; [apply: RleP|apply: Rnot_le_lt]. Qed. Lemma rad_add: forall ci1 ci2, rad (add_i ci1 ci2) = rad ci1 + rad ci2. Proof. move=> ci1 ci2; rewrite /rad /add_i /=; field. Qed. End IntervalOps. Import Monoid. Canonical Structure add_i_law := Law assoc_add_i left_id_add_i right_id_add_i. Canonical Structure add_i_com_law := ComLaw comm_add_i. Canonical Structure mul_i_mul_law := MulLaw left_zero_mul_i right_zero_mul_i.