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.