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

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