From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Export set_interval.
From HB Require Import structures.
Require Import reals ereal signed topology normedtype sequences.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

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.

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

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

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

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.

Section itv_realDomainType .
Context ( R : realDomainType).

Lemma le_bnd_ereal ( a b : itv_bound R) : (a <= b)%O -> (a <= b)%E.

Lemma lt_ereal_bnd ( a b : itv_bound R) : (a < b)%E -> (a < b)%O.

Lemma Interval_ereal_mem ( r : R) ( a b : itv_bound R) :
  r \in Interval a b -> (a <= r%:E <= b)%E.

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

Lemma itv_cyy : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R).

Lemma itv_oyy : `]+oo%E, +oo[%classic = set0 :> set (\bar R).

Lemma itv_cNyy : `[-oo%E, +oo[%classic = setT :> set (\bar R).

Lemma itv_oNyy : `]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R).

End itv_realDomainType.

Section set_ereal .
Context ( R : realType) T ( f g : T -> \bar R).
Local Open Scope ereal_scope.

Let E j := [set x | f x - g x >= j.+1%:R^-1%:E].

Lemma set_lte_bigcup : [set x | f x > g x] = \bigcup_j E j.

End set_ereal.

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

Lemma set1_bigcap_oc ( R : realType) ( r : R) :
  [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic.

Lemma itv_bnd_open_bigcup ( R : realType) b ( r s : R) :
  [set` Interval (BSide b r) (BLeft s)] =
  \bigcup_n [set` Interval (BSide b r) (BRight (s - n.+1%:R^-1))].

Lemma itv_open_bnd_bigcup ( R : realType) b ( r s : R) :
  [set` Interval (BRight s) (BSide b r)] =
  \bigcup_n [set` Interval (BLeft (s + n.+1%:R^-1)) (BSide b r)].

Lemma itv_bnd_infty_bigcup ( R : realType) b ( x : R) :
  [set` Interval (BSide b x) +oo%O] =
  \bigcup_i [set` Interval (BSide b x) (BRight (x + i%:R))].

Lemma itv_infty_bnd_bigcup ( R : realType) b ( x : R) :
  [set` Interval -oo%O (BSide b x)] =
  \bigcup_i [set` Interval (BLeft (x - i%:R)) (BSide b x)].

Lemma bigcup_itvT {R : realType} b :
  \bigcup_i [set` Interval (BSide b (- i%:R)) (BRight i%:R)] = [set: R].