Library mathcomp.algebra.interval
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype.
From mathcomp
Require Import bigop ssralg finset fingroup zmodp ssrint ssrnum.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Import GRing.Theory Num.Theory.
Local Notation mid x y := ((x + y) / 2%:R).
Section IntervalPo.
CoInductive itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
Notation BOpen := (BOpen_if true).
Notation BClose := (BOpen_if false).
CoInductive interval (T : Type) := Interval of itv_bound T & itv_bound T.
Variable (R : numDomainType).
Definition pred_of_itv (i : interval R) : pred R :=
[pred x | let: Interval l u := i in
match l with
| BOpen a => a < x
| BClose a => a <= x
| BInfty => true
end &&
match u with
| BOpen b => x < b
| BClose b => x <= b
| BInfty => true
end].
Canonical Structure itvPredType := Eval hnf in mkPredType pred_of_itv.
Notation "`[ a , b ]" := (Interval (BClose a) (BClose b))
(at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope.
Notation "`] a , b ]" := (Interval (BOpen a) (BClose b))
(at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
Notation "`[ a , b [" := (Interval (BClose a) (BOpen b))
(at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope.
Notation "`] a , b [" := (Interval (BOpen a) (BOpen b))
(at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b))
(at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b))
(at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _))
(at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _))
(at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope.
Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _))
(at level 0, format "`] -oo , '+oo' [") : ring_scope.
Definition itv_rewrite (i : interval R) x : Type :=
let: Interval l u := i in
(match l with
| BClose a => (a <= x) * (x < a = false)
| BOpen a => (a <= x) * (a < x) * (x <= a = false)
| BInfty => forall x : R, x == x
end *
match u with
| BClose b => (x <= b) * (b < x = false)
| BOpen b => (x <= b) * (x < b) * (b <= x = false)
| BInfty => forall x : R, x == x
end *
match l, u with
| BClose a, BClose b =>
(a <= b) * (b < a = false) * (a \in `[a, b]) * (b \in `[a, b])
| BClose a, BOpen b =>
(a <= b) * (a < b) * (b <= a = false)
* (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b])
| BOpen a, BClose b =>
(a <= b) * (a < b) * (b <= a = false)
* (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b])
| BOpen a, BOpen b =>
(a <= b) * (a < b) * (b <= a = false)
* (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b])
| _, _ => forall x : R, x == x
end)%type.
Definition itv_decompose (i : interval R) x : Prop :=
let: Interval l u := i in
((match l with
| BClose a => (a <= x) : Prop
| BOpen a => (a < x) : Prop
| BInfty => True
end : Prop) *
(match u with
| BClose b => (x <= b) : Prop
| BOpen b => (x < b) : Prop
| BInfty => True
end : Prop))%type.
Lemma itv_dec : forall (x : R) (i : interval R),
reflect (itv_decompose i x) (x \in i).
Proof. by move=> x [[[] a|] [[] b|]]; apply: (iffP andP); case. Qed.
Arguments itv_dec [x i].
Definition lersif (x y : R) b := if b then x < y else x <= y.
Local Notation "x <= y ?< 'if' b" := (lersif x y b)
(at level 70, y at next level,
format "x '[hv' <= y '/' ?< 'if' b ']'") : ring_scope.
Lemma lersifxx x b: (x <= x ?< if b) = ~~ b.
Proof. by case: b; rewrite /= lterr. Qed.
Lemma lersif_trans x y z b1 b2 :
x <= y ?< if b1 -> y <= z ?< if b2 -> x <= z ?< if b1 || b2.
Proof.
case: b1; first by case: b2; [apply: ltr_trans | apply: ltr_le_trans].
by case: b2; [apply: ler_lt_trans | apply: ler_trans].
Qed.
Lemma lersifW b x y : x <= y ?< if b -> x <= y.
Proof. by case: b => //; move/ltrW. Qed.
Lemma lersifNF x y b : y <= x ?< if ~~ b -> x <= y ?< if b = false.
Proof. by case: b => /= [/ler_gtF|/ltr_geF]. Qed.
Lemma lersifS x y b : x < y -> x <= y ?< if b.
Proof. by case: b => //= /ltrW. Qed.
Lemma lersifT x y : x <= y ?< if true = (x < y). Proof. by []. Qed.
Lemma lersifF x y : x <= y ?< if false = (x <= y). Proof. by []. Qed.
Definition le_boundl b1 b2 :=
match b1, b2 with
| BOpen_if b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if (~~ b2 && b1)
| BOpen_if _ _, BInfty => false
| _, _ => true
end.
Definition le_boundr b1 b2 :=
match b1, b2 with
| BOpen_if b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if (~~ b1 && b2)
| BInfty, BOpen_if _ _ => false
| _, _ => true
end.
Lemma itv_boundlr bl br x :
(x \in Interval bl br) =
(le_boundl bl (BClose x)) && (le_boundr (BClose x) br).
Proof. by move: bl br => [[] a|] [[] b|]. Qed.
Lemma le_boundr_refl : reflexive le_boundr.
Proof. by move=> [[] b|]; rewrite /le_boundr /= ?lerr. Qed.
Hint Resolve le_boundr_refl.
Lemma le_boundl_refl : reflexive le_boundl.
Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed.
Hint Resolve le_boundl_refl.
Lemma le_boundl_bb x b1 b2 :
le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).
Proof. by rewrite /le_boundl lersifxx andbC negb_and negbK implybE. Qed.
Lemma le_boundr_bb x b1 b2 :
le_boundr (BOpen_if b1 x) (BOpen_if b2 x) = (b2 ==> b1).
Proof. by rewrite /le_boundr lersifxx andbC negb_and negbK implybE. Qed.
Lemma itv_xx x bl br :
Interval (BOpen_if bl x) (BOpen_if br x) =i
if ~~ (bl || br) then pred1 x else pred0.
Proof.
by move: bl br => [] [] y /=; rewrite !inE 1?eq_sym (eqr_le, lter_anti).
Qed.
Lemma itv_gte ba xa bb xb : xb <= xa ?< if ~~ (ba || bb)
-> Interval (BOpen_if ba xa) (BOpen_if bb xb) =i pred0.
Proof.
move=> hx y; rewrite itv_boundlr inE /=.
by apply/negP => /andP [] /lersif_trans hy /hy {hy}; rewrite lersifNF.
Qed.
Lemma boundl_in_itv : forall ba xa b,
xa \in Interval (BOpen_if ba xa) b =
if ba then false else le_boundr (BClose xa) b.
Proof. by move=> [] xa [[] xb|] //=; rewrite inE lterr. Qed.
Lemma boundr_in_itv : forall bb xb a,
xb \in Interval a (BOpen_if bb xb) =
if bb then false else le_boundl a (BClose xb).
Proof. by move=> [] xb [[] xa|] //=; rewrite inE lterr ?andbT ?andbF. Qed.
Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
Lemma itvP : forall (x : R) (i : interval R), (x \in i) -> itv_rewrite i x.
Proof.
move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //;
do ?[by rewrite ltrW | by rewrite ltrWN | by rewrite ltrNW |
by rewrite (ltr_geF, ler_gtF)]];
rewrite ?(bound_in_itv) /le_boundl /le_boundr //=; do ?
[ by rewrite (@ler_trans _ x)
| by rewrite 1?ltrW // (@ltr_le_trans _ x)
| by rewrite 1?ltrW // (@ler_lt_trans _ x) // 1?ltrW
| by apply: negbTE; rewrite ler_gtF // (@ler_trans _ x)
| by apply: negbTE; rewrite ltr_geF // (@ltr_le_trans _ x) // 1?ltrW
| by apply: negbTE; rewrite ltr_geF // (@ler_lt_trans _ x)].
Qed.
Hint Rewrite intP.
Arguments itvP [x i].
Definition subitv (i1 i2 : interval R) :=
match i1, i2 with
| Interval a1 b1, Interval a2 b2 => le_boundl a2 a1 && le_boundr b1 b2
end.
Lemma subitvP : forall (i2 i1 : interval R),
(subitv i1 i2) -> {subset i1 <= i2}.
Proof.
by move=> [[[] a2|] [[] b2|]] [[[] a1|] [[] b1|]];
rewrite /subitv //; case/andP=> /= ha hb x hx; rewrite ?inE;
rewrite ?(ler_trans ha) ?(ler_lt_trans ha) ?(ltr_le_trans ha) //;
rewrite ?(ler_trans _ hb) ?(ltr_le_trans _ hb) ?(ler_lt_trans _ hb) //;
rewrite ?(itvP hx) //.
Qed.
Lemma subitvPr : forall (a b1 b2 : itv_bound R),
le_boundr b1 b2 -> {subset (Interval a b1) <= (Interval a b2)}.
Proof. by move=> a b1 b2 hb; apply: subitvP=> /=; rewrite hb andbT. Qed.
Lemma subitvPl : forall (a1 a2 b : itv_bound R),
le_boundl a2 a1 -> {subset (Interval a1 b) <= (Interval a2 b)}.
Proof. by move=> a1 a2 b ha; apply: subitvP=> /=; rewrite ha /=. Qed.
Lemma lersif_in_itv : forall ba bb xa xb x,
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) ->
xa <= xb ?< if ba || bb.
Proof.
by move=> ba bb xa xb y; rewrite itv_boundlr; case/andP; apply: lersif_trans.
Qed.
Lemma ltr_in_itv : forall ba bb xa xb x, ba || bb ->
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> xa < xb.
Proof.
move=> ba bb xa xb x; case bab: (_ || _) => // _.
by move/lersif_in_itv; rewrite bab.
Qed.
Lemma ler_in_itv : forall ba bb xa xb x,
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> xa <= xb.
Proof. by move=> ba bb xa xb x; move/lersif_in_itv; move/lersifW. Qed.
Lemma mem0_itvcc_xNx : forall x, (0 \in `[-x, x]) = (0 <= x).
Proof.
by move=> x; rewrite !inE; case hx: (0 <= _); rewrite (andbT, andbF) ?ge0_cp.
Qed.
Lemma mem0_itvoo_xNx : forall x, 0 \in `](-x), x[ = (0 < x).
Proof.
by move=> x; rewrite !inE; case hx: (0 < _); rewrite (andbT, andbF) ?gt0_cp.
Qed.
Lemma itv_splitI : forall a b, forall x,
x \in Interval a b = (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b).
Proof. by move=> [[] a|] [[] b|] x; rewrite ?inE ?andbT. Qed.
Lemma real_lersifN x y b : x \in Num.real -> y \in Num.real ->
x <= y ?< if ~~b = ~~ (y <= x ?< if b).
Proof. by case: b => [] xR yR /=; rewrite (real_ltrNge, real_lerNgt). Qed.
Lemma oppr_itv ba bb (xa xb x : R) :
(-x \in Interval (BOpen_if ba xa) (BOpen_if bb xb)) =
(x \in Interval (BOpen_if bb (-xb)) (BOpen_if ba (-xa))).
Proof. by move: ba bb => [] []; rewrite ?inE lter_oppr andbC lter_oppl. Qed.
Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[).
Proof. exact: oppr_itv. Qed.
Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]).
Proof. exact: oppr_itv. Qed.
Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[).
Proof. exact: oppr_itv. Qed.
Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]).
Proof. exact: oppr_itv. Qed.
End IntervalPo.
Notation BOpen := (BOpen_if true).
Notation BClose := (BOpen_if false).
Notation "`[ a , b ]" := (Interval (BClose a) (BClose b))
(at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope.
Notation "`] a , b ]" := (Interval (BOpen a) (BClose b))
(at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
Notation "`[ a , b [" := (Interval (BClose a) (BOpen b))
(at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope.
Notation "`] a , b [" := (Interval (BOpen a) (BOpen b))
(at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b))
(at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b))
(at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _))
(at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _))
(at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope.
Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _))
(at level 0, format "`] -oo , '+oo' [") : ring_scope.
Notation "x <= y ?< 'if' b" := (lersif x y b)
(at level 70, y at next level,
format "x '[hv' <= y '/' ?< 'if' b ']'") : ring_scope.
Section IntervalOrdered.
Variable R : realDomainType.
Lemma lersifN (x y : R) b : (x <= y ?< if ~~ b) = ~~ (y <= x ?< if b).
Proof. by rewrite real_lersifN ?num_real. Qed.
Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b ->
forall y, y \in Interval a b =
(y \in Interval a (BOpen_if (~~ bc) xc))
|| (y \in Interval (BOpen_if bc xc) b).
Proof.
move=> hxc y; rewrite !itv_boundlr [le_boundr]lock /=.
have [la /=|nla /=] := boolP (le_boundl a _); rewrite -lock.
have [lb /=|nlb /=] := boolP (le_boundr _ b); rewrite ?andbT ?andbF ?orbF //.
by case: bc => //=; case: ltrgtP.
symmetry; apply: contraNF nlb; rewrite /le_boundr /=.
case: b hxc => // bb xb hxc hyc.
suff /(lersif_trans hyc) : xc <= xb ?< if bb.
by case: bc {hyc} => //= /lersifS.
by case: a bb hxc {la} => [[] ?|] [] /= /itvP->.
symmetry; apply: contraNF nla => /andP [hc _].
case: a hxc hc => [[] xa|] hxc; rewrite /le_boundl //=.
by move=> /lersifW /(ltr_le_trans _) -> //; move: b hxc=> [[] ?|] /itvP->.
by move=> /lersifW /(ler_trans _) -> //; move: b hxc=> [[] ?|] /itvP->.
Qed.
Lemma itv_splitU2 (x : R) a b : x \in Interval a b ->
forall y, y \in Interval a b =
[|| (y \in Interval a (BOpen x)), (y == x)
| (y \in Interval (BOpen x) b)].
Proof.
move=> xab y; rewrite (itv_splitU false xab y); congr (_ || _).
rewrite (@itv_splitU x true _ _ _ y); first by rewrite itv_xx inE.
by move: xab; rewrite boundl_in_itv itv_boundlr => /andP [].
Qed.
End IntervalOrdered.
Section IntervalField.
Variable R : realFieldType.
Lemma mid_in_itv : forall ba bb (xa xb : R), xa <= xb ?< if (ba || bb)
-> mid xa xb \in Interval (BOpen_if ba xa) (BOpen_if bb xb).
Proof.
by move=> [] [] xa xb /= hx; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltrW.
Qed.
Lemma mid_in_itvoo : forall (xa xb : R), xa < xb -> mid xa xb \in `]xa, xb[.
Proof. by move=> xa xb hx; apply: mid_in_itv. Qed.
Lemma mid_in_itvcc : forall (xa xb : R), xa <= xb -> mid xa xb \in `[xa, xb].
Proof. by move=> xa xb hx; apply: mid_in_itv. Qed.
End IntervalField.
From mathcomp
Require Import ssrfun ssrbool eqtype ssrnat seq div choice fintype.
From mathcomp
Require Import bigop ssralg finset fingroup zmodp ssrint ssrnum.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Import GRing.Theory Num.Theory.
Local Notation mid x y := ((x + y) / 2%:R).
Section IntervalPo.
CoInductive itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
Notation BOpen := (BOpen_if true).
Notation BClose := (BOpen_if false).
CoInductive interval (T : Type) := Interval of itv_bound T & itv_bound T.
Variable (R : numDomainType).
Definition pred_of_itv (i : interval R) : pred R :=
[pred x | let: Interval l u := i in
match l with
| BOpen a => a < x
| BClose a => a <= x
| BInfty => true
end &&
match u with
| BOpen b => x < b
| BClose b => x <= b
| BInfty => true
end].
Canonical Structure itvPredType := Eval hnf in mkPredType pred_of_itv.
Notation "`[ a , b ]" := (Interval (BClose a) (BClose b))
(at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope.
Notation "`] a , b ]" := (Interval (BOpen a) (BClose b))
(at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
Notation "`[ a , b [" := (Interval (BClose a) (BOpen b))
(at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope.
Notation "`] a , b [" := (Interval (BOpen a) (BOpen b))
(at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b))
(at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b))
(at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _))
(at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _))
(at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope.
Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _))
(at level 0, format "`] -oo , '+oo' [") : ring_scope.
Definition itv_rewrite (i : interval R) x : Type :=
let: Interval l u := i in
(match l with
| BClose a => (a <= x) * (x < a = false)
| BOpen a => (a <= x) * (a < x) * (x <= a = false)
| BInfty => forall x : R, x == x
end *
match u with
| BClose b => (x <= b) * (b < x = false)
| BOpen b => (x <= b) * (x < b) * (b <= x = false)
| BInfty => forall x : R, x == x
end *
match l, u with
| BClose a, BClose b =>
(a <= b) * (b < a = false) * (a \in `[a, b]) * (b \in `[a, b])
| BClose a, BOpen b =>
(a <= b) * (a < b) * (b <= a = false)
* (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b])
| BOpen a, BClose b =>
(a <= b) * (a < b) * (b <= a = false)
* (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b])
| BOpen a, BOpen b =>
(a <= b) * (a < b) * (b <= a = false)
* (a \in `[a, b]) * (a \in `[a, b[)* (b \in `[a, b]) * (b \in `]a, b])
| _, _ => forall x : R, x == x
end)%type.
Definition itv_decompose (i : interval R) x : Prop :=
let: Interval l u := i in
((match l with
| BClose a => (a <= x) : Prop
| BOpen a => (a < x) : Prop
| BInfty => True
end : Prop) *
(match u with
| BClose b => (x <= b) : Prop
| BOpen b => (x < b) : Prop
| BInfty => True
end : Prop))%type.
Lemma itv_dec : forall (x : R) (i : interval R),
reflect (itv_decompose i x) (x \in i).
Proof. by move=> x [[[] a|] [[] b|]]; apply: (iffP andP); case. Qed.
Arguments itv_dec [x i].
Definition lersif (x y : R) b := if b then x < y else x <= y.
Local Notation "x <= y ?< 'if' b" := (lersif x y b)
(at level 70, y at next level,
format "x '[hv' <= y '/' ?< 'if' b ']'") : ring_scope.
Lemma lersifxx x b: (x <= x ?< if b) = ~~ b.
Proof. by case: b; rewrite /= lterr. Qed.
Lemma lersif_trans x y z b1 b2 :
x <= y ?< if b1 -> y <= z ?< if b2 -> x <= z ?< if b1 || b2.
Proof.
case: b1; first by case: b2; [apply: ltr_trans | apply: ltr_le_trans].
by case: b2; [apply: ler_lt_trans | apply: ler_trans].
Qed.
Lemma lersifW b x y : x <= y ?< if b -> x <= y.
Proof. by case: b => //; move/ltrW. Qed.
Lemma lersifNF x y b : y <= x ?< if ~~ b -> x <= y ?< if b = false.
Proof. by case: b => /= [/ler_gtF|/ltr_geF]. Qed.
Lemma lersifS x y b : x < y -> x <= y ?< if b.
Proof. by case: b => //= /ltrW. Qed.
Lemma lersifT x y : x <= y ?< if true = (x < y). Proof. by []. Qed.
Lemma lersifF x y : x <= y ?< if false = (x <= y). Proof. by []. Qed.
Definition le_boundl b1 b2 :=
match b1, b2 with
| BOpen_if b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if (~~ b2 && b1)
| BOpen_if _ _, BInfty => false
| _, _ => true
end.
Definition le_boundr b1 b2 :=
match b1, b2 with
| BOpen_if b1 x1, BOpen_if b2 x2 => x1 <= x2 ?< if (~~ b1 && b2)
| BInfty, BOpen_if _ _ => false
| _, _ => true
end.
Lemma itv_boundlr bl br x :
(x \in Interval bl br) =
(le_boundl bl (BClose x)) && (le_boundr (BClose x) br).
Proof. by move: bl br => [[] a|] [[] b|]. Qed.
Lemma le_boundr_refl : reflexive le_boundr.
Proof. by move=> [[] b|]; rewrite /le_boundr /= ?lerr. Qed.
Hint Resolve le_boundr_refl.
Lemma le_boundl_refl : reflexive le_boundl.
Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed.
Hint Resolve le_boundl_refl.
Lemma le_boundl_bb x b1 b2 :
le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).
Proof. by rewrite /le_boundl lersifxx andbC negb_and negbK implybE. Qed.
Lemma le_boundr_bb x b1 b2 :
le_boundr (BOpen_if b1 x) (BOpen_if b2 x) = (b2 ==> b1).
Proof. by rewrite /le_boundr lersifxx andbC negb_and negbK implybE. Qed.
Lemma itv_xx x bl br :
Interval (BOpen_if bl x) (BOpen_if br x) =i
if ~~ (bl || br) then pred1 x else pred0.
Proof.
by move: bl br => [] [] y /=; rewrite !inE 1?eq_sym (eqr_le, lter_anti).
Qed.
Lemma itv_gte ba xa bb xb : xb <= xa ?< if ~~ (ba || bb)
-> Interval (BOpen_if ba xa) (BOpen_if bb xb) =i pred0.
Proof.
move=> hx y; rewrite itv_boundlr inE /=.
by apply/negP => /andP [] /lersif_trans hy /hy {hy}; rewrite lersifNF.
Qed.
Lemma boundl_in_itv : forall ba xa b,
xa \in Interval (BOpen_if ba xa) b =
if ba then false else le_boundr (BClose xa) b.
Proof. by move=> [] xa [[] xb|] //=; rewrite inE lterr. Qed.
Lemma boundr_in_itv : forall bb xb a,
xb \in Interval a (BOpen_if bb xb) =
if bb then false else le_boundl a (BClose xb).
Proof. by move=> [] xb [[] xa|] //=; rewrite inE lterr ?andbT ?andbF. Qed.
Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
Lemma itvP : forall (x : R) (i : interval R), (x \in i) -> itv_rewrite i x.
Proof.
move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //;
do ?[by rewrite ltrW | by rewrite ltrWN | by rewrite ltrNW |
by rewrite (ltr_geF, ler_gtF)]];
rewrite ?(bound_in_itv) /le_boundl /le_boundr //=; do ?
[ by rewrite (@ler_trans _ x)
| by rewrite 1?ltrW // (@ltr_le_trans _ x)
| by rewrite 1?ltrW // (@ler_lt_trans _ x) // 1?ltrW
| by apply: negbTE; rewrite ler_gtF // (@ler_trans _ x)
| by apply: negbTE; rewrite ltr_geF // (@ltr_le_trans _ x) // 1?ltrW
| by apply: negbTE; rewrite ltr_geF // (@ler_lt_trans _ x)].
Qed.
Hint Rewrite intP.
Arguments itvP [x i].
Definition subitv (i1 i2 : interval R) :=
match i1, i2 with
| Interval a1 b1, Interval a2 b2 => le_boundl a2 a1 && le_boundr b1 b2
end.
Lemma subitvP : forall (i2 i1 : interval R),
(subitv i1 i2) -> {subset i1 <= i2}.
Proof.
by move=> [[[] a2|] [[] b2|]] [[[] a1|] [[] b1|]];
rewrite /subitv //; case/andP=> /= ha hb x hx; rewrite ?inE;
rewrite ?(ler_trans ha) ?(ler_lt_trans ha) ?(ltr_le_trans ha) //;
rewrite ?(ler_trans _ hb) ?(ltr_le_trans _ hb) ?(ler_lt_trans _ hb) //;
rewrite ?(itvP hx) //.
Qed.
Lemma subitvPr : forall (a b1 b2 : itv_bound R),
le_boundr b1 b2 -> {subset (Interval a b1) <= (Interval a b2)}.
Proof. by move=> a b1 b2 hb; apply: subitvP=> /=; rewrite hb andbT. Qed.
Lemma subitvPl : forall (a1 a2 b : itv_bound R),
le_boundl a2 a1 -> {subset (Interval a1 b) <= (Interval a2 b)}.
Proof. by move=> a1 a2 b ha; apply: subitvP=> /=; rewrite ha /=. Qed.
Lemma lersif_in_itv : forall ba bb xa xb x,
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) ->
xa <= xb ?< if ba || bb.
Proof.
by move=> ba bb xa xb y; rewrite itv_boundlr; case/andP; apply: lersif_trans.
Qed.
Lemma ltr_in_itv : forall ba bb xa xb x, ba || bb ->
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> xa < xb.
Proof.
move=> ba bb xa xb x; case bab: (_ || _) => // _.
by move/lersif_in_itv; rewrite bab.
Qed.
Lemma ler_in_itv : forall ba bb xa xb x,
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) -> xa <= xb.
Proof. by move=> ba bb xa xb x; move/lersif_in_itv; move/lersifW. Qed.
Lemma mem0_itvcc_xNx : forall x, (0 \in `[-x, x]) = (0 <= x).
Proof.
by move=> x; rewrite !inE; case hx: (0 <= _); rewrite (andbT, andbF) ?ge0_cp.
Qed.
Lemma mem0_itvoo_xNx : forall x, 0 \in `](-x), x[ = (0 < x).
Proof.
by move=> x; rewrite !inE; case hx: (0 < _); rewrite (andbT, andbF) ?gt0_cp.
Qed.
Lemma itv_splitI : forall a b, forall x,
x \in Interval a b = (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b).
Proof. by move=> [[] a|] [[] b|] x; rewrite ?inE ?andbT. Qed.
Lemma real_lersifN x y b : x \in Num.real -> y \in Num.real ->
x <= y ?< if ~~b = ~~ (y <= x ?< if b).
Proof. by case: b => [] xR yR /=; rewrite (real_ltrNge, real_lerNgt). Qed.
Lemma oppr_itv ba bb (xa xb x : R) :
(-x \in Interval (BOpen_if ba xa) (BOpen_if bb xb)) =
(x \in Interval (BOpen_if bb (-xb)) (BOpen_if ba (-xa))).
Proof. by move: ba bb => [] []; rewrite ?inE lter_oppr andbC lter_oppl. Qed.
Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[).
Proof. exact: oppr_itv. Qed.
Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]).
Proof. exact: oppr_itv. Qed.
Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[).
Proof. exact: oppr_itv. Qed.
Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]).
Proof. exact: oppr_itv. Qed.
End IntervalPo.
Notation BOpen := (BOpen_if true).
Notation BClose := (BOpen_if false).
Notation "`[ a , b ]" := (Interval (BClose a) (BClose b))
(at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope.
Notation "`] a , b ]" := (Interval (BOpen a) (BClose b))
(at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
Notation "`[ a , b [" := (Interval (BClose a) (BOpen b))
(at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope.
Notation "`] a , b [" := (Interval (BOpen a) (BOpen b))
(at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b))
(at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b))
(at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _))
(at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _))
(at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope.
Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _))
(at level 0, format "`] -oo , '+oo' [") : ring_scope.
Notation "x <= y ?< 'if' b" := (lersif x y b)
(at level 70, y at next level,
format "x '[hv' <= y '/' ?< 'if' b ']'") : ring_scope.
Section IntervalOrdered.
Variable R : realDomainType.
Lemma lersifN (x y : R) b : (x <= y ?< if ~~ b) = ~~ (y <= x ?< if b).
Proof. by rewrite real_lersifN ?num_real. Qed.
Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b ->
forall y, y \in Interval a b =
(y \in Interval a (BOpen_if (~~ bc) xc))
|| (y \in Interval (BOpen_if bc xc) b).
Proof.
move=> hxc y; rewrite !itv_boundlr [le_boundr]lock /=.
have [la /=|nla /=] := boolP (le_boundl a _); rewrite -lock.
have [lb /=|nlb /=] := boolP (le_boundr _ b); rewrite ?andbT ?andbF ?orbF //.
by case: bc => //=; case: ltrgtP.
symmetry; apply: contraNF nlb; rewrite /le_boundr /=.
case: b hxc => // bb xb hxc hyc.
suff /(lersif_trans hyc) : xc <= xb ?< if bb.
by case: bc {hyc} => //= /lersifS.
by case: a bb hxc {la} => [[] ?|] [] /= /itvP->.
symmetry; apply: contraNF nla => /andP [hc _].
case: a hxc hc => [[] xa|] hxc; rewrite /le_boundl //=.
by move=> /lersifW /(ltr_le_trans _) -> //; move: b hxc=> [[] ?|] /itvP->.
by move=> /lersifW /(ler_trans _) -> //; move: b hxc=> [[] ?|] /itvP->.
Qed.
Lemma itv_splitU2 (x : R) a b : x \in Interval a b ->
forall y, y \in Interval a b =
[|| (y \in Interval a (BOpen x)), (y == x)
| (y \in Interval (BOpen x) b)].
Proof.
move=> xab y; rewrite (itv_splitU false xab y); congr (_ || _).
rewrite (@itv_splitU x true _ _ _ y); first by rewrite itv_xx inE.
by move: xab; rewrite boundl_in_itv itv_boundlr => /andP [].
Qed.
End IntervalOrdered.
Section IntervalField.
Variable R : realFieldType.
Lemma mid_in_itv : forall ba bb (xa xb : R), xa <= xb ?< if (ba || bb)
-> mid xa xb \in Interval (BOpen_if ba xa) (BOpen_if bb xb).
Proof.
by move=> [] [] xa xb /= hx; apply/itv_dec=> /=; rewrite ?midf_lte // ?ltrW.
Qed.
Lemma mid_in_itvoo : forall (xa xb : R), xa < xb -> mid xa xb \in `]xa, xb[.
Proof. by move=> xa xb hx; apply: mid_in_itv. Qed.
Lemma mid_in_itvcc : forall (xa xb : R), xa <= xb -> mid xa xb \in `[xa, xb].
Proof. by move=> xa xb hx; apply: mid_in_itv. Qed.
End IntervalField.