Search code examples
coq

Differential calculus on Coq

I want to reperesent the exact value of differential calculus on Coq, not approximation.

I defined the inductive type represents the differentiation of the real number as you can see below.

Require Import Coq.Reals.Reals.

Inductive myR:=
| mR : R -> myR 
| Diff : myR -> myR.

This is not interesting. Do you know a better way?

Solution

  • In Coquelicot, Derive is defined as

    Definition Derive (f : R → R) (x : R) := real (Lim (fun h ⇒ (f (x+h) - f x)/h) 0).