(Joint Center)Library interval

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype.
Require Import bigop ssralg finset fingroup zmodp ssrint ssrnum.

Set Implicit Arguments.

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

Local Notation mid x y := ((x + y) / 2%:R).

Section IntervalPo.

CoInductive itv_bound (T : Type) : Type := BClose of bool & T | BInfty.

CoInductive interval (T : Type) := Interval of itv_bound T & itv_bound T.

Variable (R : numDomainType).

Definition pred_of_itv (i : interval R) : pred R :=
  [pred x | let: Interval l u := i in
      match l with
        | BClose false aa < x
        | BClose _ aa x
        | BInftytrue
      end &&
      match u with
        | BClose false bx < b
        | BClose _ bx b
        | BInftytrue
      end].
Canonical Structure itvPredType := Eval hnf in mkPredType pred_of_itv.

Notation "`[ a , b ]" := (Interval (BClose true a) (BClose true b))
  (at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope.
Notation "`] a , b ]" := (Interval (BClose false a) (BClose true b))
  (at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
Notation "`[ a , b [" := (Interval (BClose true a) (BClose false b))
  (at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope.
Notation "`] a , b [" := (Interval (BClose false a) (BClose false b))
  (at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose true b))
  (at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval (BInfty _) (BClose false b))
  (at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BClose true a) (BInfty _))
  (at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BClose false a) (BInfty _))
  (at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope.
Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _))
  (at level 0, format "`] -oo , '+oo' [") : ring_scope.

Definition itv_rewrite (i : interval R) x : Type :=
  let: Interval l u := i in
    (match l with
       | BClose true a(a x) × (x < a = false)
       | BClose false a(a x) × (a < x) × (x a = false)
       | BInfty x : R, x == x
     end ×
    match u with
       | BClose true b(x b) × (b < x = false)
       | BClose false b(x b) × (x < b) × (b x = false)
       | BInfty x : R, x == x
     end ×
    match l, u with
       | BClose true a, BClose true b
         (a b) × (b < a = false) × (a \in `[a, b]) × (b \in `[a, b])
       | BClose true a, BClose false b
         (a b) × (a < b) × (b a = false)
         × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
       | BClose false a, BClose true b
         (a b) × (a < b) × (b a = false)
         × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
       | BClose false a, BClose false b
         (a b) × (a < b) × (b a = false)
         × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
       | _, _ x : R, x == x
    end)%type.

Definition itv_decompose (i : interval R) x : Prop :=
  let: Interval l u := i in
  ((match l with
    | BClose true a(a x) : Prop
    | BClose _ a(a < x) : Prop
    | BInftyTrue
  end : Prop) ×
  (match u with
    | BClose true b(x b) : Prop
    | BClose _ b(x < b) : Prop
    | BInftyTrue
  end : Prop))%type.

Lemma itv_dec : (x : R) (i : interval R),
  reflect (itv_decompose i x) (x \in i).

Implicit Arguments itv_dec [x i].

Definition ltreif (x y : R) b := if b then x y else x < y.

Local Notation "x < y ?<= 'if' b" := (ltreif x y b)
  (at level 70, y at next level,
  format "x '[hv' < y '/' ?<= 'if' b ']'") : ring_scope.

Lemma ltreifxx : x b, (x < x ?<= if b) = b.

Lemma ltreif_trans : x y z b1 b2,
  x < y ?<= if b1y < z ?<= if b2x < z ?<= if b1 && b2.

Lemma ltreifW : b x y, x < y ?<= if bx y.

Definition le_boundl b1 b2 :=
  match b1, b2 with
    | BClose b1 x1, BClose b2 x2x1 < x2 ?<= if (b2 ==> b1)
    | BClose _ _, BInftyfalse
    | _, _true
  end.

Definition le_boundr b1 b2 :=
  match b1, b2 with
    | BClose b1 x1, BClose b2 x2x1 < x2 ?<= if (b1 ==> b2)
    | BInfty, BClose _ _false
    | _, _true
  end.

Lemma itv_boundlr bl br x :
  x \in Interval bl br = le_boundl bl (BClose true x)
                      && le_boundr (BClose true x) br.

Lemma le_boundr_refl : reflexive le_boundr.

Hint Resolve le_boundr_refl.

Lemma le_boundl_refl : reflexive le_boundl.

Hint Resolve le_boundl_refl.

Lemma le_boundl_bb : x b1 b2, le_boundl (BClose b1 x) (BClose b2 x) = (b2 ==> b1).

