]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/tactics/DiffTactics3.mma
ground_2 released and permanently renamed as ground
[helm.git] / helm / software / matita / contribs / procedural / CoRN / tactics / DiffTactics3.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "CoRN.ma".
18
19 (* $Id: DiffTactics3.v,v 1.1.1.1 2004/02/05 16:25:44 lionelm Exp $ *)
20
21 (* begin hide *)
22
23 include "ftc/MoreFunSeries.ma".
24
25 include "ftc/Composition.ma".
26
27 include "tactics/DiffTactics2.ma".
28
29 (* UNEXPORTED
30 Ltac Deriv_substR :=
31   match goal with
32   |  |- (Derivative ?X1 _) =>
33       let t := derivative_of X1 in
34       apply Derivative_wdr with t
35   end.
36 *)
37
38 inline procedural "cic:/CoRN/tactics/DiffTactics3/symbPF.ind".
39
40 (*
41   | ssum0     : nat->(nat->symbPF)->symbPF
42   | ssumx     : (n:nat)((i:nat)(lt i n)->symbPF)->symbPF
43   | ssum      : nat->nat->(nat->symbPF)->symbPF
44 *)
45
46 inline procedural "cic:/CoRN/tactics/DiffTactics3/symb_to_PartIR.con" as definition.
47
48 inline procedural "cic:/CoRN/tactics/DiffTactics3/symbPF_deriv.con" as definition.
49
50 (* UNEXPORTED
51 Ltac PartIR_to_symbPF f :=
52   match constr:f with
53   | ([-C-]?X3) => constr:(sconst X3)
54   | FId => constr:sid
55   | (?X3{+}?X4) =>
56       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
57       constr:(splus t1 t2)
58   | ({--}?X3) =>
59       let t1 := PartIR_to_symbPF X3 in
60       constr:(sinv t1)
61   | (?X3{-}?X4) =>
62       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
63       constr:(sminus t1 t2)
64   | (?X3{*}?X4) =>
65       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
66       constr:(smult t1 t2)
67   | (?X3{**}?X4) =>
68       let t := PartIR_to_symbPF X4 in
69       constr:(sscalmult X3 t)
70   | (?X3{^}?X4) =>
71       let t1 := PartIR_to_symbPF X3 in
72       constr:(snth t1 X4)
73   | ({1/}?X3) =>
74       let t1 := PartIR_to_symbPF X3 in
75       constr:(srecip t1)
76   | (?X3{/}?X4) =>
77       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
78       constr:(sdiv t1 t2)
79   | (?X3[o]?X4) =>
80       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
81       constr:(scomp t1 t2)
82   | ?X3 =>
83       let t := constr:X3 in
84       match goal with
85       | H:(Derivative ?X1 ?X2 t ?X4) |- _ =>
86           constr:(shyp X1 X2 t X4 H)
87       | H:(Diffble ?X1 ?X2 t) |- _ => constr:(shyp' X1 X2 t H)
88       end
89   end.
90 *)
91
92 (* UNEXPORTED
93 Ltac Derivative_Help :=
94   match goal with
95   |  |- (Derivative ?X1 ?X2 ?X3 ?X4) =>
96       let r := PartIR_to_symbPF X3 in
97       (apply Derivative_wdr with (symbPF_deriv r);
98         [ unfold symbPF_deriv, symb_to_PartIR in |- *
99         | simpl in |- *; Deriv ])
100   end.
101 *)
102
103 (* end hide *)
104