Library set_interval

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
Require Import mathcomp_extra boolp classical_sets functions.
From HB Require Import structures.

This files contains lemmas about sets and intervals.
neitv i == the interval i is non-empty when the support type is a numFieldType, this is equivalent to (i.1 < i.2)%O (lemma neitvE) set_itv_infty_set0 == multirule to simplify empty intervals conv, ndconv == convexity operator factor a b x := (x - a) / (b - a) set_itvE == multirule to turn intervals into inequalities disjoint_itv i j == intervals i and j are disjoint

Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

definitions and lemmas to make a bridge between MathComp intervals and classical sets
Section set_itv_porderType.
Variables (d : unit) (T : porderType d).
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).

Definition neitv i := [set` i] != set0.

Lemma neitv_lt_bnd i : neitv i → (i.1 < i.2)%O.

Lemma set_itvP i j : [set` i] = [set` j] :> set _i =i j.

Lemma subset_itvP i j : {subset ij} ↔ [set` i] `<=` [set` j].

Lemma set_itvoo x y : `]x, y[%classic = [set z | (x < z < y)%O].

Lemma set_itvco x y : `[x, y[%classic = [set z | (xz < y)%O].

Lemma set_itvcc x y : `[x, y]%classic = [set z | (xzy)%O].

Lemma set_itvoc x y : `]x, y]%classic = [set z | (x < zy)%O].

Lemma set_itv1 x : `[x, x]%classic = [set x].

Lemma set_itvoo0 x : `]x, x[%classic = set0.

Lemma set_itvoc0 x : `]x, x]%classic = set0.

Lemma set_itvco0 x : `[x, x[%classic = set0.

Lemma set_itv_infty_infty : `]-oo, +oo[%classic = @setT T.

Lemma set_itv_o_infty x : `]x, +oo[%classic = [set z | (x < z)%O].

Lemma set_itv_c_infty x : `[x, +oo[%classic = [set z | (xz)%O].

Lemma set_itv_infty_o x : `]-oo, x[%classic = [set z | (z < x)%O].

Lemma set_itv_infty_c x : `]-oo, x]%classic = [set z | (zx)%O].

Lemma set_itv_pinfty_bnd a : [set` Interval +oo%O a] = set0.

Lemma set_itv_bnd_ninfty a : [set` Interval a -oo%O] = set0.

Definition set_itv_infty_set0 := (set_itv_bnd_ninfty, set_itv_pinfty_bnd).

Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo,
  set_itvcc, set_itvoc, set_itvco, set_itv_infty_infty, set_itv_o_infty,
  set_itv_c_infty, set_itv_infty_o, set_itv_infty_c, set_itv_infty_set0).

Lemma setUitv1 (a : itv_bound T) (x : T) : (aBLeft x)%O
  [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].

Lemma setU1itv (a : itv_bound T) (x : T) : (BRight xa)%O
  x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a].

End set_itv_porderType.
Arguments neitv {d T} _.

Lemma set_itv_ge [disp : unit] [T : porderType disp] [b1 b2 : itv_bound T] :
  ~~ (b1 < b2)%O → [set` Interval b1 b2] = set0.

Section set_itv_latticeType.
Variables (d : unit) (T : latticeType d).
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).

Lemma set_itvI i j : [set` (i `&` j)%O] = [set` i] `&` [set` j].

End set_itv_latticeType.

Section set_itv_numFieldType.
Variable R : numFieldType.
Implicit Types i : interval R.

Lemma neitvE i : neitv i = (i.1 < i.2)%O.

Lemma neitvP i : reflect (i.1 < i.2)%O (neitv i).

End set_itv_numFieldType.

Lemma setitv0 (R : realDomainType) : [set` (0%O : interval R)] = set0.

Section interval_has_bound.
Variable R : numDomainType.

Lemma has_lbound_itv (x : R) b (a : itv_bound R) :
  has_lbound [set` Interval (BSide b x) a].

Lemma has_ubound_itv (x : R) b (a : itv_bound R) :
  has_ubound [set` Interval a (BSide b x)].

End interval_has_bound.

Section subr_image.
Variable R : numDomainType.
Implicit Types E : set R.
Implicit Types x : R.

Lemma setNK : involutive (fun E ⇒ -%R @` E).