Lemma le_boundr_bb : x b1 b2, le_boundr (BClose b1 x) (BClose b2 x) = (b1 ==> b2).

Lemma itv_xx : x bl br,
  Interval (BClose bl x) (BClose br x) =i if bl && br then pred1 x else pred0.

Lemma itv_gte : ba xa bb xb, (if ba && bb then xb < xa else xb xa)
  → Interval (BClose ba xa) (BClose bb xb) =i pred0.

Lemma boundl_in_itv : ba xa b,
  xa \in Interval (BClose ba xa) b = if ba then le_boundr (BClose true xa) b else false.

Lemma boundr_in_itv : bb xb a,
  xb \in Interval a (BClose bb xb) = if bb then le_boundl a (BClose true xb) else false.

Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).

Lemma itvP : (x : R) (i : interval R), (x \in i) → itv_rewrite i x.

Hint Rewrite intP.
Implicit Arguments itvP [x i].

Definition subitv (i1 i2 : interval R) :=
  match i1, i2 with
    | Interval a1 b1, Interval a2 b2le_boundl a2 a1 && le_boundr b1 b2
  end.

Lemma subitvP : (i2 i1 : interval R),
  (subitv i1 i2) → {subset i1 i2}.

Lemma subitvPr : (a b1 b2 : itv_bound R),
  le_boundr b1 b2{subset (Interval a b1) (Interval a b2)}.

Lemma subitvPl : (a1 a2 b : itv_bound R),
  le_boundl a2 a1{subset (Interval a1 b) (Interval a2 b)}.

Lemma ltreif_in_itv : ba bb xa xb x,
  x \in Interval (BClose ba xa) (BClose bb xb) → xa < xb ?<= if ba && bb.

Lemma ltr_in_itv : ba bb xa xb x, ~~ (ba && bb)
  x \in Interval (BClose ba xa) (BClose bb xb) → xa < xb.

Lemma ler_in_itv : ba bb xa xb x,
  x \in Interval (BClose ba xa) (BClose bb xb) → xa xb.

Lemma subinP' : forall (i2 i1 : interval), reflect {subset i1 <= i2} (subint i1 i2). Proof. move=> i2 i1; apply: (iffP idP); first exact: subitvP. move: i1 i2=> [ [#[ ] a1| ] [ [ ] b1| ]#] [ [#[ ] a2| ] [ [ ] b2| ]#] //=.

