Library mathcomp.algebra.interval
+ +
+(* (c) Copyright 2006-2016 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.
+ +
+
+
++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).
+ +
+ +
+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.
+ +
+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).
+ +
+ +
+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.
+ +
+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.
+