Skip to content

Documentation differentiation #2053

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
yosakaon wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Documentation differentiation #2053

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 57 additions & 0 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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: *)
Expand All @@ -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`. *)
(* *)
(******************************************************************************)

Expand Down
Loading