fact: Definition diff_operations A (ops : @operations A) := Build_operations (fun x => (constant ops x, constant ops 0)) (unknown ops, unknown ops) (fun o x => match x with | (v, d) => match o with | Neg => let f := unary ops Neg in (f v, f d) | Abs => let w := unary ops Abs v in (w, match sign ops v with Xlt => unary ops Neg d | Xgt => d | _ => unknown ops end) | Inv => let w := unary ops Inv v in (w, binary ops Mul d (unary ops Neg (unary ops Sqr w))) | Sqr => let w := binary ops Mul d v in (unary ops Sqr v, binary ops Add w w) | Sqrt => let w := unary ops Sqrt v in (w, binary ops Div d (binary ops Add w w)) | Cos => (unary ops Cos v, binary ops Mul d (unary ops Neg (unary ops Sin v))) | Sin => (unary ops Sin v, binary ops Mul d (unary ops Cos v)) | Tan => let w := unary ops Tan v in (w, binary ops Mul d (binary ops Add (constant ops 1) (unary ops Sqr w))) | Atan => (unary ops Atan v, binary ops Div d (binary ops Add (constant ops 1) (unary ops Sqr v))) | Exp => let w := unary ops Exp v in (w, binary ops Mul d w) | Ln => (unary ops Ln v, match sign ops v with Xgt => binary ops Div d v | _ => unknown ops end) | PowerInt n => (unary ops o v, binary ops Mul d (binary ops Mul (constant ops n) (unary ops (PowerInt (n-1)) v))) | Nearbyint m => (unary ops (Nearbyint m) v, unknown ops) | RoundFlt m emin prec => (unary ops (RoundFlt m emin prec) v, unknown ops) | ErrorFlt m emin prec => (unary ops (ErrorFlt m emin prec) v, unknown ops) | RoundFix m emin => (unary ops (RoundFix m emin) v, unknown ops) | ErrorFix m emin => (unary ops (ErrorFix m emin) v, unknown ops) end end) (fun o x y => match x, y with | (vx, dx), (vy, dy) => match o with | Add => let f := binary ops Add in (f vx vy, f dx dy) | Sub => let f := binary ops Sub in (f vx vy, f dx dy) | Mul => let f := binary ops Mul in (f vx vy, binary ops Add (f dx vy) (f dy vx)) | Div => let f := binary ops Div in let w := f vx vy in (w, f (binary ops Sub dx (binary ops Mul dy w)) vy) end end) (fun x => match x with (vx, _) => sign ops vx end).
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog