Library mathcomp.analysis.set_interval

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
Require Import boolp reals ereal classical_sets signed topology.
Require Import mathcomp_extra functions normedtype.
From HB Require Import structures.
Require Import sequences.

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

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 i ≤ j} ↔ [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 | (x ≤ z < y)%O].

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

Lemma set_itvoc x y : `]x, y]%classic = [set z | (x < z ≤ y)%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 | (x ≤ z)%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 | (z ≤ x)%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) : (a ≤ BLeft x)%O →
  [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].

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

End set_itv_porderType.
Arguments neitv {d T} _.

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 interval_hasNbound.
Variable R : realDomainType.

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.

Section interval_has.
Variable R : realType.
Implicit Types x : R.

Lemma has_sup_half x b (i : itv_bound R) : (i < BSide b x)%O →
  has_sup [set` Interval i (BSide b x)].

Lemma has_inf_half x b (i : itv_bound R) : (BSide b x < i)%O →
  has_inf [set` Interval (BSide b x) i].

End interval_has.

#[global]
Hint Extern 0 (has_sup _) ⇒ solve[apply: has_sup1 | exact: has_sup_half] : core.
#[global]
Hint Extern 0 (has_inf _) ⇒ solve[apply: has_inf1 | exact: has_inf_half]: 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))].

Section interval_sup_inf.
Variable R : realType.
Implicit Types x y : R.

Let sup_itv_infty_bnd x b : sup [set` Interval -oo%O (BSide b x)] = x.

Let inf_itv_bnd_infty x b : inf [set` Interval (BSide b x) +oo%O] = x.

Let sup_itv_o_bnd x y b : x < y →
  sup [set` Interval (BRight x) (BSide b y)] = y.

Let sup_itv_bounded x y a b : (BSide a x < BSide b y)%O →
  sup [set` Interval (BSide a x) (BSide b y)] = y.

Let inf_itv_bnd_o x y b : (BSide b x < BLeft y)%O →
  inf [set` Interval (BSide b x) (BLeft y)] = x.

Let inf_itv_bounded x y a b : (BSide a x < BSide b y)%O →
  inf [set` Interval (BSide a x) (BSide b y)] = x.

Lemma sup_itv a b x : (a < BSide b x)%O →
  sup [set` Interval a (BSide b x)] = x.

Lemma inf_itv a b x : (BSide b x < a)%O →
  inf [set` Interval (BSide b x) a] = x.

Lemma sup_itvcc x y : x ≤ y → sup `[x, y] = y.

Lemma inf_itvcc x y : x ≤ y → inf `[x, y] = x.

End interval_sup_inf.

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 set_itv_realType.
Variable R : realType.
Implicit Types x : R.

Lemma set_itvK : {in neitv, cancel pred_set (@Rhull R)}.

Lemma RhullT : Rhull setT = `]-oo, +oo[%R :> interval R.

Lemma RhullK : {in (@is_interval _ : set (set R)), cancel (@Rhull R) pred_set}.

Lemma itv_c_inftyEbigcap x :
  `[x, +oo[%classic = \bigcap_k `]x - k.+1%:R^-1, +oo[%classic.

Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] =
  \bigcup_k [set` Interval (BSide b x) (BLeft k%:R)].

Lemma itv_o_inftyEbigcup x :
  `]x, +oo[%classic = \bigcup_k `[x + k.+1%:R^-1, +oo[%classic.

Lemma set_itv_setT (i : interval R) : [set` i] = setT → i = `]-oo, +oo[.

End set_itv_realType.

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

Section conv_Rhull.
Variable R : realType.
Implicit Types (a b t r : R) (A : set R).

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

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

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 factorl a b : factor a b a = 0.

Lemma factorr a b : a != b → factor a b b = 1.

Lemma factor_flat a : factor a a = cst 0.

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

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

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

Lemma conv_inj a b : a != b → injective (conv a b).

Lemma factor_inj a b : a != b → injective (factor a b).

Lemma conv_bij a b : a != b → bijective (conv a b).

Lemma factor_bij a b : a != b → bijective (factor a b).

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

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

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

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

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}.

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

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

Let ltNeq a b : a < b → a != 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_factor_itv ba bb a b :
  set_fun [set` Interval (BSide ba a) (BSide bb b)]
          [set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).

Lemma mem_conv_itvcc a b : a ≤ b → set_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)].

Lemma Rhull_smallest A : [set` Rhull A] = smallest (@is_interval R) A.

Lemma le_Rhull : {homo (@Rhull R) : A B / (A `<=` B) >-> {subset A ≤ B}}.

Lemma neitv_Rhull A : ~~ neitv (Rhull A) → A = set0.

Lemma Rhull_involutive A : Rhull [set` Rhull A] = Rhull A.

End conv_Rhull.

Coercion ereal_of_itv_bound T (b : itv_bound T) : \bar T :=
  match b with BSide _ y ⇒ y%:E | +oo%O ⇒ +oo%E | -oo%O ⇒ -oo%E end.
Arguments ereal_of_itv_bound T !b.

Lemma le_bnd_ereal (R : realDomainType) (a b : itv_bound R) :
  (a ≤ b)%O → (a ≤ b)%E.

Lemma lt_ereal_bnd (R : realDomainType) (a b : itv_bound R) :
  (a < b)%E → (a < b)%O.

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

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

Lemma Interval_ereal_mem (R : realDomainType) (r : R) (a b : itv_bound R) :
  r \in Interval a b → (a ≤ r%:E ≤ b)%E.

Lemma ereal_mem_Interval (R : realDomainType) (r : R) (a b : itv_bound R) :
  (a < r%:E < b)%E → r \in Interval a b.

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 i ⇒ nth 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 i → y \in j → x < 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).

Lemma disj_itv_Rhull {R : realType} (A B : set R) : A `&` B = set0 →
  is_interval A → is_interval B → disjoint_itv (Rhull A) (Rhull B).