Library mathcomp.algebra.interval
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import div fintype bigop order ssralg finset fingroup.
From mathcomp Require Import ssrnum.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import div fintype bigop order ssralg finset fingroup.
From mathcomp Require Import ssrnum.
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 Order.TTheory GRing.Theory Num.Theory.
Section LersifPo.
Variable R : numDomainType.
Implicit Types (b : bool) (x y z : R).
Definition lersif (x y : R) b := if b then x < y else x ≤ y.
Lemma subr_lersifr0 b (x y : R) : (y - x ≤ 0 ?< if b) = (y ≤ x ?< if b).
Lemma subr_lersif0r b (x y : R) : (0 ≤ y - x ?< if b) = (x ≤ y ?< if b).
Definition subr_lersif0 := (subr_lersifr0, subr_lersif0r).
Lemma lersif_trans x y z b1 b2 :
x ≤ y ?< if b1 → y ≤ z ?< if b2 → x ≤ z ?< if b1 || b2.
Lemma lersif01 b : 0 ≤ 1 ?< if b.
Lemma lersif_anti b1 b2 x y :
(x ≤ y ?< if b1) && (y ≤ x ?< if b2) =
if b1 || b2 then false else x == y.
Lemma lersifxx x b : (x ≤ x ?< if b) = ~~ b.
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).
Lemma lersif_oppl b x y : - x ≤ y ?< if b = (- y ≤ x ?< if b).
Lemma lersif_oppr b x y : x ≤ - y ?< if b = (y ≤ - x ?< if b).
Lemma lersif_0oppr b x : 0 ≤ - x ?< if b = (x ≤ 0 ?< if b).
Lemma lersif_oppr0 b x : - x ≤ 0 ?< if b = (0 ≤ x ?< if b).
Lemma lersif_opp2 b : {mono -%R : x y /~ x ≤ y ?< if b}.
Definition lersif_oppE := (lersif_0oppr, lersif_oppr0, lersif_opp2).
Lemma lersif_add2l b x : {mono +%R x : y z / y ≤ z ?< if b}.
Lemma lersif_add2r b x : {mono +%R^~ x : y z / y ≤ z ?< if b}.
Definition lersif_add2 := (lersif_add2l, lersif_add2r).
Lemma lersif_subl_addr b x y z : (x - y ≤ z ?< if b) = (x ≤ z + y ?< if b).
Lemma lersif_subr_addr b x y z : (x ≤ y - z ?< if b) = (x + z ≤ y ?< if b).
Definition lersif_sub_addr := (lersif_subl_addr, lersif_subr_addr).
Lemma lersif_subl_addl b x y z : (x - y ≤ z ?< if b) = (x ≤ y + z ?< if b).
Lemma lersif_subr_addl b x y z : (x ≤ y - z ?< if b) = (z + x ≤ y ?< if b).
Definition lersif_sub_addl := (lersif_subl_addl, lersif_subr_addl).
Lemma lersif_andb x y : {morph lersif x y : p q / p || q >-> p && q}.
Lemma lersif_orb x y : {morph lersif x y : p q / p && q >-> p || q}.
Lemma lersif_imply b1 b2 r1 r2 :
b2 ==> b1 → r1 ≤ r2 ?< if b1 → r1 ≤ r2 ?< if b2.
Lemma lersifW b x y : x ≤ y ?< if b → x ≤ y.
Lemma ltrW_lersif b x y : x < y → x ≤ y ?< if b.
Lemma lersif_pmul2l b x : 0 < x → {mono *%R x : y z / y ≤ z ?< if b}.
Lemma lersif_pmul2r b x : 0 < x → {mono *%R^~ x : y z / y ≤ z ?< if b}.
Lemma lersif_nmul2l b x : x < 0 → {mono *%R x : y z /~ y ≤ z ?< if b}.
Lemma lersif_nmul2r b x : x < 0 → {mono *%R^~ x : y z /~ y ≤ z ?< if b}.
Lemma real_lersifN x y b : x \is Num.real → y \is Num.real →
x ≤ y ?< if ~~b = ~~ (y ≤ x ?< if b).
Lemma real_lersif_norml b x y :
x \is Num.real →
(`|x| ≤ y ?< if b) = ((- y ≤ x ?< if b) && (x ≤ y ?< if b)).
Lemma real_lersif_normr b x y :
y \is Num.real →
(x ≤ `|y| ?< if b) = ((x ≤ y ?< if b) || (x ≤ - y ?< if b)).
Lemma lersif_nnormr b x y : y ≤ 0 ?< if ~~ b → (`|x| ≤ y ?< if b) = false.
End LersifPo.
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 LersifOrdered.
Variable (R : realDomainType) (b : bool) (x y z e : R).
Lemma lersifN : (x ≤ y ?< if ~~ b) = ~~ (y ≤ x ?< if b).
Lemma lersif_norml :
(`|x| ≤ y ?< if b) = (- y ≤ x ?< if b) && (x ≤ y ?< if b).
Lemma lersif_normr :
(x ≤ `|y| ?< if b) = (x ≤ y ?< if b) || (x ≤ - y ?< if b).
Lemma lersif_distl :
(`|x - y| ≤ e ?< if b) = (y - e ≤ x ?< if b) && (x ≤ y + e ?< if b).
Lemma lersif_minr :
(x ≤ Num.min y z ?< if b) = (x ≤ y ?< if b) && (x ≤ z ?< if b).
Lemma lersif_minl :
(Num.min y z ≤ x ?< if b) = (y ≤ x ?< if b) || (z ≤ x ?< if b).
Lemma lersif_maxr :
(x ≤ Num.max y z ?< if b) = (x ≤ y ?< if b) || (x ≤ z ?< if b).
Lemma lersif_maxl :
(Num.max y z ≤ x ?< if b) = (y ≤ x ?< if b) && (z ≤ x ?< if b).
End LersifOrdered.
Section LersifField.
Variable (F : numFieldType) (b : bool) (z x y : F).
Lemma lersif_pdivl_mulr : 0 < z → x ≤ y / z ?< if b = (x × z ≤ y ?< if b).
Lemma lersif_pdivr_mulr : 0 < z → y / z ≤ x ?< if b = (y ≤ x × z ?< if b).
Lemma lersif_pdivl_mull : 0 < z → x ≤ z^-1 × y ?< if b = (z × x ≤ y ?< if b).
Lemma lersif_pdivr_mull : 0 < z → z^-1 × y ≤ x ?< if b = (y ≤ z × x ?< if b).
Lemma lersif_ndivl_mulr : z < 0 → x ≤ y / z ?< if b = (y ≤ x × z ?< if b).
Lemma lersif_ndivr_mulr : z < 0 → y / z ≤ x ?< if b = (x × z ≤ y ?< if b).
Lemma lersif_ndivl_mull : z < 0 → x ≤ z^-1 × y ?< if b = (y ≤z × x ?< if b).
Lemma lersif_ndivr_mull : z < 0 → z^-1 × y ≤ x ?< if b = (z × x ≤ y ?< if b).
End LersifField.
Variant itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
Notation BOpen := (BOpen_if true).
Notation BClose := (BOpen_if false).
Variant interval (T : Type) := Interval of itv_bound T & itv_bound T.
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.
Section IntervalEq.
Variable T : eqType.
Definition eq_itv_bound (b1 b2 : itv_bound T) : bool :=
match b1, b2 with
| BOpen_if a x, BOpen_if b y ⇒ (a == b) && (x == y)
| BInfty, BInfty ⇒ true
| _, _ ⇒ false
end.
Lemma eq_itv_boundP : Equality.axiom eq_itv_bound.
Canonical itv_bound_eqMixin := EqMixin eq_itv_boundP.
Canonical itv_bound_eqType :=
Eval hnf in EqType (itv_bound T) itv_bound_eqMixin.
Definition eqitv (x y : interval T) : bool :=
let: Interval x x' := x in
let: Interval y y' := y in (x == y) && (x' == y').
Lemma eqitvP : Equality.axiom eqitv.
Canonical interval_eqMixin := EqMixin eqitvP.
Canonical interval_eqType := Eval hnf in EqType (interval T) interval_eqMixin.
End IntervalEq.
Section IntervalPo.
Variable R : numDomainType.
Definition pred_of_itv (i : interval R) : pred R :=
[pred x | let: Interval l u := i in
match l with
| BOpen_if b lb ⇒ lb ≤ x ?< if b
| BInfty ⇒ true
end &&
match u with
| BOpen_if b ub ⇒ x ≤ ub ?< if b
| BInfty ⇒ true
end].
Canonical Structure itvPredType := PredType pred_of_itv.
(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.
Section IntervalEq.
Variable T : eqType.
Definition eq_itv_bound (b1 b2 : itv_bound T) : bool :=
match b1, b2 with
| BOpen_if a x, BOpen_if b y ⇒ (a == b) && (x == y)
| BInfty, BInfty ⇒ true
| _, _ ⇒ false
end.
Lemma eq_itv_boundP : Equality.axiom eq_itv_bound.
Canonical itv_bound_eqMixin := EqMixin eq_itv_boundP.
Canonical itv_bound_eqType :=
Eval hnf in EqType (itv_bound T) itv_bound_eqMixin.
Definition eqitv (x y : interval T) : bool :=
let: Interval x x' := x in
let: Interval y y' := y in (x == y) && (x' == y').
Lemma eqitvP : Equality.axiom eqitv.
Canonical interval_eqMixin := EqMixin eqitvP.
Canonical interval_eqType := Eval hnf in EqType (interval T) interval_eqMixin.
End IntervalEq.
Section IntervalPo.
Variable R : numDomainType.
Definition pred_of_itv (i : interval R) : pred R :=
[pred x | let: Interval l u := i in
match l with
| BOpen_if b lb ⇒ lb ≤ x ?< if b
| BInfty ⇒ true
end &&
match u with
| BOpen_if b ub ⇒ x ≤ ub ?< if b
| BInfty ⇒ true
end].
Canonical Structure itvPredType := PredType pred_of_itv.
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) × (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) × (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) × (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) × (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) × (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
| BOpen_if b lb ⇒ (lb ≤ x ?< if b) : Prop
| BInfty ⇒ True
end : Prop) ×
(match u with
| BOpen_if b ub ⇒ (x ≤ ub ?< if b) : Prop
| BInfty ⇒ True
end : Prop))%type.
Lemma itv_dec : ∀ (x : R) (i : interval R),
reflect (itv_decompose i x) (x \in i).
Definition le_boundl (b1 b2 : itv_bound R) :=
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 : itv_bound R) :=
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_boundl_refl : reflexive le_boundl.
Hint Resolve le_boundl_refl : core.
Lemma le_boundr_refl : reflexive le_boundr.
Hint Resolve le_boundr_refl : core.
Lemma le_boundl_trans : transitive le_boundl.
Lemma le_boundr_trans : transitive le_boundr.
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 le_boundl_anti b1 b2 : (le_boundl b1 b2 && le_boundl b2 b1) = (b1 == b2).
Lemma le_boundr_anti b1 b2 : (le_boundr b1 b2 && le_boundr b2 b1) = (b1 == b2).
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.
Definition itv_intersection (x y : interval R) : interval R :=
let: Interval x x' := x in
let: Interval y y' := y in
Interval
(if le_boundl x y then y else x)
(if le_boundr x' y' then x' else y').
Definition itv_intersection1i : left_id `]-oo, +oo[ itv_intersection.
Definition itv_intersectioni1 : right_id `]-oo, +oo[ itv_intersection.
Lemma itv_intersectionii : idempotent itv_intersection.
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 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.
Section IntervalOrdered.
Variable R : realDomainType.
Lemma le_boundl_total : total (@le_boundl R).
Lemma le_boundr_total : total (@le_boundr R).
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)].
Lemma itv_intersectionC : commutative (@itv_intersection R).
Lemma itv_intersectionA : associative (@itv_intersection R).
Canonical itv_intersection_monoid :=
Monoid.Law itv_intersectionA (@itv_intersection1i R) (@itv_intersectioni1 R).
Canonical itv_intersection_comoid := Monoid.ComLaw itv_intersectionC.
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) × (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) × (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) × (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) × (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) × (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
| BOpen_if b lb ⇒ (lb ≤ x ?< if b) : Prop
| BInfty ⇒ True
end : Prop) ×
(match u with
| BOpen_if b ub ⇒ (x ≤ ub ?< if b) : Prop
| BInfty ⇒ True
end : Prop))%type.
Lemma itv_dec : ∀ (x : R) (i : interval R),
reflect (itv_decompose i x) (x \in i).
Definition le_boundl (b1 b2 : itv_bound R) :=
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 : itv_bound R) :=
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_boundl_refl : reflexive le_boundl.
Hint Resolve le_boundl_refl : core.
Lemma le_boundr_refl : reflexive le_boundr.
Hint Resolve le_boundr_refl : core.
Lemma le_boundl_trans : transitive le_boundl.
Lemma le_boundr_trans : transitive le_boundr.
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 le_boundl_anti b1 b2 : (le_boundl b1 b2 && le_boundl b2 b1) = (b1 == b2).
Lemma le_boundr_anti b1 b2 : (le_boundr b1 b2 && le_boundr b2 b1) = (b1 == b2).
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.
Definition itv_intersection (x y : interval R) : interval R :=
let: Interval x x' := x in
let: Interval y y' := y in
Interval
(if le_boundl x y then y else x)
(if le_boundr x' y' then x' else y').
Definition itv_intersection1i : left_id `]-oo, +oo[ itv_intersection.
Definition itv_intersectioni1 : right_id `]-oo, +oo[ itv_intersection.
Lemma itv_intersectionii : idempotent itv_intersection.
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 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.
Section IntervalOrdered.
Variable R : realDomainType.
Lemma le_boundl_total : total (@le_boundl R).
Lemma le_boundr_total : total (@le_boundr R).
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)].
Lemma itv_intersectionC : commutative (@itv_intersection R).
Lemma itv_intersectionA : associative (@itv_intersection R).
Canonical itv_intersection_monoid :=
Monoid.Law itv_intersectionA (@itv_intersection1i R) (@itv_intersectioni1 R).
Canonical itv_intersection_comoid := Monoid.ComLaw itv_intersectionC.
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.