## Stream: Coq users

### Topic: How can I define ODE (ordinary differential equation)?

#### Lessness (Oct 24 2021 at 16:59):

Is there some way to define structure for (implicit) general ODE of nth order in Coq?
I tried to google, but I haven't found anything for now.

#### Lessness (Oct 24 2021 at 18:08):

Using total functions for now, I got to this:

``````Require Import Reals Utf8.
Set Implicit Arguments.
Open Scope R.

Fixpoint type_pow (n: nat) (x: Type): Type :=
match n with
| O => x
| S m => prod (type_pow m x) x
end.

Definition derivative (i: nat): (R -> R) -> (R -> R).

Definition implicit_general_ODE (n: nat): (type_pow (S (S n)) R -> R) -> (R -> R) -> Prop.
Proof.
intros F x. refine (∀ (t: R), _: Prop).
induction n.
+ simpl in *. exact (F (t, x t, (derivative 1%nat x) t) = 0).
+ simpl in *. pose ((derivative (S (S n)) x) t) as x'. exact (IHn (λ t, F (t, x'))).
Defined.

Definition test: type_pow 3%nat R -> R.
Proof.
intros [[[x y] z] w]. simpl in *. exact (x + y + z + w).
Defined.

Eval compute in (implicit_general_ODE test).
``````

#### Karl Palmskog (Oct 24 2021 at 18:13):

for ODEs in Coq, you have at least this paper which talks about this code in the CoRN library

Last updated: Oct 04 2023 at 19:01 UTC