Library Interval.Real.Xreal_derive

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 Reals.
From Flocq Require Import Raux.

Require Import Stdlib.
Require Import Xreal.

Theorem derivable_imp_defined :
  ∀ f r d u v,
  f (Xreal r) = Xreal u → u ≠ v →
  derivable_pt_lim (proj_fun v f) r d →
  locally_true r (fun a ⇒ ∃ w , f (Xreal a) = Xreal w).

Theorem derivable_imp_defined_any :
  ∀ f r d u,
  f (Xreal r) = Xreal u →
(∀ v, derivable_pt_lim (proj_fun v f) r d ) →
  locally_true r (fun a ⇒ ∃ w , f (Xreal a) = Xreal w).

Theorem derivable_imp_defined_any_2 :
  ∀ f1 f2 r d1 d2 u1 u2,
  f1 (Xreal r) = Xreal u1 →
  f2 (Xreal r) = Xreal u2 →
(∀ v, derivable_pt_lim (proj_fun v f1) r d1 ) →
(∀ v, derivable_pt_lim (proj_fun v f2) r d2 ) →
  locally_true r (fun a ⇒
    (∃ w1 , f1 (Xreal a) = Xreal w1 ) ∧
    (∃ w2 , f2 (Xreal a) = Xreal w2 )).

Theorem derivable_imp_defined_gt :
  ∀ f r d u t,
  f (Xreal r) = Xreal u → (t < u)%R →
(∀ v, derivable_pt_lim (proj_fun v f) r d ) →
  locally_true r (fun a ⇒ ∃ w , (t < w)%R ∧ f (Xreal a) = Xreal w).

Theorem derivable_imp_defined_lt :
  ∀ f r d u t,
  f (Xreal r) = Xreal u → (u < t)%R →
(∀ v, derivable_pt_lim (proj_fun v f) r d ) →
  locally_true r (fun a ⇒ ∃ w , (w < t)%R ∧ f (Xreal a) = Xreal w).

Theorem derivable_imp_defined_ne :
  ∀ f r d u t,
  f (Xreal r) = Xreal u → (u ≠ t)%R →
(∀ v, derivable_pt_lim (proj_fun v f) r d ) →
  locally_true r (fun a ⇒ ∃ w , (w ≠ t)%R ∧ f (Xreal a) = Xreal w).

Definition Xderive_pt f x y' :=
  match x, y', f x with
  | Xreal r, Xreal d, Xreal _ ⇒ ∀ v, derivable_pt_lim (proj_fun v f) r d
  | _, Xnan, _ ⇒ True
  | _, _, _ ⇒ False
  end.

Definition Xderive f f' := ∀ x, Xderive_pt f x (f' x).

Ltac xtotal_get_spec1 f :=
  match f with
  | Req_bool ⇒ Req_bool_spec
  | Rle_bool ⇒ Rle_bool_spec
  | Rlt_bool ⇒ Rlt_bool_spec
  | is_zero ⇒ is_zero_spec
  | is_positive ⇒ is_positive_spec
  | is_negative ⇒ is_negative_spec
  end.

Ltac xtotal_destruct_xreal v :=
  match v with
  | context [?f ?x] ⇒
    let r := fresh "r" in
    let X := fresh "X" in
    case_eq v ; [ intros X | intros r X ] ; try rewrite X in ×
  | _ ⇒
    let r := fresh "r" in
    destruct v as [|r]
  end.

Ltac xtotal_aux :=
  trivial ;
  try discriminate ;
  match goal with
  | H: False |- _ ⇒ elim H

  | H: ?v = ?v |- _ ⇒ clear H
  | H: Xreal _ = Xreal _ |- _ ⇒
    injection H ; clear H ; intro H
  | H: context [match ?v with Xnan ⇒ _ | Xreal _ ⇒ _ end] |- _ ⇒
    xtotal_destruct_xreal v ; try discriminate H ; trivial

  | H1 : Xderive ?f1 ?f2 , H2 : context [?f2 ?v] |- _ ⇒
    generalize (H1 v) ; clear H1 ; intro H1 ; unfold Xderive_pt in H1
  | H: ?v = Xreal _ |- _ ⇒ rewrite H in ×
  | H: ?v = Xnan |- _ ⇒ rewrite H in ×
  | v: R, H: ?v = _ |- _ ⇒
    try rewrite H in × ; clear H v
  | v: R, H: _ = ?v |- _ ⇒
    try rewrite <- H in × ; clear H v
  | H: context [?f ?v] |- _ ⇒
    let s := xtotal_get_spec1 f in
    let Y := fresh "Y" in
    destruct (s v) as [Y|Y]
  | H: match ?v with true ⇒ Xnan | false ⇒ Xreal _ end = _ |- _ ⇒
    let X := fresh "X" in
    case_eq v ; intro X ; rewrite X in H ; try discriminate H
  | |- match ?v with Xnan ⇒ _ | Xreal _ ⇒ _ end ⇒
    xtotal_destruct_xreal v
  | |- context [?f ?v] ⇒
    let s := xtotal_get_spec1 f in
    let Y := fresh "Y" in
    destruct (s v) as [Y|Y]
  end.

