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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/tactics/DiffTactics3".
19 (* $Id: DiffTactics3.v,v 1.1.1.1 2004/02/05 16:25:44 lionelm Exp $ *)
38 | |- (Derivative ?X1 _) =>
39 let t := derivative_of X1 in
40 apply Derivative_wdr with t
44 inline cic:/CoRN/tactics/DiffTactics3/symbPF.ind.
47 | ssum0 : nat->(nat->symbPF)->symbPF
48 | ssumx : (n:nat)((i:nat)(lt i n)->symbPF)->symbPF
49 | ssum : nat->nat->(nat->symbPF)->symbPF
52 inline cic:/CoRN/tactics/DiffTactics3/symb_to_PartIR.con.
54 inline cic:/CoRN/tactics/DiffTactics3/symbPF_deriv.con.
57 Ltac PartIR_to_symbPF f :=
59 | ([-C-]?X3) => constr:(sconst X3)
62 let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
65 let t1 := PartIR_to_symbPF X3 in
68 let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
71 let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
74 let t := PartIR_to_symbPF X4 in
75 constr:(sscalmult X3 t)
77 let t1 := PartIR_to_symbPF X3 in
80 let t1 := PartIR_to_symbPF X3 in
83 let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
86 let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
91 | H:(Derivative ?X1 ?X2 t ?X4) |- _ =>
92 constr:(shyp X1 X2 t X4 H)
93 | H:(Diffble ?X1 ?X2 t) |- _ => constr:(shyp' X1 X2 t H)
99 Ltac Derivative_Help :=
101 | |- (Derivative ?X1 ?X2 ?X3 ?X4) =>
102 let r := PartIR_to_symbPF X3 in
103 (apply Derivative_wdr with (symbPF_deriv r);
104 [ unfold symbPF_deriv, symb_to_PartIR in |- *
105 | simpl in |- *; Deriv ])