fact: Fixpoint D (e : expr) n {struct e} : expr * domain := match e with | Var v => (if ssrnat.eqn v n then Cst 1 else Cst 0, Always) | Cst _ => (Cst 0, Always) | AppExt k f le => let lnc := index_not_const le n in let ld := map (fun e => D e n) le in match lnc with | nil => (Cst 0, Always) | v :: nil => let '(d1,d2) := nth (Cst 0,Never) ld v in (Binary Emult d1 (AppExtD k f v le), And (Derivable v k f le :: d2 :: nil)) | v1 :: v2 :: nil => let '(d1,d2) := nth (Cst 0,Never) ld v1 in let '(d3,d4) := nth (Cst 0,Never) ld v2 in (Binary Eplus (Binary Emult d1 (AppExtD k f v1 le)) (Binary Emult d3 (AppExtD k f v2 le)), And (Derivable2 v1 v2 k f le :: d2 :: Derivable v2 k f le :: d4 :: nil)) | _ => (Cst 0, Never) end | AppExtD k f v le => (Cst 0, Never) | App f e => (Cst 0, Never) | Subst f e => (Cst 0, Never) | Binary b e1 e2 => let '(a1,b1) := D e1 n in let '(a2,b2) := D e2 n in match b, is_const e1 n, is_const e2 n with | Eplus, true, _ => (a2, b2) | Eplus, _, true => (a1, b1) | Eplus, _, _ => (Binary Eplus a1 a2, And (b1::b2::nil)) | Emult, true, _ => (Binary Emult e1 a2, b2) | Emult, _, true => (Binary Emult a1 e2, b1) | Emult, _, _ => (Binary Eplus (Binary Emult a1 e2) (Binary Emult e1 a2), And (b1::b2::nil)) end | Unary u e => let '(a,b) := D e n in match u with | Eopp => (Unary Eopp a, b) | Einv => (Binary Emult (Unary Eopp a) (Unary Einv (Binary Emult e e)), And (b:: (Partial (fun x => x <> 0) e) :: nil)) | Efct f f' H => (Binary Emult a (AppExt 1 f' [:: e]), b) | Efct' f f' df H => (Binary Emult a (AppExt 1 f' [:: e]), And (b :: (Partial df e) :: nil)) end | Int f e1 e2 => let '(a1,b1) := D e1 n in let '(a2,b2) := D e2 n in let '(a3,b3) := D f (S n) in match is_const f (S n), is_const e1 n, is_const e2 n with | true, true, _ => (Binary Emult a2 (App f e2), And (b2::(Integrable f e1 e2)::(Forone e2 (Locally 0 (Continuous 0 f)))::nil)) | true, false, true => (Unary Eopp (Binary Emult a1 (App f e1)), And (b1::(Integrable f e1 e2)::(Forone e1 (Locally 0 (Continuous 0 f)))::nil)) | true, false, false => (Binary Eplus (Binary Emult a2 (App f e2)) (Unary Eopp (Binary Emult a1 (App f e1))), And (b1::b2::(Integrable f e1 e2)::(Forone e1 (Locally 0 (Continuous 0 f)))::(Forone e2 (Locally 0 (Continuous 0 f)))::nil)) | false, true, true => (Int a3 e1 e2, And ((ForallWide n e1 e2 b3)::(Locally n (Integrable f e1 e2)):: (Forall e1 e2 (Continuous2 (S n) 0 a3))::nil)) | false, false, true => (Binary Eplus (Unary Eopp (Binary Emult a1 (App f e1))) (Int a3 e1 e2), And ((Forone e1 (Locally2 (S n) 0 (Continuous2 (S n) 0 a3))):: (Forall e1 e2 (Continuous2 (S n) 0 a3)):: b1::(Forone e1 (Locally 0 (Continuous 0 f))):: ParamIntegrable n f e1 e2::LocallyParamIntegrable n f e1:: ForallWide n e1 e2 b3::nil)) | false, true, false => (Binary Eplus (Binary Emult a2 (App f e2)) (Int a3 e1 e2), And ((Forone e2 (Locally2 (S n) 0 (Continuous2 (S n) 0 a3))):: (Forall e1 e2 (Continuous2 (S n) 0 a3)):: b2::(Forone e2 (Locally 0 (Continuous 0 f))):: ParamIntegrable n f e1 e2::LocallyParamIntegrable n f e2:: ForallWide n e1 e2 b3::nil)) | false, false, false => (Binary Eplus (Binary Eplus (Binary Emult a2 (App f e2)) (Unary Eopp (Binary Emult a1 (App f e1)))) (Int a3 e1 e2), And ((Forone e1 (Locally2 (S n) 0 (Continuous2 (S n) 0 a3))):: (Forone e2 (Locally2 (S n) 0 (Continuous2 (S n) 0 a3))):: (Forall e1 e2 (Continuous2 (S n) 0 a3)):: b1::(Forone e1 (Locally 0 (Continuous 0 f))):: b2::(Forone e2 (Locally 0 (Continuous 0 f))):: ParamIntegrable n f e1 e2::LocallyParamIntegrable n f e1::LocallyParamIntegrable n f e2:: ForallWide n e1 e2 b3::nil)) end end.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct