# Interval Domain

Require Import base ord tower.llat.
Require Import mathcomp.algebra.all_algebra.

Section IntervalDomain.
Import GRing.Theory.
Import Num.Theory.
Local Open Scope ring_scope.

Structure interval := mk_interval
{ lower_interval : rat -> Prop
; upper_interval : rat -> Prop
; lower_lset :
forall p q, p <= q -> lower_interval q -> lower_interval p
; upper_uset :
forall p q, p <= q -> upper_interval p -> upper_interval q
; lower_uopen :
forall p, lower_interval p -> exists2 q, p < q & lower_interval q
; upper_lopen :
forall q, upper_interval q -> exists2 p, p < q & upper_interval p
; interval_lower_lt_upper :
forall p q, lower_interval p -> upper_interval q -> p < q
}.

Implicit Types (x y z : interval).
Local Notation "x ^+" := (upper_interval x).
Local Notation "x ^-" := (lower_interval x).

Lemma interval_eq x y :
x^- = y^- -> x^+ = y^+ -> x = y.
Proof.
destruct x, y => /=E1 E2. destruct E1, E2. f_equal; exact: pi.
Qed.

Definition interval_le x y := (x^- y^-) /\ (y^+ x^+).

Lemma interval_le_refl x : interval_le x x.
Proof. by split. Qed.

Lemma interval_le_trans : transitive interval_le.
Proof. move=> x y z [l1 l2] [r1 r2]. split. by rewrite l1. by rewrite -l2. Qed.

Canonical interval_proMixin := ProMixin interval_le_refl interval_le_trans.
Canonical interval_proType := Eval hnf in ProType interval interval_proMixin.

Lemma interval_le_eq x y : x y -> y x -> x = y.
Proof. move=> -[l1 l2] [r1 r2]. apply: interval_eq; exact: le_eq. Qed.

Canonical interval_ordMixin := OrdMixin interval_le_eq.
Canonical interval_ordType := Eval hnf in OrdType interval interval_ordMixin.

Definition interior (P : rat -> Prop) (p : rat) : Prop :=
exists2 q, p < q & P q.

Program Definition interval_inf I (F : I -> interval) : interval :=
{| lower_interval := interior (fun q => forall i, (F i)^- q)
; upper_interval := fun q => exists i, (F i)^+ q
|}.
Next Obligation.
case: H0 => r lt_q_r H1. exists r => //. exact: ler_lt_trans lt_q_r.
Qed.
Next Obligation.
exists H0. exact: upper_uset H _.
Qed.
Next Obligation.
case: H => q lt_p_q h. exists ((p + q) / 2%:Q).
by rewrite ltr_pdivl_mulr // mulrDr mulr1 ltr_add2l.
exists q. by rewrite ltr_pdivr_mulr // mulrDr mulr1 ltr_add2r.
exact: h.
Qed.
Next Obligation.
case/upper_lopen: H0 => p lt_p_q h. exists p => //. by exists H.
Qed.
Next Obligation.
case: H => r lt_q_r /(_ H0) HH. apply: interval_lower_lt_upper H1.
apply: lower_lset HH. exact: ltrW.
Qed.

Lemma interval_inf_axiom I (F : I -> interval) :
is_glb F (interval_inf F).
Proof.
apply: mk_glb.
- move=> i. split=> /=.
+ hnf=> q. case=> r lt_q_r h. apply: lower_lset (h i). exact: ltrW.
+ hnf=> p h. exists i. exact: h.
- move=> /= x lbx. split=> /=.
+ move=> p px. case/lower_uopen: px => q lt_p_q xq.
exists q => // i. case: (lbx i) => L _. exact: L.
+ move=> p [i fp]. case: (lbx i) => _ R. exact: R.
Qed.

Canonical interval_clatMixin := CLatMixin interval_inf_axiom.
Canonical interval_clat := Eval hnf in CLat interval interval_clatMixin.

Definition interval_lt x y := exists2 r, x^+ r & y^- r.

Lemma interval_lt_left x y z :
interval_lt x y -> (y z) -> interval_lt x z.
Proof.
move=> -[r h1 h2] [l1 l2]. exists r => //. exact: l1.
Qed.

Lemma interval_lt_right x y z :
(x y) -> interval_lt y z -> interval_lt x z.
Proof.
move=> [l1 l2] [r h1 h2]. exists r => //. exact: l2.
Qed.

Lemma interval_lt_inf I (F : I -> interval) x :
interval_lt (inf F) x -> exists i, interval_lt (F i) x.
Proof.
case=> r /= [i h1] h2. exists i. by exists r.
Qed.

Canonical interval_llatMixin := LLatMixin interval_lt_left interval_lt_right interval_lt_inf.
Canonical interval_llat := Eval hnf in LLat interval interval_llatMixin.
End IntervalDomain.