Lemma mem0_itvcc_xNx : x, (0 \in `[-x, x]) = (0 x).

Lemma mem0_itvoo_xNx : x, 0 \in `](-x), x[ = (0 < x).

Lemma itv_splitI : a b, x,
  x \in Interval a b = (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b).

Lemma ltreifNF : x y b, y < x ?<= if ~~ bx < y ?<= if b = false.

Lemma ltreifS : b x y, x < yx < y ?<= if b.

Lemma ltreifT : x y, x < y ?<= if true = (x y).

Lemma ltreifF : x y, x < y ?<= if false = (x < y).

Lemma real_ltreifN : x y b, x \in Num.realy \in Num.real
  x < y ?<= if ~~b = ~~ (y < x ?<= if b).

Lemma itv_splitU_po xc bc : xc \in Num.real -> forall a b, xc \in Interval a b -> forall y, y \in Interval a b = (y \in Interval a (BClose bc xc)) || (y \in Interval (BClose (~~bc) xc) b). Proof. move=> xc bc [ba xa| ] [bb xb| ] cab y cyc; move: cab;

(Joint Center)case/andP=> hac hcb; case hay: ltreif=> /=; case hyb: ltreif=> //=.

+ by case: bc=> /=; case: cpable3P cyc. + rewrite ltreifN_po ?andbF // ltreifS // cpable_ltrNge 1?cpable_sym //. move/negP:hyb; move/negP; apply: contra. case: bb hcb=> /= hcb hyc; first exact: ler_trans hcb. exact: ler_lt_trans hcb. move/ltreifW:hyb=> hyb; suff: false by [ ]. by rewrite -hay - [ba]andbT (ltreif_trans hac).

(Joint Center)rewrite !andbT; move=> hac; case hay: ltreif=> /=; symmetry.

by case: bc=> /=; case: cpable3P cyc. apply: negbTE; move/negP: hay; move/negP; apply: contra. by move/ltreifW; rewrite - [ba]andbT -ltreifT; move/(ltreif_trans _); apply.

(Joint Center)move=> hcb; case hyb: ltreif=> /=; symmetry; rewrite ?(andbF, orbF).

by case: bc=> /=; case: cpable3P cyc. apply: negbTE; move/negP: hyb; move/negP; apply: contra. by move/ltreifW; rewrite -ltreifT; move/ltreif_trans; apply. by case: bc=> /=; case: cpable3P cyc. Qed.
Lemma itv_splitU2_po : forall x a b, x \in Interval a b -> forall y, Num.cpable y x -> y \in Interval a b = [|| (y \in Interval a (BClose false x)), (y == x) | (y \in Interval (BClose false x) b) ]. Proof. move=> x a b hx y cxy; rewrite (@itv_splitU_po x false) //. case hyx: (_ \in _); rewrite //= (@itv_splitU_po x true) ?itv_xx //=. by rewrite bound_in_itv; move: hx; rewrite itv_boundlr; case/andP. Qed.
Lemma itvUff : forall x y b1 b2 a b, x \in Interval (BClose b2 y) b -> y \in Interval a (BClose b1 x) -> forall z, Num.cpable z x -> Num.cpable z y -> (z \in Interval a (BClose b1 x)) || (z \in Interval (BClose b2 y) b) = (z \in Interval a b). Proof. move=> x y b1 b2 a b /= hx hy z czx czy. rewrite (itv_splitU_po (~~b2) hy) //; rewrite (itv_splitU_po b1 hx) //. rewrite negbK orbA orbC -!orbA orbb orbC; symmetry. rewrite (@itv_splitU_po y (~~b2)) //. by rewrite -orbA; congr orb; rewrite (@itv_splitU_po x b1) ?negbK. apply: subitvP hy=> /=; rewrite le_boundl_refl /=. move: hx; rewrite itv_boundlr; case/andP=> _. rewrite /le_boundr; case: b=> [ [ ] b| ] //=. by rewrite implybT. exact: ltreifS. Qed.

Lemma oppr_itv : ba bb (xa xb x : R),
  (-x \in Interval (BClose ba xa) (BClose bb xb))
= (x \in Interval (BClose bb (-xb)) (BClose ba (-xa))).

Lemma oppr_itvoo : (a b x : R), (-x \in `]a, b[) = (x \in `](-b), (-a)[).

Lemma oppr_itvco : (a b x : R), (-x \in `[a, b[) = (x \in `](-b), (-a)]).

Lemma oppr_itvoc : (a b x : R), (-x \in `]a, b]) = (x \in `[(-b), (-a)[).

Lemma oppr_itvcc : (a b x : R), (-x \in `[a, b]) = (x \in `[(-b), (-a)]).

End IntervalPo.

Notation "`[ a , b ]" := (Interval (BClose true a) (BClose true b))
  (at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope.
Notation "`] a , b ]" := (Interval (BClose false a) (BClose true b))
  (at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
Notation "`[ a , b [" := (Interval (BClose true a) (BClose false b))
  (at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope.
Notation "`] a , b [" := (Interval (BClose false a) (BClose false b))
  (at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose true b))
  (at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval (BInfty _) (BClose false b))
  (at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BClose true a) (BInfty _))
  (at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BClose false a) (BInfty _))
  (at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope.
Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _))
  (at level 0, format "`] -oo , '+oo' [") : ring_scope.

Notation "x < y ?<= 'if' b" := (ltreif x y b)
  (at level 70, y at next level,
  format "x '[hv' < y '/' ?<= 'if' b ']'") : ring_scope.

Section IntervalOrdered.

Variable R : realDomainType.

Lemma ltreifN (x y : R) b : x < y ?<= if ~~b = ~~ (y < x ?<= if b).

Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b
   y, y \in Interval a b =
    (y \in Interval a (BClose bc xc)) || (y \in Interval (BClose (~~bc) xc) b).

Lemma itv_splitU2 (x : R) a b : x \in Interval a b
   y, y \in Interval a b =
    [|| (y \in Interval a (BClose false x)), (y == x)
      | (y \in Interval (BClose false x) b)].

End IntervalOrdered.

Section IntervalField.

Variable R : realFieldType.

Lemma mid_in_itv : ba bb (xa xb : R), xa < xb ?<= if (ba && bb)
  → mid xa xb \in Interval (BClose ba xa) (BClose bb xb).

Lemma mid_in_itvoo : (xa xb : R), xa < xbmid xa xb \in `]xa, xb[.

Lemma mid_in_itvcc : (xa xb : R), xa xbmid xa xb \in `[xa, xb].

End IntervalField.