Library Interval.Integral.Refine

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/
Copyright (C) 2007-2019, Inria
This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

From Coq Require Import BinPos Reals List.
From Coquelicot Require Import Coquelicot.

Require Import Coquelicot.
Require Import Xreal.
Require Import Interval.
Require Import Priority.

Section IterUntil.

Fixpoint iter_until {T} n (step : T T) (cache_step : T T) (done : T bool) v :=
  match n with
  | xHstep v
  | xO n
    let v := iter_until n step cache_step done v in
    if done v then v else
    let v := cache_step v in
    iter_until n step (fun xx) done v
  | xI n
    let v := step v in
    if done v then v else
    let v := iter_until n step cache_step done v in
    if done v then v else
    let v := cache_step v in
    iter_until n step (fun xx) done v
  end.

Theorem iter_until_correct :
   {T} (P : T Prop) n step slow_step done,
  ( v : T, P v P (step v))
  ( v : T, P v P (slow_step v))
   v : T, P v P (iter_until n step slow_step done v).

End IterUntil.

Definition valid (f : R R) (uf vf : (R Prop) Prop) yi :=
  (yi Inan ex_RInt_gen f uf vf)
  contains yi (Xreal (RInt_gen f uf vf)).

Lemma valid_Inan :
   f uf vf, valid f uf vf Inan.

Module IntegralRefiner (I : IntervalOps).

Module J := IntervalExt I.

Inductive integral_bound := IBu | IBv | IBp (x : I.F.type).

Section Bounds.

Variable uf vf : (R Prop) Prop.
Context (Fuf : ProperFilter' uf) (Fvf : ProperFilter' vf).

Definition convert b :=
  match b with
  | IBuuf
  | IBvvf
  | IBp xat_point (proj_val (I.F.convert x))
  end.

Local Instance filter_convert :
   b, ProperFilter' (convert b).

Definition valid f u v i :=
  valid f (convert u) (convert v) (I.convert i).

Inductive piece :=
  Piece (u v : integral_bound) (i : I.type).

Fixpoint invariant_aux h l (u : integral_bound) :=
  match h with
  | Piece u' v iu = u'
    match l with
    | nilv = IBv
    | h :: t
      match v with IBp _invariant_aux h t v | _False end
    end
  end.

Let exact_sum (f : R R) l :=
  fold_right (fun r sRplus s
    match r with
    | Piece ur vr _RInt_gen f (convert ur) (convert vr)
    end) 0%R l.

Definition invariant (f : R R) (p : ptree piece) :=
  all (fun rmatch r with Piece uf vf ivalid f uf vf i end) (ptree_to_list p)
   qh, qt, permut (ptree_to_list p) (qh :: qt) invariant_aux qh qt IBu.

Definition sum prec (p : ptree piece) :=
  ptree_fold (fun acc vI.add prec acc match v with Piece _ _ ii end) p I.zero.

Theorem sum_invariant :
   prec p f,
  invariant f p
  valid f IBu IBv (sum prec p).

Definition le_piece prec (p q : piece) :=
  match p, q with
  | Piece _ _ pi, Piece _ _ qiI.wider prec pi qi
  end.

Definition split_piece prec midp fi sp :=
  let le_piece := le_piece prec in
  match sp with
  | (s, p)
    match ptree_pop le_piece p with
    | (Piece u v i, h)
      let m := IBp (midp u v) in
      let i1 := fi u m in
      let i2 := fi m v in
      let p1 := Piece u m i1 in
      let p2 := Piece m v i2 in
      let s := I.add prec (I.cancel_add prec s i) (I.add prec i1 i2) in
      let p := ptree_insert le_piece (pheap_insert le_piece h p1) p2 in
      (s, p)
    end
  end.

Theorem split_piece_correct :
   prec midp f fi p,
  ( u v, valid f u v (fi u v))
  invariant f (snd p)
  invariant f (snd (split_piece prec midp fi p)).