Ltac xtotal :=
  unfold Xderive_pt, Xinv', Xdiv', Xsqrt', Xtan', Xln', Xpower_int, Xpower_int', Xmask, Xbind2, Xbind in × ;
  repeat xtotal_aux.

Theorem Xderive_pt_add :
  ∀ f g f' g' x,
  Xderive_pt f x f' → Xderive_pt g x g' →
  Xderive_pt (fun x ⇒ Xadd (f x) (g x)) x (Xadd f' g').

Theorem Xderive_pt_sub :
  ∀ f g f' g' x,
  Xderive_pt f x f' → Xderive_pt g x g' →
  Xderive_pt (fun x ⇒ Xsub (f x) (g x)) x (Xsub f' g').

Theorem Xderive_pt_mul :
  ∀ f g f' g' x,
  Xderive_pt f x f' → Xderive_pt g x g' →
  Xderive_pt (fun x ⇒ Xmul (f x) (g x)) x (Xadd (Xmul f' (g x)) (Xmul g' (f x))).

Theorem Xderive_pt_div :
  ∀ f g f' g' x,
  Xderive_pt f x f' → Xderive_pt g x g' →
  Xderive_pt (fun x ⇒ Xdiv (f x) (g x)) x (Xdiv (Xsub (Xmul f' (g x)) (Xmul g' (f x))) (Xmul (g x) (g x))).

Theorem Xderive_pt_neg :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xneg (f x)) x (Xneg f').

Theorem Xderive_pt_abs :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xabs (f x)) x (match Xcmp (f x) (Xreal 0) with Xlt ⇒ Xneg f' | Xgt ⇒ f' | _ ⇒ Xnan end).

Theorem Xderive_pt_inv :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xinv (f x)) x (Xneg (Xdiv f' (Xsqr (f x)))).

Theorem Xderive_pt_sqrt :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xsqrt (f x)) x (Xdiv f' (Xadd (Xsqrt (f x)) (Xsqrt (f x)))).

Theorem Xderive_pt_sin :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xsin (f x)) x (Xmul f' (Xcos (f x))).

Theorem Xderive_pt_cos :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xcos (f x)) x (Xmul f' (Xneg (Xsin (f x)))).

Theorem Xderive_pt_tan :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xtan (f x)) x (Xmul f' (Xadd (Xreal 1) (Xsqr (Xtan (f x))))).

Theorem Xderive_pt_exp :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xexp (f x)) x (Xmul f' (Xexp (f x))).

Theorem Xderive_pt_ln :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xln (f x)) x (match Xcmp (f x) (Xreal 0) with Xgt ⇒ Xdiv f' (f x) | _ ⇒ Xnan end).

Theorem Xderive_pt_atan :
  ∀ f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xatan (f x)) x (Xdiv f' (Xadd (Xreal 1) (Xsqr (f x)))).

Theorem Xderive_pt_power_int :
  ∀ n f f' x,
  Xderive_pt f x f' →
  Xderive_pt (fun x ⇒ Xpower_int (f x) n) x (Xmul f' (Xmul (Xreal (IZR n)) (Xpower_int (f x) (Z.pred n)))).

Theorem Xderive_pt_partial_fun :
  ∀ g f f',
(∀ x y, g x = Xreal y → f x = Xreal y ) →
  ∀ x,
  Xderive_pt g x f' →
  Xderive_pt f x f'.

Theorem Xderive_pt_eq_fun :
  ∀ g f f',
(∀ x, f x = g x ) →
  ∀ x,
  Xderive_pt g x f' →
  Xderive_pt f x f'.

Theorem Xderive_pt_identity :
  ∀ x, Xderive_pt (fun x ⇒ x) x (Xmask (Xreal 1) x).

Theorem Xderive_pt_constant :
  ∀ v x,
  Xderive_pt (fun _ ⇒ Xreal v) x (Xmask (Xreal 0) x).

Theorem Xderive_MVT :
  ∀ f f',
  Xderive f f' →
  ∀ dom : R → Prop,
  connected dom →
(∀ x, dom x → f' (Xreal x) ≠ Xnan ) →
  ∀ m, dom m →
  ∀ x, dom x →
  ∃ c , dom c ∧
  f (Xreal x) = Xadd (f (Xreal m)) (Xmul (f' (Xreal c)) (Xsub (Xreal x) (Xreal m))).