Lemma lb_ubN E x : lbound E xubound (-%R @` E) (- x).

Lemma ub_lbN E x : ubound E xlbound (-%R @` E) (- x).

Lemma memNE E x : E x = (-%R @` E) (- x).

Lemma nonemptyN E : nonempty (-%R @` E) ↔ nonempty E.

Lemma opp_set_eq0 E : (-%R @` E) = set0E = set0.

Lemma has_lb_ubN E : has_lbound Ehas_ubound (-%R @` E).

End subr_image.

Section interval_hasNbound.
Variable R : realDomainType.
Implicit Types E : set R.
Implicit Types x : R.

Lemma has_ubPn {E} : ¬ has_ubound E ↔ ( x, exists2 y, E y & x < y).

Lemma has_lbPn E : ¬ has_lbound E ↔ ( x, exists2 y, E y & y < x).

Lemma hasNlbound_itv (a : itv_bound R) : a != -oo%O
  ¬ has_lbound [set` Interval -oo%O a].

Lemma hasNubound_itv (a : itv_bound R) : a != +oo%O
  ¬ has_ubound [set` Interval a +oo%O].

End interval_hasNbound.

#[global] Hint Extern 0 (has_lbound _) ⇒ solve[apply: has_lbound_itv] : core.
#[global] Hint Extern 0 (has_ubound _) ⇒ solve[apply: has_ubound_itv] : core.
#[global]
Hint Extern 0 (~ has_lbound _) ⇒ solve[by apply: hasNlbound_itv] : core.
#[global]
Hint Extern 0 (~ has_ubound _) ⇒ solve[by apply: hasNubound_itv] : core.

