Library Interval.Tactics.Integral_helper

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-2021, 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 Reals List ZArith Psatz.
From Flocq Require Import Zaux.
From Coquelicot Require Import Coquelicot.

Require Import Stdlib.
Require Import Coquelicot.
Require Import Xreal.
Require Import Basic.
Require Import Sig.
Require Import Interval.
Require Import Integral.
Require Import Eval.
Require Import Bertrand.
Require Import Tree.
Require Import Prog.
Require Import Reify.
Require Import Refine.
Require Import Interval_helper.

Definition reify_var : R.

Ltac get_RInt_vars y i f :=
  let fapp := eval cbv beta in (f reify_var) in
  let vars := constr:(reify_var :: @nil R) in
  let vars := match get_vars fapp vars with reify_var :: ?vars ⇒ vars end in
  let vars := constr:(i :: vars) in
  let vars := match get_vars y vars with i :: ?vars ⇒ vars end in
  vars.

Ltac reify_RInt y f u v :=
  let i := constr:(RInt f u v) in
  let vars := get_RInt_vars y i f in
  let vars := get_vars u vars in
  let vars := get_vars v vars in
  reify_partial y (i :: vars) ;
  intros <- ;
  erewrite <- RInt_ext by (
    let t := fresh "t" in
    intros t _ ; hide_lhs ;
    let fapp := eval cbv beta in (f t) in
    reify_partial fapp (t :: vars) ;
    exact (fun H ⇒ H)) ;
  reify_partial u vars ;
  intros <- ;
  reify_partial v vars ;
  intros <- ;
  find_hyps vars.

Ltac reify_RInt_gen_infty y fm u :=
  let i := constr:(RInt_gen fm (at_point u) (Rbar_locally p_infty)) in
  let f :=
    lazymatch fm with
    | (fun x ⇒ @?f x × _)%R ⇒ f
    | (fun x ⇒ @?f x / _)%R ⇒ f
    | (fun x ⇒ @?f x × / _)%R ⇒ f
    | _ ⇒ fail "Unsupported integrand"
    end in
  let vars := get_RInt_vars y i f in
  let vars := get_vars u vars in
  reify_partial y (i :: vars) ;
  intros <- ;
  erewrite <- RInt_gen_ext_eq by (
    let t := fresh "t" in
    intros t ; hide_lhs ;
    apply (f_equal (fun x ⇒ Rmult x _)) ;
    let fapp := eval cbv beta in (f t) in
    reify_partial fapp (t :: vars) ;
    exact (fun H ⇒ H)) ;
  reify_partial u vars ;
  intros <- ;
  find_hyps vars.

Ltac reify_RInt_gen_zero y fm v :=
  let i := constr:(RInt_gen fm (at_right 0) (at_point v)) in
  let f :=
    lazymatch fm with
    | (fun x ⇒ @?f x × _)%R ⇒ f
    | (fun x ⇒ @?f x / _)%R ⇒ f
    | (fun x ⇒ @?f x × / _)%R ⇒ f
    | _ ⇒ fail "Unsupported integrand"
    end in
  let vars := get_RInt_vars y i f in
  let vars := get_vars v vars in
  reify_partial y (i :: vars) ;
  intros <- ;
  erewrite <- RInt_gen_ext_eq by (
    let t := fresh "t" in
    intros t ; hide_lhs ;
    apply (f_equal (fun x ⇒ Rmult x _)) ;
    let fapp := eval cbv beta in (f t) in
    reify_partial fapp (t :: vars) ;
    exact (fun H ⇒ H)) ;
  reify_partial v vars ;
  intros <- ;
  find_hyps vars.

Module IntegralTacticAux (F : FloatOps with Definition sensible_format := true) (I : IntervalOps with Module F := F).

Module F' := FloatExt F.
Module IH := IntervalTacticAux I.
Import IH.

Module BI := BertrandInterval I.
Module IR := IntegralRefiner I.
Module IT := IntegralTaylor I.
Module IU := IntegralTactic I.

