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.

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).
Proof. Admitted.
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).
```

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

Last updated: Jun 20 2024 at 11:02 UTC