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
30 cic:/CoRN/tactics/DiffTactics2/Automatizing_Continuity/a.var
34 cic:/CoRN/tactics/DiffTactics2/Automatizing_Continuity/b.var
37 inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_function.ind".
39 inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_to_pfunct.con" as definition.
41 inline procedural "cic:/CoRN/tactics/DiffTactics2/continuous_cont.con" as lemma.
44 End Automatizing_Continuity
48 Ltac pfunct_to_cont a b f :=
50 | ([-C-]?X3) => constr:(cconst a b X3)
51 | FId => constr:(cid a b)
53 let t1 := pfunct_to_cont a b X3 with t2 := pfunct_to_cont a b X4 in
54 constr:(cplus a b t1 t2)
56 let t1 := pfunct_to_cont a b X3 in
59 let t1 := pfunct_to_cont a b X3 with t2 := pfunct_to_cont a b X4 in
60 constr:(cminus a b t1 t2)
62 let t1 := pfunct_to_cont a b X3 with t2 := pfunct_to_cont a b X4 in
63 constr:(cmult a b t1 t2)
65 let t := pfunct_to_cont a b X4 in
66 constr:(cscalmult a b X3 t)
68 let t1 := pfunct_to_cont a b X3 in
69 constr:(cnth a b t1 X4)
70 | (FAbs ?X3) => let t1 := pfunct_to_cont a b X3 in
75 | Hab:_,H:(Continuous_I (a:=a) (b:=b) ?X1 t) |- _ =>
76 constr:(hyp_c a b X1 t H)
77 | H:(Derivative_I (a:=a) (b:=b) ?X1 t ?X4) |- _ =>
78 constr:(hyp_d a b X1 t X4 H)
79 | H:(Derivative_I (a:=a) (b:=b) ?X1 ?X4 t) |- _ =>
80 constr:(hyp_d' a b X1 X4 t H)
81 | H:(Diffble_I (a:=a) (b:=b) ?X1 t) |- _ =>
82 constr:(hyp_diff a b X1 t H)
90 | |- (Continuous_I (a:=?X1) (b:=?X2) ?X4 ?X3) =>
91 let r := pfunct_to_cont X1 X2 X3 in
94 (apply Continuous_I_wd with (cont_to_pfunct a b r);
95 [ unfold cont_to_pfunct in |- * | apply continuous_cont ])
100 Section Automatizing_Derivatives
104 cic:/CoRN/tactics/DiffTactics2/Automatizing_Derivatives/a.var
108 cic:/CoRN/tactics/DiffTactics2/Automatizing_Derivatives/b.var
111 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_function.ind".
113 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_to_pfunct.con" as definition.
115 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_deriv.con" as definition.
117 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_restr.con" as lemma.
119 inline procedural "cic:/CoRN/tactics/DiffTactics2/diffble_restr.con" as lemma.
122 End Automatizing_Derivatives
126 Ltac pfunct_to_restr a b f :=
128 | ([-C-]?X3) => constr:(const a b X3)
129 | FId => constr:(id a b)
131 let t1 := pfunct_to_restr a b X3 with t2 := pfunct_to_restr a b X4 in
132 constr:(rplus a b t1 t2)
134 let t1 := pfunct_to_restr a b X3 in
137 let t1 := pfunct_to_restr a b X3 with t2 := pfunct_to_restr a b X4 in
138 constr:(rminus a b t1 t2)
140 let t1 := pfunct_to_restr a b X3 with t2 := pfunct_to_restr a b X4 in
141 constr:(rmult a b t1 t2)
143 let t := pfunct_to_restr a b X4 in
144 constr:(rscalmult a b X3 t)
146 let t1 := pfunct_to_restr a b X3 in
147 constr:(rnth a b t1 X4)
149 let t := constr:X3 in
151 | H:(Derivative_I (a:=a) (b:=b) ?X1 t ?X4) |- _ =>
152 constr:(hyp a b X1 t X4 H)
153 | H:(Diffble_I (a:=a) (b:=b) ?X1 t) |- _ => constr:(
162 | |- (Derivative_I (a:=?X1) (b:=?X2) _ ?X3 ?X4) =>
163 let r := pfunct_to_restr X1 X2 X3 in
164 (apply Derivative_I_wdl with (deriv_to_pfunct X1 X2 r);
165 [ unfold deriv_to_pfunct in |- *
166 | apply Derivative_I_wdr with (deriv_deriv X1 X2 r);
167 [ unfold deriv_deriv, deriv_to_pfunct in |- *
168 | apply deriv_restr ] ])
173 Ltac Differentiate :=
175 | |- (Diffble_I (a:=?X1) (b:=?X2) _ ?X3) =>
176 let r := pfunct_to_restr X1 X2 X3 in
177 (apply Diffble_I_wd with (deriv_to_pfunct X1 X2 r);
178 [ apply diffble_restr | unfold deriv_deriv, deriv_to_pfunct in |- * ])
183 Ltac derivative_of f :=
185 | ([-C-]?X3) => constr:([-C-]ZeroR)
186 | FId => constr:([-C-]OneR)
188 let t1 := derivative_of X3 with t2 := derivative_of X4 in
190 | ({--}?X3) => let t1 := derivative_of X3 in
193 let t1 := derivative_of X3 with t2 := derivative_of X4 in
196 let t1 := derivative_of X3
197 with t2 := derivative_of X4
199 with t4 := constr:X4 in
200 constr:(t3{*}t2{+}t1{*}t4)
202 let t1 := derivative_of X4 with t2 := constr:X3 in
204 | (?X3{^}0) => constr:([-C-]ZeroR)
206 let t1 := derivative_of X3 with t2 := constr:X3 with t3 := constr:X4 in
207 constr:(nring _ (S t3){**}(t1{*}t2{^}t3))
209 let t1 := derivative_of X3 with t2 := constr:X3 in
210 constr:({--}(t1{/}t2{*}t2))
212 let t1 := derivative_of X3
213 with t2 := derivative_of X4
215 with t4 := constr:X4 in
216 constr:((t1{*}t4{-}t3{*}t2){/}t4{*}t4)
218 let t1 := derivative_of X3
219 with t2 := derivative_of X4
220 with t3 := constr:X3 in
221 constr:((t3[o]t2){*}t1)
223 let t := constr:X3 in
225 | H:(Derivative_I (b:=t) ?X4) |- _ =>
226 let t1 := constr:X4 in
233 Ltac Deriv_I_substR :=
235 | |- (Derivative_I _ ?X1 _) =>
236 let t := derivative_of X1 in
237 apply Derivative_I_wdr with t