(Joint Center)Library MathComp.interval

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype.
Require Import bigop ssralg finset fingroup zmodp ssrint ssrnum.

This file provide support for intervals in numerical and real domains. The datatype (interval R) gives a formal characterization of an interval, as the pair of its right and left bounds. interval R == the type of formal intervals on R. x \in i == when i is a formal interval on a numeric domain, \in can be used to test membership. itvP x_in_i == where x_in_i has type x \in i, if i is ground, gives a set of rewrite rules that x_in_i imply. x <= y ?< if c == x is smaller than y, and strictly if c is true
We provide a set of notations to write intervals (see below) ` [a, b], ` ]a, b], ..., ` ]-oo, a], ..., ` ]-oo, +oo[ We also provide the lemma subitvP which computes the inequalities one needs to prove when trying to prove the inclusion of intervals.
Remark that we cannot implement a boolean comparison test for intervals on an arbitrary numeric domains, for this problem might be undecidable. Note also that type (interval R) may contain several inhabitants coding for the same interval. However, this pathological issues do nor arise when R is a real domain: we could provide a specific theory for this important case.
See also "Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination", LMCS journal, 2012 by Cyril Cohen and Assia Mahboubi
And "Formalized algebraic numbers: construction and first-order theory" Cyril Cohen, PhD, 2012, section 4.3.

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 := BOpen_if of bool & T | BInfty.
Notation BOpen := (BOpen_if true).
Notation BClose := (BOpen_if false).
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
        | BOpen aa < x
        | BClose aa x
        | BInftytrue
      end &&
      match u with
        | BOpen bx < b
        | BClose bx b
        | BInftytrue
      end].
Canonical Structure itvPredType := Eval hnf in mkPredType pred_of_itv.

We provide the 9 following notations to help writing formal intervals
Notation "`[ a , b ]" := (Interval (BClose a) (BClose b))
  (at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope.
Notation "`] a , b ]" := (Interval (BOpen a) (BClose b))
  (at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
Notation "`[ a , b [" := (Interval (BClose a) (BOpen b))
  (at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope.
Notation "`] a , b [" := (Interval (BOpen a) (BOpen b))
  (at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b))
  (at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b))
  (at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _))
  (at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BOpen 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.

we compute a set of rewrite rules associated to an interval
Definition itv_rewrite (i : interval R) x : Type :=
  let: Interval l u := i in
    (match l with
       | BClose a(a x) × (x < a = false)
       | BOpen a(a x) × (a < x) × (x a = false)
       | BInfty x : R, x == x
     end ×
    match u with
       | BClose b(x b) × (b < x = false)
       | BOpen b(x b) × (x < b) × (b x = false)
       | BInfty x : R, x == x
     end ×
    match l, u with
       | BClose a, BClose b
         (a b) × (b < a = false) × (a \in `[a, b]) × (b \in `[a, b])
       | BClose a, BOpen b
         (a b) × (a < b) × (b a = false)
         × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
       | BOpen a, BClose b
         (a b) × (a < b) × (b a = false)
         × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
       | BOpen a, BOpen 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 a(a x) : Prop
    | BOpen a(a < x) : Prop
    | BInftyTrue
  end : Prop) ×
  (match u with
    | BClose b(x b) : Prop
    | BOpen 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 lersif (x y : R) b := if b then x < y else x y.

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

Lemma lersifxx x b: (x x ?< if b) = ~~ b.

Lemma lersif_trans x y z b1 b2 :
  x y ?< if b1y z ?< if b2x z ?< if b1 || b2.

Lemma lersifW b x y : x y ?< if bx y.

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

Lemma lersifS x y b : x < yx y ?< if b.

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

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

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

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

Lemma itv_boundlr bl br x :
  (x \in Interval bl br) =
  (le_boundl bl (BClose x)) && (le_boundr (BClose 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 (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).

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

Lemma itv_xx x bl br :
  Interval (BOpen_if bl x) (BOpen_if br x) =i
  if ~~ (bl || br) then pred1 x else pred0.

Lemma itv_gte ba xa bb xb : xb xa ?< if ~~ (ba || bb)
  → Interval (BOpen_if ba xa) (BOpen_if bb xb) =i pred0.

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

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

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 lersif_in_itv : ba bb xa xb x,
  x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) →
        xa xb ?< if ba || bb.

Lemma ltr_in_itv : ba bb xa xb x, ba || bb
  x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) → xa < xb.

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

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 real_lersifN x y b : x \in Num.realy \in Num.real
  x y ?< if ~~b = ~~ (y x ?< if b).

Lemma oppr_itv ba bb (xa xb x : R) :
  (-x \in Interval (BOpen_if ba xa) (BOpen_if bb xb)) =
  (x \in Interval (BOpen_if bb (-xb)) (BOpen_if 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 BOpen := (BOpen_if true).
Notation BClose := (BOpen_if false).
Notation "`[ a , b ]" := (Interval (BClose a) (BClose b))
  (at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope.
Notation "`] a , b ]" := (Interval (BOpen a) (BClose b))
  (at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
Notation "`[ a , b [" := (Interval (BClose a) (BOpen b))
  (at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope.
Notation "`] a , b [" := (Interval (BOpen a) (BOpen b))
  (at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b))
  (at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b))
  (at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _))
  (at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
Notation "`] a , '+oo' [" := (Interval (BOpen 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" := (lersif x y b)
  (at level 70, y at next level,
  format "x '[hv' <= y '/' ?< 'if' b ']'") : ring_scope.

Section IntervalOrdered.

Variable R : realDomainType.

Lemma lersifN (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 (BOpen_if (~~ bc) xc))
    || (y \in Interval (BOpen_if 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 (BOpen x)), (y == x)
      | (y \in Interval (BOpen 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 (BOpen_if ba xa) (BOpen_if 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.