Library mathcomp.analysis.derive

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
Require Import reals signed topology prodnormedzmodule normedtype landau forms.

This file provides a theory of differentiation. It includes the standard rules of differentiation (differential of a sum, of a product, of exponentiation, of the inverse, etc.) as well as standard theorems (the Extreme Value Theorem, Rolle's theorem, the Mean Value Theorem). Parsable notations (in all of the following, f is not supposed to be differentiable): 'd f x == the differential of a function f at a point x differentiable f x == the function f is differentiable at a point x 'J f x == the Jacobian of f at a point x 'D_v f == the directional derivative of f along v f^`() == the derivative of f of domain R f^`(n) == the nth derivative of f of domain R

Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope ring_scope.
Local Open Scope classical_set_scope.

Reserved Notation "''d' f x" (at level 0, f at level 0, x at level 0,
  format "''d' f x").
Reserved Notation "'is_diff' F" (at level 0, F at level 0,
  format "'is_diff' F").
Reserved Notation "''J' f p" (at level 10, p, f at next level,
  format "''J' f p").
Reserved Notation "''D_' v f" (at level 10, v, f at next level,
  format "''D_' v f").
Reserved Notation "''D_' v f c" (at level 10, v, f at next level,
  format "''D_' v f c"). (* printing *)
Reserved Notation "f ^` ()" (at level 8, format "f ^` ()").
Reserved Notation "f ^` ( n )" (at level 8, format "f ^` ( n )").

Section Differential.
Context {K : numDomainType} {V W : normedModType K}.

Definition diff (F : filter_on V) (_ : phantom (set (set V)) F) (f : V → W) :=
  (get (fun (df : {linear V → W}) ⇒ continuous df ∧ ∀ x,
      f x = f (lim F) + df (x - lim F) +o_(x \near F ) (x - lim F ))).

Fact diff_key : ∀ T, T → unit.
CoInductive differentiable_def (f : V → W) (x : filter_on V)
  (phF : phantom (set (set V)) x) : Prop := DifferentiableDef of
  (continuous ('d f x) ∧
  f = cst (f (lim x)) + 'd f x \o center (lim x) +o_x (center (lim x))).

Class is_diff_def (x : filter_on V) (Fph : phantom (set (set V)) x) (f : V → W)
  (df : V → W) := DiffDef {
    ex_diff : differentiable f x ;
    diff_val : 'd f x = df :> (V → W )
  }.

Lemma diffP (F : filter_on V) (f : V → W) :
  differentiable f F ↔
  continuous ('d f F) ∧
  (∀ x, f x = f (lim F) + 'd f F (x - lim F ) +o_(x \near F ) (x - lim F )).

Lemma diff_continuous (x : filter_on V) (f : V → W) :
  differentiable f x → continuous ('d f x).

We should have a continuous class or structure

Hint Extern 0 (continuous _) ⇒ exact: diff_continuous : core.

Lemma diffE (F : filter_on V) (f : V → W) :
  differentiable f F →
  ∀ x, f x = f (lim F) + 'd f F (x - lim F ) +o_(x \near F ) (x - lim F ).

Lemma littleo_center0 (x : V) (f : V → W) (e : V → V) :
  [o_x e of f ] = [o_ (0 : V ) (e \o shift x ) of f \o shift x ] \o center x.

End Differential.

Section Differential_numFieldType.
Context {K : numFieldType } {V W : normedModType K}.

Hint Extern 0 (continuous _) ⇒ exact: diff_continuous : core.

Lemma diff_locallyxP (x : V) (f : V → W) :
  differentiable f x ↔ continuous ('d f x) ∧
  ∀ h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V ) h.

Lemma diff_locallyx (x : V) (f : V → W) : differentiable f x →
  ∀ h, f (h + x) = f x + 'd f x h +o_(h \near 0 : V ) h.

Lemma diff_locallyxC (x : V) (f : V → W) : differentiable f x →
  ∀ h, f (x + h) = f x + 'd f x h +o_(h \near 0 : V ) h.

Lemma diff_locallyP (x : V) (f : V → W) :
  differentiable f x ↔
  continuous ('d f x) ∧ (f \o shift x = cst (f x) + 'd f x +o_ (0 : V ) id ).

Lemma diff_locally (x : V) (f : V → W) : differentiable f x →
  (f \o shift x = cst (f x) + 'd f x +o_ (0 : V ) id ).

End Differential_numFieldType.

Notation "''d' f F" := (@diff _ _ _ _ (Phantom _ [filter of F]) f).
Notation differentiable f F := (@differentiable_def _ _ _ f _ (Phantom _ [filter of F])).

Notation "'is_diff' F" := (is_diff_def (Phantom _ [filter of F])).
#[global] Hint Extern 0 (differentiable _ _) ⇒ solve[apply: ex_diff] : core.
#[global] Hint Extern 0 ({for _, continuous _}) ⇒ exact: diff_continuous : core.

Lemma differentiableP (R : numDomainType) (V W : normedModType R) (f : V → W) x :
  differentiable f x → is_diff x f ('d f x ).

Section jacobian.

Definition jacobian n m (R : numFieldType) (f : 'rV[R]_n.+1 → 'rV[R]_m.+1) p :=
  lin1_mx ('d f p).

End jacobian.

Notation "''J' f p" := (jacobian f p).

Section DifferentialR.

Context {R : numFieldType} {V W : normedModType R}.

split in multiple bits:

a linear map which is locally bounded is a little o of 1
the identity is a littleo of 1

Lemma differentiable_continuous (x : V) (f : V → W) :
differentiable f x → {for x , continuous f }.

Section littleo_lemmas.

Variables (X Y Z : normedModType R).

Lemma normm_littleo x (f : X → Y) : `| [o_(x \near x ) (1 : R ) of f x ]| = 0.

Lemma littleo_lim0 (f : X → Y) (h : _ → Z) (x : X) :
f @ x --> (0 : Y ) → [o_x f of h ] x = 0.

End littleo_lemmas.

Section diff_locally_converse_tentative.

if there exist A and B s.t. f(a + h) = A + B h + o(h) then f is differentiable at a, A = f(a) and B = f'(a) this is a consequence of diff_continuous and eqolim0 indeed the differential being b *: idfun is locally bounded and thus a littleo of 1, and so is id This can be generalized to any dimension

Lemma diff_locally_converse_part1 (f : R → R) (a b x : R) :
  f \o shift x = cst a + b *: idfun +o_ (0 : R ) id → f x = a.

End diff_locally_converse_tentative.

Definition derive (f : V → W) a v :=
  lim ((fun h ⇒ h^-1 *: ((f \o shift a ) (h *: v ) - f a)) @ 0^').

(* printing *)

Definition derivable (f : V → W) a v :=
  cvg ((fun h ⇒ h^-1 *: ((f \o shift a ) (h *: v ) - f a)) @ 0^').

Class is_derive (a v : V) (f : V → W) (df : W) := DeriveDef {
  ex_derive : derivable f a v;
  derive_val : 'D_v f a = df
}.

Lemma derivable_nbhs (f : V → W) a v :
  derivable f a v →
  (fun h ⇒ (f \o shift a ) (h *: v )) = (cst (f a)) +
    (fun h ⇒ h *: ('D_v f a)) +o_ (nbhs (0 :R)) id.

Lemma derivable_nbhsP (f : V → W) a v :
  derivable f a v ↔
  (fun h ⇒ (f \o shift a ) (h *: v )) = (cst (f a)) +
    (fun h ⇒ h *: ('D_v f a)) +o_ (nbhs (0 : R)) id.

Lemma derivable_nbhsx (f : V → W) a v :
  derivable f a v → ∀ h, f (a + h *: v) = f a + h *: 'D_v f a
  +o_(h \near (nbhs (0 : R))) h.

Lemma derivable_nbhsxP (f : V → W) a v :
  derivable f a v ↔ ∀ h, f (a + h *: v) = f a + h *: 'D_v f a
  +o_(h \near (nbhs (0 :R))) h.

End DifferentialR.

Notation "''D_' v f" := (derive f ^~ v).
Notation "''D_' v f c" := (derive f c v). (* printing *)
#[global] Hint Extern 0 (derivable _ _ _) ⇒ solve[apply: ex_derive] : core.

Section DifferentialR_numFieldType.
Context {R : numFieldType} {V W : normedModType R}.

Lemma deriveE (f : V → W) (a v : V) :
  differentiable f a → 'D_v f a = 'd f a v.

End DifferentialR_numFieldType.

Section DifferentialR2.
Variable R : numFieldType.
Implicit Type (V : normedModType R).

Lemma derivemxE m n (f : 'rV[R]_m.+1 → 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) :
  differentiable f a → 'D_ v f a = v ×m jacobian f a.

Definition derive1 V (f : R → V) (a : R) :=
   lim ((fun h ⇒ h^-1 *: (f (h + a) - f a)) @ 0^').

Lemma derive1E V (f : R → V) a : f ^`() a = 'D_1 f a.

Is it necessary?

Lemma derive1E' V f a : differentiable (f : R → V) a →
  f ^`() a = 'd f a 1.

Definition derive1n V n (f : R → V) := iter n (@derive1 V) f.

Lemma derive1n0 V (f : R → V) : f ^`(0) = f.

Lemma derive1n1 V (f : R → V) : f ^`(1) = f ^`().

Lemma derive1nS V (f : R → V) n : f ^`(n.+1) = f ^`(n )^`().

Lemma derive1Sn V (f : R → V) n : f ^`(n.+1) = f ^`()^`(n ).

End DifferentialR2.

Notation "f ^` ()" := (derive1 f).
Notation "f ^` ( n )" := (derive1n n f).

Section DifferentialR3.
Variable R : numFieldType.

Fact dcst (V W : normedModType R) (a : W) (x : V) : continuous (0 : V → W) ∧
  cst a \o shift x = cst (cst a x) + \0 +o_ (0 : V ) id.

Variables (V W : normedModType R).

Fact dadd (f g : V → W) x :
  differentiable f x → differentiable g x →
  continuous ('d f x \+ 'd g x) ∧
  (f + g ) \o shift x = cst ((f + g) x) + ('d f x \+ 'd g x) +o_ (0 : V ) id.

Fact dopp (f : V → W) x :
  differentiable f x → continuous (- ('d f x : V → W)) ∧
  (- f ) \o shift x = cst (- f x) \- 'd f x +o_ (0 : V ) id.

Lemma is_diff_eq (V' W' : normedModType R) (f f' g : V' → W') (x : V') :
  is_diff x f f' → f' = g → is_diff x f g.

Fact dscale (f : V → W) k x :
  differentiable f x → continuous (k \*: 'd f x) ∧
  (k *: f ) \o shift x = cst ((k *: f) x) + k \*: 'd f x +o_ (0 : V ) id.

NB: could be generalized with K : absRingType instead of R; DONE?

Fact dscalel (k : V → R) (f : W) x :
  differentiable k x →
  continuous (fun z : V ⇒ 'd k x z *: f) ∧
  (fun z ⇒ k z *: f ) \o shift x =
    cst (k x *: f) + (fun z ⇒ 'd k x z *: f) +o_ (0 : V ) id.

Fact dlin (V' W' : normedModType R) (f : {linear V' → W'}) x :
  continuous f → f \o shift x = cst (f x) + f +o_ (0 : V') id.

TODO: generalize

fixme using (1 / (h + x) - 1 / x) / h = - 1 / (h + x) x = -1/x^2 + o(1)

Fact dinv (x : R) :
  x != 0 → continuous (fun h : R ⇒ - x ^- 2 *: h) ∧
  (fun x ⇒ x^-1)%R \o shift x = cst (x^-1)%R +
  (fun h : R ⇒ - x ^- 2 *: h) +o_ (0 : R ) id.

Lemma diff_Rinv (x : R) : x != 0 →
  'd GRing.inv x = (fun h : R ⇒ - x ^- 2 *: h ) :> (R → R ).

Lemma differentiable_Rinv (x : R) : x != 0 →
  differentiable (GRing.inv : R → R) x.

Lemma diffV (f : V → R) x : differentiable f x → f x != 0 →
  'd (fun y ⇒ (f y)^-1) x = - (f x) ^- 2 \*: 'd f x :> (V → R ).

Lemma differentiableV (f : V → R) x :
  differentiable f x → f x != 0 → differentiable (fun y ⇒ (f y)^-1) x.

Global Instance is_diffX (f df : V → R) n x :
  is_diff x f df → is_diff x (f ^+ n .+1) (n .+1%:R × f x ^+ n *: df ).

Lemma differentiableX (f : V → R) n x :
  differentiable f x → differentiable (f ^+ n.+1) x.

Lemma diffX (f : V → R) n x :
  differentiable f x →
  'd (f ^+ n.+1) x = n.+1%:R × f x ^+ n \*: 'd f x :> (V → R ).

End DifferentialR3_numFieldType.

Section DeriveRU.
Variables (R : numFieldType) (U : normedModType R).
Implicit Types f : R → U.

Let der1 f x : derivable f x 1 →
  f \o shift x = cst (f x) + ( *:%R^~ (f ^`() x )) +o_ (0 : R ) id.

Lemma deriv1E f x : derivable f x 1 → 'd f x = ( *:%R^~ (f ^`() x )) :> (R → U ).

Lemma diff1E f x :
  differentiable f x → 'd f x = (fun h ⇒ h *: f ^`() x ) :> (R → U ).

Lemma derivable1_diffP f x : derivable f x 1 ↔ differentiable f x.

Lemma derivable_within_continuous f (i : interval R) :
  {in i , ∀ x, derivable f x 1} → {within [set ` i ], continuous f }.

End DeriveRU.

Section DeriveVW.
Variables (R : numFieldType) (V W : normedModType R).
Implicit Types f : V → W.

Lemma derivable1P f x v :
  derivable f x v ↔ derivable (fun h : R ⇒ f (h *: v + x)) 0 1.

Lemma derivableP f x v : derivable f x v → is_derive x v f ('D_v f x).

Lemma diff_derivable f a v : differentiable f a → derivable f a v.

Global Instance is_derive_cst (a : W) (x v : V) : is_derive x v (cst a) 0.

Lemma is_derive_eq f (x v : V) (df f' : W) :
  is_derive x v f f' → f' = df → is_derive x v f df.

End DeriveVW.

Section Derive_lemmasVW.
Variables (R : numFieldType) (V W : normedModType R).
Implicit Types f g : V → W.

Fact der_add f g (x v : V) : derivable f x v → derivable g x v →
  (fun h ⇒ h^-1 *: (((f + g ) \o shift x ) (h *: v ) - (f + g) x)) @
  0^' --> 'D_v f x + 'D_v g x.

Lemma deriveD f g (x v : V) : derivable f x v → derivable g x v →
  'D_v (f + g ) x = 'D_v f x + 'D_v g x.

Lemma derivableD f g (x v : V) :
  derivable f x v → derivable g x v → derivable (f + g) x v.

Global Instance is_deriveD f g (x v : V) (df dg : W) :
  is_derive x v f df → is_derive x v g dg → is_derive x v (f + g) (df + dg).

Global Instance is_derive_sum n (h : 'I_n → V → W) (x v : V)
  (dh : 'I_n → W) : (∀ i, is_derive x v (h i) (dh i)) →
  is_derive x v (\sum_(i < n) h i) (\sum_(i < n) dh i).

Lemma derivable_sum n (h : 'I_n → V → W) (x v : V) :
  (∀ i, derivable (h i) x v ) → derivable (\sum_(i < n) h i) x v.

Lemma derive_sum n (h : 'I_n → V → W) (x v : V) :
  (∀ i, derivable (h i) x v ) →
  'D_v (\sum_(i < n) h i ) x = \sum_(i < n) 'D_v (h i ) x.

Fact der_opp f (x v : V) : derivable f x v →
  (fun h ⇒ h^-1 *: (((- f ) \o shift x ) (h *: v ) - (- f) x)) @
  0^' --> - 'D_v f x.

Lemma deriveN f (x v : V) : derivable f x v →
  'D_v (- f ) x = - 'D_v f x.

Lemma derivableN f (x v : V) :
  derivable f x v → derivable (- f) x v.

Global Instance is_deriveN f (x v : V) (df : W) :
  is_derive x v f df → is_derive x v (- f) (- df).

Global Instance is_deriveB f g (x v : V) (df dg : W) :
  is_derive x v f df → is_derive x v g dg → is_derive x v (f - g) (df - dg).

Lemma deriveB f g (x v : V) : derivable f x v → derivable g x v →
  'D_v (f - g ) x = 'D_v f x - 'D_v g x.

Lemma derivableB f g (x v : V) :
  derivable f x v → derivable g x v → derivable (f - g) x v.

Fact der_scal f (k : R) (x v : V) : derivable f x v →
  (fun h ⇒ h^-1 *: ((k \*: f \o shift x ) (h *: v ) - (k \*: f) x)) @
  (0 : R )^' --> k *: 'D_v f x.

Lemma deriveZ f (k : R) (x v : V) : derivable f x v →
  'D_v (k \*: f ) x = k *: 'D_v f x.

Lemma derivableZ f (k : R) (x v : V) :
  derivable f x v → derivable (k \*: f) x v.

Global Instance is_deriveZ f (k : R) (x v : V) (df : W) :
  is_derive x v f df → is_derive x v (k \*: f) (k *: df).

End Derive_lemmasVW.

Section Derive_lemmasVR.
Variables (R : numFieldType) (V : normedModType R).
Implicit Types f g : V → R.

Fact der_mult f g (x v : V) :
  derivable f x v → derivable g x v →
  (fun h ⇒ h^-1 *: (((f × g ) \o shift x ) (h *: v ) - (f × g) x)) @
  (0 : R )^' --> f x *: 'D_v g x + g x *: 'D_v f x.

Lemma deriveM f g (x v : V) : derivable f x v → derivable g x v →
  'D_v (f × g ) x = f x *: 'D_v g x + g x *: 'D_v f x.

Lemma derivableM f g (x v : V) :
  derivable f x v → derivable g x v → derivable (f × g) x v.

Global Instance is_deriveM f g (x v : V) (df dg : R) :
  is_derive x v f df → is_derive x v g dg →
  is_derive x v (f × g) (f x *: dg + g x *: df).

Global Instance is_deriveX f n (x v : V) (df : R) :
  is_derive x v f df → is_derive x v (f ^+ n.+1) ((n.+1%:R × f x ^+n) *: df).

Lemma derivableX f n (x v : V) : derivable f x v → derivable (f ^+ n.+1) x v.

Lemma deriveX f n (x v : V) : derivable f x v →
  'D_v (f ^+ n.+1) x = (n.+1%:R × f x ^+ n) *: 'D_v f x.

Fact der_inv f (x v : V) : f x != 0 → derivable f x v →
  (fun h ⇒ h^-1 *: (((fun y ⇒ (f y)^-1) \o shift x ) (h *: v ) - (f x)^-1)) @
  (0 : R )^' --> - (f x) ^-2 *: 'D_v f x.

Lemma deriveV f x v : f x != 0 → derivable f x v →
  'D_v (fun y ⇒ (f y)^-1) x = - (f x) ^- 2 *: 'D_v f x.

Lemma derivableV f (x v : V) :
  f x != 0 → derivable f x v → derivable (fun y ⇒ (f y)^-1) x v.

Lemma derive1_cst (k : V) t : (cst k )^`() t = 0.

End Derive_lemmasVR.

Lemma EVT_max (R : realType) (f : R → R) (a b : R) : (* TODO : Filter not infered *)
  a ≤ b → {within `[a , b ], continuous f } → exists2 c , c \in `[a, b]%R &
  ∀ t, t \in `[a, b]%R → f t ≤ f c.

Lemma EVT_min (R : realType) (f : R → R) (a b : R) :
  a ≤ b → {within `[a , b ], continuous f } → exists2 c , c \in `[a, b]%R &
  ∀ t, t \in `[a, b]%R → f c ≤ f t.

Lemma cvg_at_rightE (R : numFieldType) (V : normedModType R) (f : R → V) x :
  cvg (f @ x ^') → lim (f @ x ^') = lim (f @ at_right x).
Arguments cvg_at_rightE {R V} f x.

Lemma cvg_at_leftE (R : numFieldType) (V : normedModType R) (f : R → V) x :
  cvg (f @ x ^') → lim (f @ x ^') = lim (f @ at_left x).
Arguments cvg_at_leftE {R V} f x.

Lemma __deprecated__le0r_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
  (FF : ProperFilter F) (f : T → R) :
  (\∀ x \near F , 0 ≤ f x ) → cvg (f @ F) → 0 ≤ lim (f @ F).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="generalized by `limr_ge`")]
Notation le0r_cvg_map := __deprecated__le0r_cvg_map.

Lemma __deprecated__ler0_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
  (FF : ProperFilter F) (f : T → R) :
  (\∀ x \near F , f x ≤ 0) → cvg (f @ F) → lim (f @ F) ≤ 0.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="generalized by `limr_le`")]
Notation ler0_cvg_map := __deprecated__ler0_cvg_map.

Lemma __deprecated__ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
    (FF : ProperFilter F) (f g : T → R) :
  (\∀ x \near F , f x ≤ g x ) → cvg (f @ F) → cvg (g @ F) →
  lim (f @ F) ≤ lim (g @ F).
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="subsumed by `ler_lim`")]
Notation ler_cvg_map := __deprecated__ler_cvg_map.

Lemma derive1_at_max (R : realFieldType) (f : R → R) (a b c : R) :
  a ≤ b → (∀ t, t \in `]a, b[%R → derivable f t 1) → c \in `]a, b[%R →
  (∀ t, t \in `]a, b[%R → f t ≤ f c ) → is_derive c 1 f 0.

Lemma derive1_at_min (R : realFieldType) (f : R → R) (a b c : R) :
  a ≤ b → (∀ t, t \in `]a, b[%R → derivable f t 1) → c \in `]a, b[%R →
  (∀ t, t \in `]a, b[%R → f c ≤ f t ) → is_derive c 1 f 0.

Lemma Rolle (R : realType) (f : R → R) (a b : R) :
  a < b → (∀ x, x \in `]a, b[%R → derivable f x 1) →
  {within `[a , b ], continuous f } → f a = f b →
  exists2 c , c \in `]a, b[%R & is_derive c 1 f 0.

Lemma MVT (R : realType) (f df : R → R) (a b : R) :
  a < b → (∀ x, x \in `]a, b[%R → is_derive x 1 f (df x)) →
  {within `[a , b ], continuous f } →
  exists2 c , c \in `]a, b[%R & f b - f a = df c × (b - a).

Weakens MVT to work when the interval is a single point.

Lemma MVT_segment (R : realType) (f df : R → R) (a b : R) :
  a ≤ b → (∀ x, x \in `]a, b[%R → is_derive x 1 f (df x)) →
  {within `[a , b ], continuous f } →
  exists2 c , c \in `[a, b]%R & f b - f a = df c × (b - a).

Lemma ler0_derive1_nincr (R : realType) (f : R → R) (a b : R) :
  (∀ x, x \in `]a, b[%R → derivable f x 1) →
  (∀ x, x \in `]a, b[%R → f ^`() x ≤ 0) →
  {within `[a ,b ], continuous f } →
  ∀ x y, a ≤ x → x ≤ y → y ≤ b → f y ≤ f x.

Lemma le0r_derive1_ndecr (R : realType) (f : R → R) (a b : R) :
  (∀ x, x \in `]a, b[%R → derivable f x 1) →
  (∀ x, x \in `]a, b[%R → 0 ≤ f ^`() x ) →
  {within `[a ,b ], continuous f } →
  ∀ x y, a ≤ x → x ≤ y → y ≤ b → f x ≤ f y.

Lemma derive1_comp (R : realFieldType) (f g : R → R) x :
  derivable f x 1 → derivable g (f x) 1 →
  (g \o f )^`() x = g ^`() (f x ) × f ^`() x.

Section is_derive_instances.
Variables (R : numFieldType) (V : normedModType R).

Lemma derivable_cst (x : V) : derivable (fun ⇒ x) 0 1.

Lemma derivable_id (x v : V) : derivable id x v.

Global Instance is_derive_id (x v : V) : is_derive x v id v.

Global Instance is_deriveNid (x v : V) : is_derive x v -%R (- v).

End is_derive_instances.

Trick to trigger type class resolution

Lemma trigger_derive (R : realType) (f : R → R) x x1 y1 :
is_derive x 1 f x1 → x1 = y1 → is_derive x 1 f y1.