Library Coqtail.Reals.Dequa.Dequa_def

Require Import Reals.
Require Import Rpser_def Rpser_sums Rpser_usual Rpser_derivative.
Require Import Rfunction_classes.
Require Import Nth_derivative_def.
Require Import Rfunction_def Functions.
Require Import Rsequence_def.
Require Import List.
Require Import Option.
Require Import Ass_handling.

Local Open Scope Rseq_scope.


Inductive side_equa : Set :=
    | cst : (r : R), side_equa
    | scal : (r : R) (s : side_equa), side_equa
    | y : (p : nat) (k : nat) (a : R), side_equa
    | opp : (s1 : side_equa), side_equa
    | min : (s1 s2 : side_equa), side_equa
    | plus : (s1 s2 : side_equa), side_equa
    | mult : (s1 s2 : side_equa), side_equa.

Definition diff_equa : Set := prod (side_equa) (side_equa).

Fixpoint interp_side_equa_in_N s (rho : list Rseq) : option Rseq :=
match s with
  | cst rReturn (constant_seq r)
  | scal r eBind (interp_side_equa_in_N e rho) (fun unReturn (r × un))
  | y i k aBind (nth_error rho i) (fun unReturn (An_expand (An_nth_deriv un k) a))
  | opp eBind (interp_side_equa_in_N e rho) (fun unReturn (- un))
  | min e1 e2Bind (interp_side_equa_in_N e1 rho) (fun un
                  Bind (interp_side_equa_in_N e2 rho) (fun vnReturn (un - vn)))
  | plus e1 e2Bind (interp_side_equa_in_N e1 rho) (fun un
                  Bind (interp_side_equa_in_N e2 rho) (fun vnReturn (un + vn)))
  | mult e1 e2Bind (interp_side_equa_in_N e1 rho) (fun un
                  Bind (interp_side_equa_in_N e2 rho) (fun vnReturn (un # vn)))
end.

Fixpoint interp_side_equa_in_R s (rho : list (sigT infinite_cv_radius)) : option (RR) :=
match s with
  | cst rReturn (fun _r)
  | scal r eBind (interp_side_equa_in_R e rho) (fun fReturn ((fun _r) × f)%F)
  | y i k aBind (nth_error rho i) (fun fReturn (fun xnth_derive (sum (projT1 f) (projT2 f))
                 (D_infty_Rpser (projT1 f) (projT2 f) k) (a × x)%R))
  | opp eBind (interp_side_equa_in_R e rho) (fun fReturn (- f)%F)
  | min e1 e2Bind (interp_side_equa_in_R e1 rho) (fun f
                  Bind (interp_side_equa_in_R e2 rho) (fun gReturn (f - g)%F))
  | plus e1 e2Bind (interp_side_equa_in_R e1 rho) (fun f
                  Bind (interp_side_equa_in_R e2 rho) (fun gReturn (f + g)%F))
  | mult e1 e2Bind (interp_side_equa_in_R e1 rho) (fun f
                  Bind (interp_side_equa_in_R e2 rho) (fun gReturn (f × g)%F))
end.

Definition Invalid_context := False.

Definition interp {A B : Type} (e : diff_equa) (rho : list A)
  (f : side_equalist Aoption B) (P : BBProp) :=
let (s1, s2) := e in
match (f s1 rho), (f s2 rho) with
  | Some b1, Some b2P b1 b2
  | _, _Invalid_context
end.

Implicit Arguments interp[A B].

Definition interp_in_N e rho : Prop :=
  interp e rho interp_side_equa_in_N Rseq_eq.

Definition interp_in_R e rho : Prop :=
  interp e rho interp_side_equa_in_R Rfun_eq.

Delimit Scope de_scope with de.

Bind Scope de_scope with diff_equa.
Bind Scope de_scope with side_equa.

Open Scope de_scope.

Notation "`c k" := (cst k) (at level 40) : de_scope.
Notation "- y" := (opp y) : de_scope.
Infix "×" := scal : de_scope.
Infix "+" := plus : de_scope.
Infix "×" := plus : de_scope.
Infix "-" := min : de_scope.
Infix ":=:" := (@pair side_equa side_equa) (at level 50): de_scope.

Notation "[| e |]N" := (interp_in_N e%de) (at level 69).
Notation "[| e |]R" := (interp_in_R e%de) (at level 69).