Definition eval_RInt_init prec deg hyps pf pu pv cf cu cv :=
  let fi :=
    let bounds := hyps ++ map (T.eval_bnd prec) cf in
    fun b ⇒ nth 0 (A.BndValuator.eval prec pf (b :: bounds)) I.nai in
  let ui :=
    let bounds := hyps ++ map (T.eval_bnd prec) cu in
    nth 0 (A.BndValuator.eval prec pu bounds) I.nai in
  let vi :=
    let bounds := hyps ++ map (T.eval_bnd prec) cv in
    nth 0 (A.BndValuator.eval prec pv bounds) I.nai in
  let cb := fun x ⇒
    match x with IR.IBu ⇒ ui | IR.IBv ⇒ vi | IR.IBp x ⇒ I.singleton x end in
  let mid := fun u v ⇒
    let u := cb u in
    let v := cb v in
    I.midpoint (I.join u v) in
  let Fi :=
    let bounds := hyps ++ map (T.eval_bnd prec) cf in
    let bounds := map A.TaylorValuator.TM.const bounds in
    fun u v ⇒
      let u := cb u in
      let v := cb v in
      let xi := I.join u v in
      let gi :=
        A.TaylorValuator.TM.get_tm (prec, deg) xi
          (nth 0 (A.TaylorValuator.eval prec deg xi pf (A.TaylorValuator.TM.var :: bounds))
            A.TaylorValuator.TM.dummy) in
      IT.taylor_integral_naive_intersection prec fi gi xi u v in
  (mid, Fi).

