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/

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
  | xH ⇒ step 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 x ⇒ x) 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 x ⇒ x) 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
  | IBu ⇒ uf
  | IBv ⇒ vf
  | IBp x ⇒ at_point (proj_val (I.F.convert x))
  end.

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 i ⇒ u = u' ∧
    match l with
    | nil ⇒ v = 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 s ⇒ Rplus 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 r ⇒ match r with Piece uf vf i ⇒ valid 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 v ⇒ I.add prec acc match v with Piece _ _ i ⇒ i 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 _ _ qi ⇒ I.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 IBu ⇒ ui | IBv ⇒ vi | IBp x ⇒ I.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 xu ⇒ fi1 ui (I.singleton xu)
    | IBp xl, IBp xu ⇒ fi1 (I.singleton xl) (I.singleton xu)
    | IBu, IBv ⇒ fi2 ui
    | IBp xl, IBv ⇒ fi2 (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 xu ⇒ fi2 (I.singleton xu)
    | IBp xl, IBp xu ⇒ fi1 (I.singleton xl) (I.singleton xu)
    | IBu, IBv ⇒ fi2 vi
    | IBp xl, IBv ⇒ fi1 (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)).