Lemma opp_itv_bnd_infty (R : numDomainType) (x : R) b :
  -%R @` [set` Interval (BSide b x) +oo%O] =
  [set` Interval -oo%O (BSide (negb b) (- x))].

Lemma opp_itv_infty_bnd (R : numDomainType) (x : R) b :
  -%R @` [set` Interval -oo%O (BSide b x)] =
  [set` Interval (BSide (negb b) (- x)) +oo%O].

Lemma opp_itv_bnd_bnd (R : numDomainType) a b (x y : R) :
  -%R @` [set` Interval (BSide a x) (BSide b y)] =
  [set` Interval (BSide (~~ b) (- y)) (BSide (~~ a) (- x))].

Lemma opp_itvoo (R : numDomainType) (x y : R) :
  -%R @` `]x, y[%classic = `](- y), (- x)[%classic.

lemmas between itv and set-theoretic operations
Section set_itv_porderType.
Variables (d : unit) (T : orderType d).
Implicit Types (a : itv_bound T) (x y : T) (i j : interval T) (b : bool).

Lemma setCitvl a : ~` [set` Interval -oo%O a] = [set` Interval a +oo%O].

Lemma setCitvr a : ~` [set` Interval a +oo%O] = [set` Interval -oo%O a].

Lemma set_itv_splitI i : [set` i] = [set` Interval i.1 +oo%O] `&` [set` Interval -oo%O i.2].

Lemma setCitv i :
  ~` [set` i] = [set` Interval -oo%O i.1] `|` [set` Interval i.2 +oo%O].

Lemma set_itv_splitD i :
  [set` i] = [set` Interval i.1 +oo%O] `\` [set` Interval i.2 +oo%O].

End set_itv_porderType.

Section conv_factor_numDomainType.
Variable R : numDomainType.
Implicit Types (a b t r : R) (A : set R).

Lemma mem_1B_itvcc t : (1 - t \in `[0, 1]) = (t \in `[0, 1]).

Definition conv a b t : R := (1 - t) × a + t × b.

Lemma conv_id : conv 0 1 = id.

Lemma convEl a b t : conv a b t = t × (b - a) + a.

Lemma convEr a b t : conv a b t = (1 - t) × (a - b) + b.

Lemma conv10 t : conv 1 0 t = 1 - t.

Lemma conv0 a b : conv a b 0 = a.

Lemma conv1 a b : conv a b 1 = b.

Lemma conv_sym a b t : conv a b t = conv b a (1 - t).

Lemma conv_flat a : conv a a = cst a.

Lemma leW_conv a b : ab → {homo conv a b : x y / xy}.

Definition factor a b x := (x - a) / (b - a).

Lemma leW_factor a b : ab → {homo factor a b : x y / xy}.

Lemma factor_flat a : factor a a = cst 0.

Lemma factorl a b : factor a b a = 0.

Definition ndconv a b of a < b := conv a b.

Lemma ndconvE a b (ab : a < b) : ndconv ab = conv a b.

End conv_factor_numDomainType.

Section conv_factor_numFieldType.
Variable R : numFieldType.
Implicit Types (a b t r : R) (A : set R).

Lemma factorr a b : a != bfactor a b b = 1.

Lemma factorK a b : a != bcancel (factor a b) (conv a b).

Lemma convK a b : a != bcancel (conv a b) (factor a b).

Lemma conv_inj a b : a != binjective (conv a b).

Lemma factor_inj a b : a != binjective (factor a b).

Lemma conv_bij a b : a != bbijective (conv a b).

Lemma factor_bij a b : a != bbijective (factor a b).

Lemma le_conv a b : a < b → {mono conv a b : x y / xy}.

Lemma le_factor a b : a < b → {mono factor a b : x y / xy}.

Lemma lt_conv a b : a < b → {mono conv a b : x y / x < y}.

Lemma lt_factor a b : a < b → {mono factor a b : x y / x < y}.

Let ltNeq a b : a < ba != b.


Lemma conv_itv_bij ba bb a b : a < b
  set_bij [set` Interval (BSide ba 0) (BSide bb 1)]
          [set` Interval (BSide ba a) (BSide bb b)] (conv a b).

Lemma factor_itv_bij ba bb a b : a < b
  set_bij [set` Interval (BSide ba a) (BSide bb b)]
          [set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).

Lemma mem_conv_itv ba bb a b : a < b
  set_fun [set` Interval (BSide ba 0) (BSide bb 1)]
          [set` Interval (BSide ba a) (BSide bb b)] (conv a b).

Lemma mem_conv_itvcc a b : abset_fun `[0, 1] `[a, b] (conv a b).

Lemma range_conv ba bb a b : a < b
   conv a b @` [set` Interval (BSide ba 0) (BSide bb 1)] =
               [set` Interval (BSide ba a) (BSide bb b)].

Lemma range_factor ba bb a b : a < b
   factor a b @` [set` Interval (BSide ba a) (BSide bb b)] =
                 [set` Interval (BSide ba 0) (BSide bb 1)].

End conv_factor_numFieldType.

Lemma mem_factor_itv (R : realFieldType) ba bb (a b : R) :
  set_fun [set` Interval (BSide ba a) (BSide bb b)]
          [set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).

Lemma neitv_bnd1 (R : numFieldType) (s : seq (interval R)) :
  all neitv s i, i \in si.1 != +oo%O.

Lemma neitv_bnd2 (R : numFieldType) (s : seq (interval R)) :
  all neitv s i, i \in si.2 != -oo%O.

Lemma trivIset_set_itv_nth (R : numDomainType) def (s : seq (interval R))
  (D : set nat) : [set` def] = set0
  trivIset D (fun i ⇒ [set` nth def s i]) ↔
    trivIset D (fun inth set0 [seq [set` j] | j <- s] i).
Arguments trivIset_set_itv_nth {R} _ {s}.

Section disjoint_itv.
Context {R : numDomainType}.

Definition disjoint_itv : rel (interval R) :=
  fun a b ⇒ [disjoint [set` a] & [set` b]].

Lemma disjoint_itvxx (i : interval R) : neitv i → ~~ disjoint_itv i i.

Lemma lt_disjoint (i j : interval R) :
  ( x y, x \in iy \in jx < y) → disjoint_itv i j.

End disjoint_itv.

Lemma disjoint_neitv {R : realFieldType} (i j : interval R) :
  disjoint_itv i j ↔ ~~ neitv (itv_meet i j).