Lemma contains_RInt :
  ∀ prec deg limit check vars hyps pf pu pv cf cu cv,
  R.eval_hyps_bnd (R.merge_hyps prec hyps) vars →
  no_floor_prog pf = true →
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_init prec deg hyps pf pu pv cf cu cv in
  contains (I.convert (IR.bisect prec limit mid Fi check))
    (Xreal (RInt (fun t ⇒ Prog.eval_real' pf (t :: vars) cf)
      (Prog.eval_real' pu vars cu) (Prog.eval_real' pv vars cv))).

Definition check_goal prec hyps pg cg g :=
  let bounds := hyps ++ map (T.eval_bnd prec) cg in
  let check := R.eval_goal_bnd prec g in
  fun b ⇒ check (nth 0 (A.BndValuator.eval prec pg (b :: bounds)) I.nai).

Definition eval_RInt prec deg limit hyps pg pf pu pv cg cf cu cv g :=
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_init prec deg hyps pf pu pv cf cu cv in
  let check := check_goal prec hyps pg cg g in
  check (IR.bisect prec limit mid Fi check).

Theorem eval_RInt_correct :
  ∀ prec deg limit vars hyps pg pf pu pv cg cf cu cv g,
  no_floor_prog pf = true →
  eval_RInt prec deg limit hyps pg pf pu pv cg cf cu cv g = true →
  eval_hyps hyps vars (
    eval_goal g (Prog.eval_real' pg (
      (RInt (fun t ⇒ Prog.eval_real' pf (t :: vars) cf)
        (Prog.eval_real' pu vars cu) (Prog.eval_real' pv vars cv)) :: vars) cg)).

Definition eval_RInt_contains prec deg limit hyps pf pu pv cf cu cv b :=
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_init prec deg hyps pf pu pv cf cu cv in
  let check yi := I.subset yi b in
  check (IR.bisect prec limit mid Fi check).

Theorem eval_RInt_contains_correct :
  ∀ prec deg limit vars hyps pf pu pv cf cu cv b,
  no_floor_prog pf = true →
  eval_RInt_contains prec deg limit hyps pf pu pv cf cu cv b = true →
  eval_hyps hyps vars (
    contains (I.convert b) (Xreal
      (RInt (fun t ⇒ Prog.eval_real' pf (t :: vars) cf)
        (Prog.eval_real' pu vars cu) (Prog.eval_real' pv vars cv)))).

Definition check_width prec (w : F.type × bool) yi :=
  let yl := I.lower yi in
  let yu := I.upper yi in
  let (f, r) := w in
  let w := if r then F.mul_UP prec (F.midpoint yl yu) f else f in
  F'.le' (F.sub_UP prec (I.upper yi) (I.lower yi)) f.

Definition eval_RInt_plain prec deg limit hyps pf pu pv cf cu cv w :=
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_init prec deg hyps pf pu pv cf cu cv in
  IR.bisect prec limit mid Fi (check_width prec w).

Definition bertrand_prog alpha beta p :=
  let x := length p in
  app p (Prog.Unary (PowerInt alpha) x :: Prog.Unary Ln (S x) :: Prog.Unary (PowerInt (Z_of_nat beta)) 0 :: Prog.Binary Mul 2 0 :: Prog.Binary Mul 4 0 :: nil).

Lemma bertrand_prog_correct :
  ∀ alpha beta p c x,
  nth 0 (Prog.eval_real (bertrand_prog alpha beta p) (x :: c)) 0 =
  (nth 0 (Prog.eval_real p (x :: c)) 0 × (powerRZ x alpha × pow (ln x) beta)).

Definition c1 := F.fromZ 1.

Definition bertrand_infty_interval alpha beta prec ui :=
  if F'.le' c1 (I.lower ui) then
    BI.f_int_fast prec ui alpha beta
  else I.nai.

Definition bertrand_zero_interval alpha beta prec vi :=
  if andb (F'.lt' F.zero (I.lower vi)) (F'.le' (I.upper vi) c1) then
    BI.f0eps_int prec vi alpha beta
  else I.nai.

Definition invxln_prog beta p :=
  let x := length p in
  app p (Prog.Unary Ln x :: Prog.Unary (PowerInt (Z_of_nat (S (S beta)))) 0 :: Prog.Binary Mul (S (S x)) 0 :: Prog.Binary Div 3 0 :: nil).

Lemma invxln_prog_correct :
  ∀ beta p c x,
  nth 0 (Prog.eval_real (invxln_prog beta p) (x :: c)) 0 =
  (nth 0 (Prog.eval_real p (x :: c)) 0 / (x × pow (ln x) (S (S beta)))).

Definition invxln_interval beta prec ui :=
  if F'.lt' c1 (I.lower ui) then
    BI.f_neg_int prec ui (S beta)
  else I.nai.


Definition eval_RInt_gen_infty_init prec deg hyps (mi : F.precision → I.type → I.type) pf pfm pu cf cfm cu :=
  let fi :=
    let bounds := hyps ++ map (T.eval_bnd prec) cf in
    fun b ⇒ nth 0 (A.BndValuator.eval prec pf (b :: bounds)) I.nai in
  let fmi :=
    let bounds := hyps ++ map (T.eval_bnd prec) cfm in
    fun b ⇒ nth 0 (A.BndValuator.eval prec pfm (b :: bounds)) I.nai in
  let ui :=
    let bounds := hyps ++ map (T.eval_bnd prec) cu in
    nth 0 (A.BndValuator.eval prec pu bounds) I.nai in
  let mid u v :=
    match u, v with
    | IR.IBu, IR.IBv ⇒ I.midpoint (I.upper_extent ui)
    | IR.IBu, IR.IBp v ⇒ I.midpoint (I.join ui (I.singleton v))
    | IR.IBp u, IR.IBv ⇒ I.midpoint (I.upper_extent (I.singleton u))
    | IR.IBp u, IR.IBp v ⇒ I.midpoint (I.bnd u v)
    | _, _ ⇒ F.zero
    end in
  let Fi1 :=
    let bounds := hyps ++ map (T.eval_bnd prec) cfm in
    let bounds := map A.TaylorValuator.TM.const bounds in
    fun ui vi ⇒
      let xi := I.join ui vi in
      let gi :=
        A.TaylorValuator.TM.get_tm (prec, deg) xi
          (nth 0 (A.TaylorValuator.eval prec deg xi pfm (A.TaylorValuator.TM.var :: bounds))
            A.TaylorValuator.TM.dummy) in
      IT.taylor_integral_naive_intersection prec fmi gi xi ui vi in
  let Fi2 :=
    let bounds := hyps ++ map (T.eval_bnd prec) cf in
    let bounds := map A.TaylorValuator.TM.const bounds in
    fun ui ⇒
      let yi := fi (I.upper_extent ui) in
      if I.bounded yi then I.mul prec yi (mi prec ui) else I.nai in
  let Fi u v :=
    match u, v with
    | IR.IBu, IR.IBv ⇒ Fi2 ui
    | IR.IBu, IR.IBp v ⇒ Fi1 ui (I.singleton v)
    | IR.IBp u, IR.IBv ⇒ Fi2 (I.singleton u)
    | IR.IBp u, IR.IBp v ⇒ Fi1 (I.singleton u) (I.singleton v)
    | _, _ ⇒ I.nai
    end in
  (mid, Fi).

Lemma contains_RInt_gen_infty :
  ∀ prec deg limit check vars hyps mi mp mr pf pu cf cu,
  R.eval_hyps_bnd (R.merge_hyps prec hyps) vars →
  (∀ yi ui f u, contains (I.convert ui) (Xreal u) →
    (∀ t, (u ≤ t)%R → continuous f t) →
    (∀ t, (u ≤ t)%R → contains (I.convert yi) (Xreal (f t))) →
    I.bounded yi = true →
    I.convert (mi prec ui) ≠ Inan →
    ∃ I : R,
    is_RInt_gen (fun t : R ⇒ f t × mr t) (at_point u) (Rbar_locally p_infty) I ∧
    contains (I.convert (I.mul prec yi (mi prec ui))) (Xreal I)) →
  (∀ c t, nth 0 (Prog.eval_real mp (t :: c)) 0 = nth 0 (Prog.eval_real pf (t :: c)) 0 × mr t)%R →
  no_floor_prog mp = true →
  no_floor_prog pf = true →
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps mi pf mp pu cf cf cu in
  contains (I.convert (IR.bisect prec limit mid Fi check))
    (Xreal (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × mr t)
      (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty))).

Definition eval_RInt_gen_infty prec deg limit hyps mi pg pf pfm pu cg cf cfm cu g :=
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps mi pf pfm pu cf cfm cu in
  let check := check_goal prec hyps pg cg g in
  check (IR.bisect prec limit mid Fi check).

Definition eval_RInt_gen_infty_contains prec deg limit hyps mi pf pfm pu cf cfm cu b :=
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps mi pf pfm pu cf cfm cu in
  let check yi := I.subset yi b in
  check (IR.bisect prec limit mid Fi check).

Definition eval_RInt_gen_infty_plain prec deg limit hyps mi pf pfm pu cf cfm cu w :=
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps mi pf pfm pu cf cfm cu in
  IR.bisect prec limit mid Fi (check_width prec w).

Lemma contains_RInt_gen_infty_bertrand :
  ∀ prec deg limit check vars hyps alpha beta pf pu cf cu,
  R.eval_hyps_bnd (R.merge_hyps prec hyps) vars →
  (alpha < -1)%Z →
  no_floor_prog pf = true →
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps (bertrand_infty_interval alpha beta) pf (bertrand_prog alpha beta pf) pu cf cf cu in
  contains (I.convert (IR.bisect prec limit mid Fi check))
    (Xreal (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × (powerRZ t alpha × pow (ln t) beta))
      (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty))).

