From 6df3c56dad2fc3ceb5c1a357038ec3d80a7f0f4d Mon Sep 17 00:00:00 2001 From: Lynda Date: Mon, 27 Jul 2026 17:23:07 +0200 Subject: [PATCH 1/8] documentation --- theories/derive.v | 57 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/theories/derive.v b/theories/derive.v index aadc6c86c9..d6e1ae9ffa 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -28,6 +28,10 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* and R : numFieldType *) (* f^`() == the derivative of f of domain R *) (* f^`(n) == the nth derivative of f of domain R *) +(* is_derive x v f df == the derivative of a function f at point x along v *) +(* is df and f is derivable at x along v *) +(* is_diff x f df == the differential of a function f at point x is df *) +(* and f is differentiable at point x *) (* ``` *) (* *) (* Naming convention in this file: *) @@ -40,6 +44,59 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* (e.g., `derive1_cst`, `derive1_comp`) *) (* - lemmas of the form `... -> is_derive x v f df` are named `is_derive*` *) (* (e.g., `is_derive_cst`) *) +(* - lemmas of the form `... -> is_diff x f df` are named `is_diff*` *) +(* (e.g., `is_diff_cst`) *) +(* *) +(* # Automatic derivation and differentiation with `is_diff _` and *) +(* `is_derive _` *) +(* *) +(* Statements of the form `is_diff _` and `is_derive _` are typeclasses *) +(* registered via `Instance` declarations with a proof `ex_derive`/`ex_diff *) +(* of derivability/differentiability of the expression and a proof *) +(* `derive_val`/`diff_val` of the value of the derivative/differential *) +(* of the function ; so that typeclass resolution can automatically synthesize*) +(* the differential/derivative of a compound expression from the *) +(* differentials/derivatives of its parts, instead of requiring the user to *) +(* prove and compute derivatives by hand. *) +(* *) +(* ## Lemmas of the form `is_derive _` and `is_diff _` *) +(* *) +(* For a compound expression, e.g. built from f and g, state the goal with the*) +(* expected derivative/differential and let typeclass resolution fill the *) +(* proof by `apply: is_derive_eq / is_diff_eq.` : *) +(* `Lemma is_derive_example (W : normedModType R) *) +(* (t : R^o) (f g : R^o -> W) (f' g' : W) v : *) +(* is_derive t v f f' -> *) +(* is_derive t v g g' -> *) +(* is_derive t v (f + g) (f'+g'). *) +(* Proof. move => is_der_f is_der_g. by apply: is_derive_eq. Qed.` *) +(* *) +(* The proof is inferred structurally by chaining declared `is_derive _` or *) +(* `is_diff _` instances matching the pattern of the goal stated. *) +(* *) +(* To verify if a given expression is derivable or differentiable, you can use*) +(* `apply: ex_derive. or `apply: ex_diff`, given the right *) +(* `is_derive _` or `is_diff _` instances are defined such as : *) +(* Hypothesis derivable_f : forall t, derivable f t 1. *) +(* Hypothesis derivable_h : forall t, derivable h t 1. *) +(* Local Instance is_derive_f t : is_derive t 1 f ('D_1 f t). *) +(* by apply: derivableP. Qed. *) +(* Local Instance is_derive_h t : is_derive t 1 h ('D_1 h t). *) +(* by apply: derivableP. Qed. *) +(* *) +(* Lemma is_derivable_example (t : R^o) : derivable (f+h) t 1. *) +(* Proof. apply/ex_derive. Qed. *) +(* *) +(* To verify the value of a given function you can apply `derive_val` or *) +(* diff_val`, given the right `is_derive/diff` instances are defined such as :*) +(* *) +(* Lemma is_derive_val_example t : *) +(* 'D_1 (f + h) t = ('D_1 f t) + ('D_1 h t). Proof. by apply/derive_val. Qed. *) +(* *) +(* It is worth mentioning that every differentiable function is derivable *) +(* via the lemma `diff_derivable` and that a function is differentiable iff *) +(* it is derivable in the case of functions from R to a normed module, *) +(* via the lemma `derivable1_diffP`. *) (* *) (******************************************************************************) From 87fea6200da7ac7bf9ee3a5ce71e8d55070543b0 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 28 Jul 2026 23:42:23 +0900 Subject: [PATCH 2/8] Apply suggestion from @affeldt-aist --- theories/derive.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/derive.v b/theories/derive.v index d6e1ae9ffa..f0db3c7d21 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -31,7 +31,7 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* is_derive x v f df == the derivative of a function f at point x along v *) (* is df and f is derivable at x along v *) (* is_diff x f df == the differential of a function f at point x is df *) -(* and f is differentiable at point x *) +(* and f is differentiable at point x *) (* ``` *) (* *) (* Naming convention in this file: *) From 2ee8ca95dec5911fa755db9279498c6934da809c Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 28 Jul 2026 23:43:13 +0900 Subject: [PATCH 3/8] Apply suggestion from @affeldt-aist --- theories/derive.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/derive.v b/theories/derive.v index f0db3c7d21..3200c7ec94 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -54,7 +54,7 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* registered via `Instance` declarations with a proof `ex_derive`/`ex_diff *) (* of derivability/differentiability of the expression and a proof *) (* `derive_val`/`diff_val` of the value of the derivative/differential *) -(* of the function ; so that typeclass resolution can automatically synthesize*) +(* of the function; so that typeclass resolution can automatically synthesize *) (* the differential/derivative of a compound expression from the *) (* differentials/derivatives of its parts, instead of requiring the user to *) (* prove and compute derivatives by hand. *) From ded3c441a278a84f7df70fab35c6ed152f989eed Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 28 Jul 2026 23:44:33 +0900 Subject: [PATCH 4/8] Apply suggestion from @affeldt-aist --- theories/derive.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index 3200c7ec94..17bf78216c 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -61,8 +61,8 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* *) (* ## Lemmas of the form `is_derive _` and `is_diff _` *) (* *) -(* For a compound expression, e.g. built from f and g, state the goal with the*) -(* expected derivative/differential and let typeclass resolution fill the *) +(* For a compound expression, e.g., built from f and g, state the goal with *) +(* the expected derivative/differential and let typeclass resolution fill the *) (* proof by `apply: is_derive_eq / is_diff_eq.` : *) (* `Lemma is_derive_example (W : normedModType R) *) (* (t : R^o) (f g : R^o -> W) (f' g' : W) v : *) From 03cbdd7c53f9a0fbf35f0b1d590e1d939f38b3f9 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 28 Jul 2026 23:45:52 +0900 Subject: [PATCH 5/8] Apply suggestion from @affeldt-aist --- theories/derive.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/derive.v b/theories/derive.v index 17bf78216c..fdb388b8f8 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -63,7 +63,7 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* *) (* For a compound expression, e.g., built from f and g, state the goal with *) (* the expected derivative/differential and let typeclass resolution fill the *) -(* proof by `apply: is_derive_eq / is_diff_eq.` : *) +(* proof by `apply: is_derive_eq / is_diff_eq.`: *) (* `Lemma is_derive_example (W : normedModType R) *) (* (t : R^o) (f g : R^o -> W) (f' g' : W) v : *) (* is_derive t v f f' -> *) From c4272a769c73474868611f49f7f5ec13383d21dc Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 28 Jul 2026 23:46:47 +0900 Subject: [PATCH 6/8] Apply suggestion from @affeldt-aist --- theories/derive.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/derive.v b/theories/derive.v index fdb388b8f8..0a114fa972 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -68,7 +68,7 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* (t : R^o) (f g : R^o -> W) (f' g' : W) v : *) (* is_derive t v f f' -> *) (* is_derive t v g g' -> *) -(* is_derive t v (f + g) (f'+g'). *) +(* is_derive t v (f + g) (f' + g'). *) (* Proof. move => is_der_f is_der_g. by apply: is_derive_eq. Qed.` *) (* *) (* The proof is inferred structurally by chaining declared `is_derive _` or *) From 1399843e2a9adafa65451e737fa35e32f0bbf6ff Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 28 Jul 2026 23:48:09 +0900 Subject: [PATCH 7/8] Apply suggestion from @affeldt-aist --- theories/derive.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/derive.v b/theories/derive.v index 0a114fa972..75d3ba8737 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -75,7 +75,7 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* `is_diff _` instances matching the pattern of the goal stated. *) (* *) (* To verify if a given expression is derivable or differentiable, you can use*) -(* `apply: ex_derive. or `apply: ex_diff`, given the right *) +(* `apply: ex_derive` or `apply: ex_diff`, given the right *) (* `is_derive _` or `is_diff _` instances are defined such as : *) (* Hypothesis derivable_f : forall t, derivable f t 1. *) (* Hypothesis derivable_h : forall t, derivable h t 1. *) From 9c92eba31cc203554a7493d22a57840f5b9b38dc Mon Sep 17 00:00:00 2001 From: Lynda Date: Tue, 28 Jul 2026 17:29:36 +0200 Subject: [PATCH 8/8] triple backquotes --- theories/derive.v | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index 75d3ba8737..12b8c3feee 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -64,12 +64,12 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* For a compound expression, e.g., built from f and g, state the goal with *) (* the expected derivative/differential and let typeclass resolution fill the *) (* proof by `apply: is_derive_eq / is_diff_eq.`: *) -(* `Lemma is_derive_example (W : normedModType R) *) +(* ```Lemma is_derive_example (W : normedModType R) *) (* (t : R^o) (f g : R^o -> W) (f' g' : W) v : *) (* is_derive t v f f' -> *) (* is_derive t v g g' -> *) (* is_derive t v (f + g) (f' + g'). *) -(* Proof. move => is_der_f is_der_g. by apply: is_derive_eq. Qed.` *) +(* Proof. move => is_der_f is_der_g. by apply: is_derive_eq. Qed.``` *) (* *) (* The proof is inferred structurally by chaining declared `is_derive _` or *) (* `is_diff _` instances matching the pattern of the goal stated. *) @@ -77,7 +77,7 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* To verify if a given expression is derivable or differentiable, you can use*) (* `apply: ex_derive` or `apply: ex_diff`, given the right *) (* `is_derive _` or `is_diff _` instances are defined such as : *) -(* Hypothesis derivable_f : forall t, derivable f t 1. *) +(* ```Hypothesis derivable_f : forall t, derivable f t 1. *) (* Hypothesis derivable_h : forall t, derivable h t 1. *) (* Local Instance is_derive_f t : is_derive t 1 f ('D_1 f t). *) (* by apply: derivableP. Qed. *) @@ -85,13 +85,14 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (* by apply: derivableP. Qed. *) (* *) (* Lemma is_derivable_example (t : R^o) : derivable (f+h) t 1. *) -(* Proof. apply/ex_derive. Qed. *) +(* Proof. apply/ex_derive. Qed.``` *) (* *) (* To verify the value of a given function you can apply `derive_val` or *) (* diff_val`, given the right `is_derive/diff` instances are defined such as :*) (* *) -(* Lemma is_derive_val_example t : *) -(* 'D_1 (f + h) t = ('D_1 f t) + ('D_1 h t). Proof. by apply/derive_val. Qed. *) +(* ```Lemma is_derive_val_example t : *) +(* 'D_1 (f + h) t = ('D_1 f t) + ('D_1 h t). *) +(* Proof. by apply/derive_val. Qed.``` *) (* *) (* It is worth mentioning that every differentiable function is derivable *) (* via the lemma `diff_derivable` and that a function is differentiable iff *)