move is_deriveV and is_derive1_comp to derive.v

CHANGELOG_UNRELEASED.md

@@ -354,6 +354,9 @@
 - in `classical_sets.v`
   + lemma `bigcupDr` -> `setD_bigcupr` (deprecating `bigcupDr`)
 
+- moved from `realfun.v` to `derive.v` and generalized:
+  + lemmas `is_deriveV`, `is_derive1_comp`
+
 ### Renamed
 
 - in `tvs.v`:

theories/derive.v

@@ -1287,7 +1287,7 @@ by apply/funext => x; rewrite derive1E deriveB// derive_id derive_cst sub0r.
 Qed.
 
 Section Derive_lemmasVR.
-Variables (R : numFieldType) (V : normedModType R).
+Context {R : numFieldType} {V : normedModType R}.
 Implicit Types (f g : V -> R) (x v : V).
 
 Fact der_mult f g x v :
@@ -1398,8 +1398,19 @@ move=> df dg; apply/cvg_ex; exists (- (f x) ^- 2 *: 'D_v f x).
 exact: der_inv.
 Qed.
 
+Lemma is_deriveV f x v (df : R) :
+  f x != 0 -> is_derive x v f df ->
+  is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: df).
+Proof.
+move=> fxNZ Df; apply: DeriveDef; first exact: derivableV.
+by rewrite deriveV//; case: Df => _ ->.
+Qed.
+
 End Derive_lemmasVR.
 
+#[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
+  (apply: is_deriveV; first by []) : typeclass_instances.
+
 Lemma derive_shift {R : numFieldType} (v k : R) :
   'D_v (shift k : R -> R) = cst v.
 Proof.
@@ -2068,6 +2079,15 @@ rewrite diff_comp // !derive1E' //= -[X in 'd  _ _ X = _]mulr1.
 by rewrite [LHS]linearZ mulrC.
 Qed.
 
+Global Instance is_derive1_comp (R : realFieldType) (f g : R -> R) (x a b : R) :
+  is_derive (g x) 1 f a -> is_derive x 1 g b -> is_derive x 1 (f \o g) (a * b).
+Proof.
+move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)).
+  apply/derivable1_diffP/differentiable_comp; first exact/derivable1_diffP.
+  by move/derivable1_diffP in fgxv.
+by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E.
+Qed.
+
 Lemma near_eq_growth_rate (R : numFieldType) (V W : normedModType R)
     (f g : V -> W) (a v : V) : {near a, f =1 g} ->
    \forall h \near 0,

theories/realfun.v

@@ -1872,25 +1872,6 @@ apply/continuous_subspaceT=> r.
 exact/differentiable_continuous/derivable1_diffP.
 Qed.
 
-Global Instance is_derive1_comp (f g : R -> R) (x a b : R) :
-  is_derive (g x) 1 f a -> is_derive x 1 g b ->
-  is_derive x 1 (f \o g) (a * b).
-Proof.
-move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)).
-  apply/derivable1_diffP/differentiable_comp; first exact/derivable1_diffP.
-  by move/derivable1_diffP in fgxv.
-by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E.
-Qed.
-
-Lemma is_deriveV (f : R -> R) (x t v : R) :
-  f x != 0 -> is_derive x v f t ->
-  is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: t).
-Proof.
-move=> fxNZ Df.
-constructor; first by apply: derivableV => //; case: Df.
-by rewrite deriveV //; case: Df => _ ->.
-Qed.
-
 Lemma is_derive_inverse (f g : R -> R) l x :
   {near x, cancel f g}  ->
   {near x, continuous f}  ->
@@ -1950,9 +1931,6 @@ Lemma derive_sqrt {K : realType} (r : K) : 0 < r ->
   'D_1 Num.sqrt r = (2 * Num.sqrt r)^-1.
 Proof. by move=> r0; exact/derive_val/is_derive1_sqrt. Qed.
 
-#[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
-  (eapply is_deriveV; first by []) : typeclass_instances.
-
 Section total_variation_realFieldType.
 Context {R : realFieldType}.
 Implicit Types (a b : R) (f : R -> R).