Library mathcomp.algebra.interval
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
This file provide support for intervals in numerical and real domains.
The datatype (interval R) gives a formal characterization of an
interval, as the pair of its right and left bounds.
interval R == the type of formal intervals on R.
x \in i == when i is a formal interval on a numeric domain,
\in can be used to test membership.
itvP x_in_i == where x_in_i has type x \in i, if i is ground,
gives a set of rewrite rules that x_in_i imply.
x <= y ?< if c == x is smaller than y, and strictly if c is true
We provide a set of notations to write intervals (see below)
` [a, b], ` ]a, b], ..., ` ]-oo, a], ..., ` ]-oo, +oo[
We also provide the lemma subitvP which computes the inequalities one
needs to prove when trying to prove the inclusion of intervals.
Remark that we cannot implement a boolean comparison test for intervals
on an arbitrary numeric domains, for this problem might be undecidable.
Note also that type (interval R) may contain several inhabitants coding
for the same interval. However, this pathological issues do nor arise
when R is a real domain: we could provide a specific theory for this
important case.
See also ``Formal proofs in real algebraic geometry: from ordered fields
to quantifier elimination'', LMCS journal, 2012
by Cyril Cohen and Assia Mahboubi
And "Formalized algebraic numbers: construction and first-order theory"
Cyril Cohen, PhD, 2012, section 4.3.
Set Implicit Arguments.
Local Open Scope ring_scope.
Import GRing.Theory Num.Theory.
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.
We provide the 9 following notations to help writing formal intervals
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.
(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.
we compute a set of rewrite rules associated to an interval
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 ⇒ ∀ 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 ⇒ ∀ 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])
| _, _ ⇒ ∀ 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 : ∀ (x : R) (i : interval R),
reflect (itv_decompose i x) (x \in i).
Implicit Arguments itv_dec [x i].
Definition lersif (x y : R) b := if b then x < y else x ≤ y.
Lemma lersifxx x b: (x ≤ x ?< if b) = ~~ b.
Lemma lersif_trans x y z b1 b2 :
x ≤ y ?< if b1 → y ≤ z ?< if b2 → x ≤ z ?< if b1 || b2.
Lemma lersifW b x y : x ≤ y ?< if b → x ≤ y.
Lemma lersifNF x y b : y ≤ x ?< if ~~ b → x ≤ y ?< if b = false.
Lemma lersifS x y b : x < y → x ≤ y ?< if b.
Lemma lersifT x y : x ≤ y ?< if true = (x < y).
Lemma lersifF x y : x ≤ y ?< if false = (x ≤ y).
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).
Lemma le_boundr_refl : reflexive le_boundr.
Hint Resolve le_boundr_refl.
Lemma le_boundl_refl : reflexive le_boundl.
Hint Resolve le_boundl_refl.
Lemma le_boundl_bb x b1 b2 :
le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).
Lemma le_boundr_bb x b1 b2 :
le_boundr (BOpen_if b1 x) (BOpen_if b2 x) = (b2 ==> b1).
Lemma itv_xx x bl br :
Interval (BOpen_if bl x) (BOpen_if br x) =i
if ~~ (bl || br) then pred1 x else pred0.
Lemma itv_gte ba xa bb xb : xb ≤ xa ?< if ~~ (ba || bb)
→ Interval (BOpen_if ba xa) (BOpen_if bb xb) =i pred0.
Lemma boundl_in_itv : ∀ ba xa b,
xa \in Interval (BOpen_if ba xa) b =
if ba then false else le_boundr (BClose xa) b.
Lemma boundr_in_itv : ∀ bb xb a,
xb \in Interval a (BOpen_if bb xb) =
if bb then false else le_boundl a (BClose xb).
Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
Lemma itvP : ∀ (x : R) (i : interval R), (x \in i) → itv_rewrite i x.
Hint Rewrite intP.
Implicit 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 : ∀ (i2 i1 : interval R),
(subitv i1 i2) → {subset i1 ≤ i2}.
Lemma subitvPr : ∀ (a b1 b2 : itv_bound R),
le_boundr b1 b2 → {subset (Interval a b1) ≤ (Interval a b2)}.
Lemma subitvPl : ∀ (a1 a2 b : itv_bound R),
le_boundl a2 a1 → {subset (Interval a1 b) ≤ (Interval a2 b)}.
Lemma lersif_in_itv : ∀ ba bb xa xb x,
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) →
xa ≤ xb ?< if ba || bb.
Lemma ltr_in_itv : ∀ ba bb xa xb x, ba || bb →
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) → xa < xb.
Lemma ler_in_itv : ∀ ba bb xa xb x,
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) → xa ≤ xb.
Lemma mem0_itvcc_xNx : ∀ x, (0 \in `[-x, x]) = (0 ≤ x).
Lemma mem0_itvoo_xNx : ∀ x, 0 \in `](-x), x[ = (0 < x).
Lemma itv_splitI : ∀ a b, ∀ x,
x \in Interval a b = (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b).
Lemma real_lersifN x y b : x \in Num.real → y \in Num.real →
x ≤ y ?< if ~~b = ~~ (y ≤ x ?< if b).
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))).
Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[).
Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]).
Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[).
Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]).
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).
Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b →
∀ y, y \in Interval a b =
(y \in Interval a (BOpen_if (~~ bc) xc))
|| (y \in Interval (BOpen_if bc xc) b).
Lemma itv_splitU2 (x : R) a b : x \in Interval a b →
∀ y, y \in Interval a b =
[|| (y \in Interval a (BOpen x)), (y == x)
| (y \in Interval (BOpen x) b)].
End IntervalOrdered.
Section IntervalField.
Variable R : realFieldType.
Lemma mid_in_itv : ∀ ba bb (xa xb : R), xa ≤ xb ?< if (ba || bb)
→ mid xa xb \in Interval (BOpen_if ba xa) (BOpen_if bb xb).
Lemma mid_in_itvoo : ∀ (xa xb : R), xa < xb → mid xa xb \in `]xa, xb[.
Lemma mid_in_itvcc : ∀ (xa xb : R), xa ≤ xb → mid xa xb \in `[xa, xb].
End IntervalField.
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 ⇒ ∀ 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 ⇒ ∀ 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])
| _, _ ⇒ ∀ 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 : ∀ (x : R) (i : interval R),
reflect (itv_decompose i x) (x \in i).
Implicit Arguments itv_dec [x i].
Definition lersif (x y : R) b := if b then x < y else x ≤ y.
Lemma lersifxx x b: (x ≤ x ?< if b) = ~~ b.
Lemma lersif_trans x y z b1 b2 :
x ≤ y ?< if b1 → y ≤ z ?< if b2 → x ≤ z ?< if b1 || b2.
Lemma lersifW b x y : x ≤ y ?< if b → x ≤ y.
Lemma lersifNF x y b : y ≤ x ?< if ~~ b → x ≤ y ?< if b = false.
Lemma lersifS x y b : x < y → x ≤ y ?< if b.
Lemma lersifT x y : x ≤ y ?< if true = (x < y).
Lemma lersifF x y : x ≤ y ?< if false = (x ≤ y).
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).
Lemma le_boundr_refl : reflexive le_boundr.
Hint Resolve le_boundr_refl.
Lemma le_boundl_refl : reflexive le_boundl.
Hint Resolve le_boundl_refl.
Lemma le_boundl_bb x b1 b2 :
le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).
Lemma le_boundr_bb x b1 b2 :
le_boundr (BOpen_if b1 x) (BOpen_if b2 x) = (b2 ==> b1).
Lemma itv_xx x bl br :
Interval (BOpen_if bl x) (BOpen_if br x) =i
if ~~ (bl || br) then pred1 x else pred0.
Lemma itv_gte ba xa bb xb : xb ≤ xa ?< if ~~ (ba || bb)
→ Interval (BOpen_if ba xa) (BOpen_if bb xb) =i pred0.
Lemma boundl_in_itv : ∀ ba xa b,
xa \in Interval (BOpen_if ba xa) b =
if ba then false else le_boundr (BClose xa) b.
Lemma boundr_in_itv : ∀ bb xb a,
xb \in Interval a (BOpen_if bb xb) =
if bb then false else le_boundl a (BClose xb).
Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
Lemma itvP : ∀ (x : R) (i : interval R), (x \in i) → itv_rewrite i x.
Hint Rewrite intP.
Implicit 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 : ∀ (i2 i1 : interval R),
(subitv i1 i2) → {subset i1 ≤ i2}.
Lemma subitvPr : ∀ (a b1 b2 : itv_bound R),
le_boundr b1 b2 → {subset (Interval a b1) ≤ (Interval a b2)}.
Lemma subitvPl : ∀ (a1 a2 b : itv_bound R),
le_boundl a2 a1 → {subset (Interval a1 b) ≤ (Interval a2 b)}.
Lemma lersif_in_itv : ∀ ba bb xa xb x,
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) →
xa ≤ xb ?< if ba || bb.
Lemma ltr_in_itv : ∀ ba bb xa xb x, ba || bb →
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) → xa < xb.
Lemma ler_in_itv : ∀ ba bb xa xb x,
x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) → xa ≤ xb.
Lemma mem0_itvcc_xNx : ∀ x, (0 \in `[-x, x]) = (0 ≤ x).
Lemma mem0_itvoo_xNx : ∀ x, 0 \in `](-x), x[ = (0 < x).
Lemma itv_splitI : ∀ a b, ∀ x,
x \in Interval a b = (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b).
Lemma real_lersifN x y b : x \in Num.real → y \in Num.real →
x ≤ y ?< if ~~b = ~~ (y ≤ x ?< if b).
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))).
Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[).
Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]).
Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[).
Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]).
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).
Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b →
∀ y, y \in Interval a b =
(y \in Interval a (BOpen_if (~~ bc) xc))
|| (y \in Interval (BOpen_if bc xc) b).
Lemma itv_splitU2 (x : R) a b : x \in Interval a b →
∀ y, y \in Interval a b =
[|| (y \in Interval a (BOpen x)), (y == x)
| (y \in Interval (BOpen x) b)].
End IntervalOrdered.
Section IntervalField.
Variable R : realFieldType.
Lemma mid_in_itv : ∀ ba bb (xa xb : R), xa ≤ xb ?< if (ba || bb)
→ mid xa xb \in Interval (BOpen_if ba xa) (BOpen_if bb xb).
Lemma mid_in_itvoo : ∀ (xa xb : R), xa < xb → mid xa xb \in `]xa, xb[.
Lemma mid_in_itvcc : ∀ (xa xb : R), xa ≤ xb → mid xa xb \in `[xa, xb].
End IntervalField.