Stream: Coq users

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

view this post on Zulip 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.

view this post on Zulip 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

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.
  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'))).

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

Eval compute in (implicit_general_ODE test).

view this post on Zulip 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: Jun 20 2024 at 11:02 UTC