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: Feb 01 2023 at 13:03 UTC