Definition bisect prec n midp fi (check : I.type bool) :=
  let i := fi IBu IBv in
  if check i then i
  else
    let p := iter_until n
      (split_piece prec midp fi)
      (fun '(_, p)(sum prec p, p))
      (fun '(p, _)check p)
      (i, PTsome (Piece IBu IBv i) nil) in
    sum prec (snd p).

Theorem bisect_correct :
   prec n midp f fi check,
  ( u v, valid f u v (fi u v))
  valid f IBu IBv (bisect prec n midp fi check).

End Bounds.

Theorem contains_RInt_valid :
   f u v i,
  valid (at_point u) (at_point v) f IBu IBv i
  contains (I.convert i) (Xreal (RInt f u v)).

Theorem valid_at_point :
   f u v fi ui vi,
  contains (I.convert ui) (Xreal u)
  contains (I.convert vi) (Xreal v)
  ( ui' vi' u' v',
    contains (I.convert ui') (Xreal u')
    contains (I.convert vi') (Xreal v')
    (I.convert (fi ui' vi') Inan ex_RInt f u' v')
    contains (I.convert (fi ui' vi')) (Xreal (RInt f u' v')))
   u' v',
  let cb := fun x
    match x with IBuui | IBvvi | IBp xI.singleton x end in
  valid (at_point u) (at_point v) f u' v' (fi (cb u') (cb v')).

Theorem valid_at_mixed :
   f u v (Fv: ProperFilter v) fi1 fi2 ui,
  contains (I.convert ui) (Xreal u)
  ( ui' vi' u' v',
    contains (I.convert ui') (Xreal u')
    contains (I.convert vi') (Xreal v')
    (I.convert (fi1 ui' vi') Inan ex_RInt f u' v')
    contains (I.convert (fi1 ui' vi')) (Xreal (RInt f u' v')))
  ( ui' u',
    contains (I.convert ui') (Xreal u')
    (I.convert (fi2 ui') Inan ex_RInt_gen f (at_point u') v)
    contains (I.convert (fi2 ui')) (Xreal (RInt_gen f (at_point u') v)))
   u' v',
  valid (at_point u) v f u' v'
    (match u', v' with
    | IBu, IBp xufi1 ui (I.singleton xu)
    | IBp xl, IBp xufi1 (I.singleton xl) (I.singleton xu)
    | IBu, IBvfi2 ui
    | IBp xl, IBvfi2 (I.singleton xl)
    | _, _I.nai
    end).

Theorem valid_at_mixed' :
   f u v (Fu: ProperFilter u) fi1 fi2 vi,
  contains (I.convert vi) (Xreal v)
  ( ui' vi' u' v',
    contains (I.convert ui') (Xreal u')
    contains (I.convert vi') (Xreal v')
    (I.convert (fi1 ui' vi') Inan ex_RInt f u' v')
    contains (I.convert (fi1 ui' vi')) (Xreal (RInt f u' v')))
  ( vi' v',
    contains (I.convert vi') (Xreal v')
    (I.convert (fi2 vi') Inan ex_RInt_gen f u (at_point v'))
    contains (I.convert (fi2 vi')) (Xreal (RInt_gen f u (at_point v'))))
   u' v',
  valid u (at_point v) f u' v'
    (match u', v' with
    | IBu, IBp xufi2 (I.singleton xu)
    | IBp xl, IBp xufi1 (I.singleton xl) (I.singleton xu)
    | IBu, IBvfi2 vi
    | IBp xl, IBvfi1 (I.singleton xl) vi
    | _, _I.nai
    end).

End IntegralRefiner.

Lemma RInt_helper :
   f u v i,
  (i Inan I : R, is_RInt f u v I contains i (Xreal I))
  (i Inan ex_RInt f u v) contains i (Xreal (RInt f u v)).

Lemma RInt_gen_helper :
   f u v {Fu : ProperFilter' u} {Fv : ProperFilter' v} i,
  (i Inan I : R, is_RInt_gen f u v I contains i (Xreal I))
  (i Inan ex_RInt_gen f u v) contains i (Xreal (RInt_gen f u v)).