Theorem eval_RInt_gen_infty_bertrand :
  ∀ prec deg limit vars hyps alpha beta pg pf pu cg cf cu g,
  (alpha < -1)%Z →
  no_floor_prog pf = true →
  eval_RInt_gen_infty prec deg limit hyps (bertrand_infty_interval alpha beta) pg pf (bertrand_prog alpha beta pf) pu cg cf cf cu g = true →
  eval_hyps hyps vars (
    eval_goal g (Prog.eval_real' pg (
      (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × (powerRZ t alpha × pow (ln t) beta))
        (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty)) :: vars) cg)).

Theorem eval_RInt_gen_infty_contains_bertrand :
  ∀ prec deg limit vars hyps alpha beta pf pu cf cu b,
  (alpha < -1)%Z →
  no_floor_prog pf = true →
  eval_RInt_gen_infty_contains prec deg limit hyps (bertrand_infty_interval alpha beta) pf (bertrand_prog alpha beta pf) pu cf cf cu b = true →
  eval_hyps hyps vars (
    contains (I.convert b) (Xreal
      (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × (powerRZ t alpha × pow (ln t) beta))
        (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty)))).

Lemma contains_RInt_gen_infty_invxln :
  ∀ prec deg limit check vars hyps beta pf pu cf cu,
  R.eval_hyps_bnd (R.merge_hyps prec hyps) vars →
  no_floor_prog pf = true →
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_infty_init prec deg hyps (invxln_interval beta) pf (invxln_prog beta pf) pu cf cf cu in
  contains (I.convert (IR.bisect prec limit mid Fi check))
    (Xreal (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf / (t × pow (ln t) (S (S beta))))
      (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty))).

