1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: DiffTactics2.v,v 1.1.1.1 2004/02/05 16:25:45 lionelm Exp $ *)
23 include "ftc/Differentiability.ma".
26 Section Automatizing_Continuity
29 alias id "a" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Continuity/a.var".
31 alias id "b" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Continuity/b.var".
33 inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_function.ind".
35 inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_to_pfunct.con".
37 inline procedural "cic:/CoRN/tactics/DiffTactics2/continuous_cont.con".
40 End Automatizing_Continuity
44 Ltac pfunct_to_cont a b f :=
46 | ([-C-]?X3) => constr:(cconst a b X3)
47 | FId => constr:(cid a b)
49 let t1 := pfunct_to_cont a b X3 with t2 := pfunct_to_cont a b X4 in
50 constr:(cplus a b t1 t2)
52 let t1 := pfunct_to_cont a b X3 in
55 let t1 := pfunct_to_cont a b X3 with t2 := pfunct_to_cont a b X4 in
56 constr:(cminus a b t1 t2)
58 let t1 := pfunct_to_cont a b X3 with t2 := pfunct_to_cont a b X4 in
59 constr:(cmult a b t1 t2)
61 let t := pfunct_to_cont a b X4 in
62 constr:(cscalmult a b X3 t)
64 let t1 := pfunct_to_cont a b X3 in
65 constr:(cnth a b t1 X4)
66 | (FAbs ?X3) => let t1 := pfunct_to_cont a b X3 in
71 | Hab:_,H:(Continuous_I (a:=a) (b:=b) ?X1 t) |- _ =>
72 constr:(hyp_c a b X1 t H)
73 | H:(Derivative_I (a:=a) (b:=b) ?X1 t ?X4) |- _ =>
74 constr:(hyp_d a b X1 t X4 H)
75 | H:(Derivative_I (a:=a) (b:=b) ?X1 ?X4 t) |- _ =>
76 constr:(hyp_d' a b X1 X4 t H)
77 | H:(Diffble_I (a:=a) (b:=b) ?X1 t) |- _ =>
78 constr:(hyp_diff a b X1 t H)
86 | |- (Continuous_I (a:=?X1) (b:=?X2) ?X4 ?X3) =>
87 let r := pfunct_to_cont X1 X2 X3 in
90 (apply Continuous_I_wd with (cont_to_pfunct a b r);
91 [ unfold cont_to_pfunct in |- * | apply continuous_cont ])
96 Section Automatizing_Derivatives
99 alias id "a" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Derivatives/a.var".
101 alias id "b" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Derivatives/b.var".
103 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_function.ind".
105 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_to_pfunct.con".
107 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_deriv.con".
109 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_restr.con".
111 inline procedural "cic:/CoRN/tactics/DiffTactics2/diffble_restr.con".
114 End Automatizing_Derivatives
118 Ltac pfunct_to_restr a b f :=
120 | ([-C-]?X3) => constr:(const a b X3)
121 | FId => constr:(id a b)
123 let t1 := pfunct_to_restr a b X3 with t2 := pfunct_to_restr a b X4 in
124 constr:(rplus a b t1 t2)
126 let t1 := pfunct_to_restr a b X3 in
129 let t1 := pfunct_to_restr a b X3 with t2 := pfunct_to_restr a b X4 in
130 constr:(rminus a b t1 t2)
132 let t1 := pfunct_to_restr a b X3 with t2 := pfunct_to_restr a b X4 in
133 constr:(rmult a b t1 t2)
135 let t := pfunct_to_restr a b X4 in
136 constr:(rscalmult a b X3 t)
138 let t1 := pfunct_to_restr a b X3 in
139 constr:(rnth a b t1 X4)
141 let t := constr:X3 in
143 | H:(Derivative_I (a:=a) (b:=b) ?X1 t ?X4) |- _ =>
144 constr:(hyp a b X1 t X4 H)
145 | H:(Diffble_I (a:=a) (b:=b) ?X1 t) |- _ => constr:(
154 | |- (Derivative_I (a:=?X1) (b:=?X2) _ ?X3 ?X4) =>
155 let r := pfunct_to_restr X1 X2 X3 in
156 (apply Derivative_I_wdl with (deriv_to_pfunct X1 X2 r);
157 [ unfold deriv_to_pfunct in |- *
158 | apply Derivative_I_wdr with (deriv_deriv X1 X2 r);
159 [ unfold deriv_deriv, deriv_to_pfunct in |- *
160 | apply deriv_restr ] ])
165 Ltac Differentiate :=
167 | |- (Diffble_I (a:=?X1) (b:=?X2) _ ?X3) =>
168 let r := pfunct_to_restr X1 X2 X3 in
169 (apply Diffble_I_wd with (deriv_to_pfunct X1 X2 r);
170 [ apply diffble_restr | unfold deriv_deriv, deriv_to_pfunct in |- * ])
175 Ltac derivative_of f :=
177 | ([-C-]?X3) => constr:([-C-]ZeroR)
178 | FId => constr:([-C-]OneR)
180 let t1 := derivative_of X3 with t2 := derivative_of X4 in
182 | ({--}?X3) => let t1 := derivative_of X3 in
185 let t1 := derivative_of X3 with t2 := derivative_of X4 in
188 let t1 := derivative_of X3
189 with t2 := derivative_of X4
191 with t4 := constr:X4 in
192 constr:(t3{*}t2{+}t1{*}t4)
194 let t1 := derivative_of X4 with t2 := constr:X3 in
196 | (?X3{^}0) => constr:([-C-]ZeroR)
198 let t1 := derivative_of X3 with t2 := constr:X3 with t3 := constr:X4 in
199 constr:(nring _ (S t3){**}(t1{*}t2{^}t3))
201 let t1 := derivative_of X3 with t2 := constr:X3 in
202 constr:({--}(t1{/}t2{*}t2))
204 let t1 := derivative_of X3
205 with t2 := derivative_of X4
207 with t4 := constr:X4 in
208 constr:((t1{*}t4{-}t3{*}t2){/}t4{*}t4)
210 let t1 := derivative_of X3
211 with t2 := derivative_of X4
212 with t3 := constr:X3 in
213 constr:((t3[o]t2){*}t1)
215 let t := constr:X3 in
217 | H:(Derivative_I (b:=t) ?X4) |- _ =>
218 let t1 := constr:X4 in
225 Ltac Deriv_I_substR :=
227 | |- (Derivative_I _ ?X1 _) =>
228 let t := derivative_of X1 in
229 apply Derivative_I_wdr with t