Theorem eval_RInt_gen_infty_invxln :
  ∀ prec deg limit vars hyps beta pg pf pu cg cf cu g,
  no_floor_prog pf = true →
  eval_RInt_gen_infty prec deg limit hyps (invxln_interval beta) pg pf (invxln_prog beta pf) pu cg cf cf cu g = true →
  eval_hyps hyps vars (
    eval_goal g (Prog.eval_real' pg (
      (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf / (t × pow (ln t) (S (S beta))))
        (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty)) :: vars) cg)).

Theorem eval_RInt_gen_infty_contains_invxln :
  ∀ prec deg limit vars hyps beta pf pu cf cu b,
  no_floor_prog pf = true →
  eval_RInt_gen_infty_contains prec deg limit hyps (invxln_interval beta) pf (invxln_prog beta pf) pu cf cf cu b = true →
  eval_hyps hyps vars (
    contains (I.convert b) (Xreal
      (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf / (t × pow (ln t) (S (S beta))))
        (at_point (Prog.eval_real' pu vars cu)) (Rbar_locally p_infty)))).

Definition eval_RInt_gen_zero_init prec deg hyps (mi : I.precision → I.type → I.type) pf pfm pv cf cfm cv :=
  let fi :=
    let bounds := hyps ++ map (T.eval_bnd prec) cf in
    fun b ⇒ nth 0 (A.BndValuator.eval prec pf (b :: bounds)) I.nai in
  let fmi :=
    let bounds := hyps ++ map (T.eval_bnd prec) cfm in
    fun b ⇒ nth 0 (A.BndValuator.eval prec pfm (b :: bounds)) I.nai in
  let vi :=
    let bounds := hyps ++ map (T.eval_bnd prec) cv in
    nth 0 (A.BndValuator.eval prec pv bounds) I.nai in
  let mid u v :=
    match u, v with
    | IR.IBu, IR.IBv ⇒ I.midpoint (I.join I.zero vi)
    | IR.IBu, IR.IBp v ⇒ I.midpoint (I.bnd F.zero v)
    | IR.IBp u, IR.IBv ⇒ I.midpoint (I.join (I.singleton u) vi)
    | IR.IBp u, IR.IBp v ⇒ I.midpoint (I.bnd u v)
    | _, _ ⇒ F.zero
    end in
  let Fi1 :=
    let bounds := hyps ++ map (T.eval_bnd prec) cfm in
    let bounds := map A.TaylorValuator.TM.const bounds in
    fun ui vi ⇒
      let xi := I.join ui vi in
      let gi :=
        A.TaylorValuator.TM.get_tm (prec, deg) xi
          (nth 0 (A.TaylorValuator.eval prec deg xi pfm (A.TaylorValuator.TM.var :: bounds))
            A.TaylorValuator.TM.dummy) in
      IT.taylor_integral_naive_intersection prec fmi gi xi ui vi in
  let Fi2 :=
    let bounds := hyps ++ map (T.eval_bnd prec) cf in
    let bounds := map A.TaylorValuator.TM.const bounds in
    fun vi ⇒
      let yi := fi (I.join I.zero vi) in
      if I.bounded yi then I.mul prec yi (mi prec vi) else I.nai in
  let Fi u v :=
    match u, v with
    | IR.IBu, IR.IBv ⇒ Fi2 vi
    | IR.IBu, IR.IBp v ⇒ Fi2 (I.singleton v)
    | IR.IBp u, IR.IBv ⇒ Fi1 (I.singleton u) vi
    | IR.IBp u, IR.IBp v ⇒ Fi1 (I.singleton u) (I.singleton v)
    | _, _ ⇒ I.nai
    end in
  (mid, Fi).

Lemma contains_RInt_gen_zero :
  ∀ prec deg limit check vars hyps mi mp mr pf pv cf cv,
  R.eval_hyps_bnd (R.merge_hyps prec hyps) vars →
  (∀ yi vi f v, contains (I.convert vi) (Xreal v) →
    (∀ t, (0 ≤ t ≤ v)%R → continuous f t) →
    (∀ t, (0 ≤ t ≤ v)%R → contains (I.convert yi) (Xreal (f t))) →
    I.bounded yi = true →
    I.convert (mi prec vi) ≠ Inan →
    ∃ I : R,
    is_RInt_gen (fun t : R ⇒ f t × mr t) (at_right 0) (at_point v) I ∧
    contains (I.convert (I.mul prec yi (mi prec vi))) (Xreal I)) →
  (∀ c t, nth 0 (Prog.eval_real mp (t :: c)) 0 = nth 0 (Prog.eval_real pf (t :: c)) 0 × mr t)%R →
  no_floor_prog mp = true →
  no_floor_prog pf = true →
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_zero_init prec deg hyps mi pf mp pv cf cf cv in
  contains (I.convert (IR.bisect prec limit mid Fi check))
    (Xreal (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × mr t)
      (at_right 0) (at_point (Prog.eval_real' pv vars cv)))).

Definition eval_RInt_gen_zero prec deg limit hyps mi pg pf pfm pv cg cf cfm cv g :=
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_zero_init prec deg hyps mi pf pfm pv cf cfm cv in
  let check := check_goal prec hyps pg cg g in
  check (IR.bisect prec limit mid Fi check).

Definition eval_RInt_gen_zero_contains prec deg limit hyps mi pf pfm pv cf cfm cv b :=
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_zero_init prec deg hyps mi pf pfm pv cf cfm cv in
  let check yi := I.subset yi b in
  check (IR.bisect prec limit mid Fi check).

Definition eval_RInt_gen_zero_plain prec deg limit hyps mi pf pfm pv cf cfm cv w :=
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_zero_init prec deg hyps mi pf pfm pv cf cfm cv in
  IR.bisect prec limit mid Fi (check_width prec w).

Lemma contains_RInt_gen_zero_bertrand :
  ∀ prec deg limit check vars hyps alpha beta pf pv cf cv,
  R.eval_hyps_bnd (R.merge_hyps prec hyps) vars →
  (-1 < alpha)%Z →
  no_floor_prog pf = true →
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_zero_init prec deg hyps (bertrand_zero_interval alpha beta) pf (bertrand_prog alpha beta pf) pv cf cf cv in
  contains (I.convert (IR.bisect prec limit mid Fi check))
    (Xreal (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × (powerRZ t alpha × pow (ln t) beta))
      (at_right 0) (at_point (Prog.eval_real' pv vars cv)))).

Theorem eval_RInt_gen_zero_bertrand :
  ∀ prec deg limit vars hyps alpha beta pg pf pv cg cf cv g,
  (-1 < alpha)%Z →
  no_floor_prog pf = true →
  eval_RInt_gen_zero prec deg limit hyps (bertrand_zero_interval alpha beta) pg pf (bertrand_prog alpha beta pf) pv cg cf cf cv g = true →
  eval_hyps hyps vars (
    eval_goal g (Prog.eval_real' pg (
      (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × (powerRZ t alpha × pow (ln t) beta))
        (at_right 0) (at_point (Prog.eval_real' pv vars cv))) :: vars) cg)).

Theorem eval_RInt_gen_zero_contains_bertrand :
  ∀ prec deg limit vars hyps alpha beta pf pv cf cv b,
  (-1 < alpha)%Z →
  no_floor_prog pf = true →
  eval_RInt_gen_zero_contains prec deg limit hyps (bertrand_zero_interval alpha beta) pf (bertrand_prog alpha beta pf) pv cf cf cv b = true →
  eval_hyps hyps vars (contains (I.convert b)
    (Xreal (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × (powerRZ t alpha × pow (ln t) beta))
       (at_right 0) (at_point (Prog.eval_real' pv vars cv))))).

Lemma contains_RInt_gen_zero_bertrand_pow0 :
  ∀ prec deg limit check vars hyps beta pf pv cf cv,
  R.eval_hyps_bnd (R.merge_hyps prec hyps) vars →
  no_floor_prog pf = true →
  let hyps := R.merge_hyps prec hyps in
  let (mid, Fi) := eval_RInt_gen_zero_init prec deg hyps (bertrand_zero_interval 0 beta) pf (bertrand_prog 0 beta pf) pv cf cf cv in
  contains (I.convert (IR.bisect prec limit mid Fi check))
    (Xreal (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × pow (ln t) beta)
      (at_right 0) (at_point (Prog.eval_real' pv vars cv)))).

Theorem eval_RInt_gen_zero_bertrand_pow0 :
  ∀ prec deg limit vars hyps beta pg pf pv cg cf cv g,
  no_floor_prog pf = true →
  eval_RInt_gen_zero prec deg limit hyps (bertrand_zero_interval 0 beta) pg pf (bertrand_prog 0 beta pf) pv cg cf cf cv g = true →
  eval_hyps hyps vars (
    eval_goal g (Prog.eval_real' pg (
      (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × pow (ln t) beta)
        (at_right 0) (at_point (Prog.eval_real' pv vars cv))) :: vars) cg)).

Theorem eval_RInt_gen_zero_contains_bertrand_pow0 :
  ∀ prec deg limit vars hyps beta pf pv cf cv b,
  no_floor_prog pf = true →
  eval_RInt_gen_zero_contains prec deg limit hyps (bertrand_zero_interval 0 beta) pf (bertrand_prog 0 beta pf) pv cf cf cv b = true →
  eval_hyps hyps vars (contains (I.convert b)
    (Xreal (RInt_gen (fun t ⇒ Prog.eval_real' pf (t :: vars) cf × pow (ln t) beta)
       (at_right 0) (at_point (Prog.eval_real' pv vars cv))))).

Ltac do_integral prec degree fuel native nocheck :=
  massage_goal ;
  match goal with
  | |- eval_goal ?g' ?y ⇒
    let g := fresh "__goal" in
    set (g := g') ;
    lazymatch y with
    | context [RInt ?f ?u ?v] ⇒
      reify_RInt y f u v ;
      apply (eval_RInt_correct prec degree fuel) with (1 := eq_refl true)
    | context [RInt_gen ?fm (at_point ?u) (Rbar_locally p_infty)] ⇒
      reify_RInt_gen_infty y fm u ;
      lazymatch fm with
      | fun t ⇒ (_ / (t × ln t ^ _))%R ⇒
        apply (eval_RInt_gen_infty_invxln prec degree fuel) with (1 := eq_refl true)
      | fun t ⇒ (_ × / (t × ln t ^ _))%R ⇒
        apply (eval_RInt_gen_infty_invxln prec degree fuel) with (1 := eq_refl true)
      | fun t ⇒ (_ × (powerRZ t _ × ln t ^ _))%R ⇒
        apply (eval_RInt_gen_infty_bertrand prec degree fuel) with (1 := eq_refl Lt) (2 := eq_refl true)
      | _ ⇒ fail "No integral recognized"
      end
    | context [RInt_gen ?fm (at_right 0) (at_point ?v)] ⇒
      reify_RInt_gen_zero y fm v ;
      lazymatch fm with
      | fun t ⇒ (_ × (powerRZ t _ × ln t ^ _))%R ⇒
        apply (eval_RInt_gen_zero_bertrand prec degree fuel) with (1 := eq_refl Lt) (2 := eq_refl true)
      | fun t ⇒ (_ × ln t ^ _)%R ⇒
        apply (eval_RInt_gen_zero_bertrand_pow0 prec degree fuel) with (1 := eq_refl true)
      | _ ⇒ fail "No integral recognized"
      end
    | _ ⇒ fail "No integral recognized"
    end
  end ;
  do_reduction nocheck native.

Ltac do_integral_intro y extend prec degree fuel width native nocheck output :=
  let extend := constr:(extent extend) in
  let width :=
    match width with
    | (?p, ?b) ⇒ constr:((F.scale (F.fromZ 1) (F.ZtoS p), b))
    end in
  let i := fresh "__i" in
  evar (i : I.type) ;
  cut (contains (I.convert i) (Xreal y))%R ; cycle 1 ; [
    lazymatch y with
    | RInt ?f ?u ?v ⇒
      reify_RInt y f u v ;
      apply (eval_RInt_contains_correct prec degree fuel) with (1 := eq_refl true) ;
      match goal with
      | |- _ ?hyps ?pf ?pu ?pv ?cf ?cu ?cv _ = true ⇒
        let yi := constr:(eval_RInt_plain prec degree fuel hyps pf pu pv cf cu cv width) in
        do_instantiate i extend native yi
      end
    | RInt_gen ?fm (at_point ?u) (Rbar_locally p_infty) ⇒
      reify_RInt_gen_infty y fm u ;
      lazymatch fm with
      | fun t ⇒ (_ / (t × ln t ^ _))%R ⇒
        apply (eval_RInt_gen_infty_contains_invxln prec degree fuel) with (1 := eq_refl true)
      | fun t ⇒ (_ × / (t × ln t ^ _))%R ⇒
        apply (eval_RInt_gen_infty_contains_invxln prec degree fuel) with (1 := eq_refl true)
      | fun t ⇒ (_ × (powerRZ t _ × ln t ^ _))%R ⇒
        apply (eval_RInt_gen_infty_contains_bertrand prec degree fuel) with (1 := eq_refl Lt) (2 := eq_refl true)
      | _ ⇒ fail "No integral recognized"
      end ;
      match goal with
      | |- _ ?hyps ?mi ?pf ?pfm ?pu ?cf ?cfm ?cu _ = true ⇒
        let yi := constr:(eval_RInt_gen_infty_plain prec degree fuel hyps mi pf pfm pu cf cfm cu width) in
        do_instantiate i extend native yi
      end
    | RInt_gen ?fm (at_right 0) (at_point ?v) ⇒
      reify_RInt_gen_zero y fm v ;
      lazymatch fm with
      | fun t ⇒ (_ × (powerRZ t _ × ln t ^ _))%R ⇒
        apply (eval_RInt_gen_zero_contains_bertrand prec degree fuel) with (1 := eq_refl Lt) (2 := eq_refl true)
      | fun t ⇒ (_ × ln t ^ _)%R ⇒
        apply (eval_RInt_gen_zero_contains_bertrand_pow0 prec degree fuel) with (1 := eq_refl true)
      | _ ⇒ fail "No integral recognized"
      end ;
      match goal with
      | |- _ ?hyps ?mi ?pf ?pfm ?pv ?cf ?cfm ?cv _ = true ⇒
        let yi := constr:(eval_RInt_gen_zero_plain prec degree fuel hyps mi pf pfm pv cf cfm cv width) in
        do_instantiate i extend native yi
      end
    | _ ⇒ fail "No integral recognized"
    end ;
    do_reduction nocheck native
  | unfold i ; clear i ;
    do_interval_generalize (I.output_correct output) ].

End IntegralTacticAux.