helm/software/matita/contribs/procedural/CoRN/tactics/DiffTactics2.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: DiffTactics2.v,v 1.1.1.1 2004/02/05 16:25:45 lionelm Exp $ *)
  20
  21 (* begin hide *)
  22
  23 include "ftc/Differentiability.ma".
  24
  25 (* UNEXPORTED
  26 Section Automatizing_Continuity
  27 *)
  28
  29 (* UNEXPORTED
  30 cic:/CoRN/tactics/DiffTactics2/Automatizing_Continuity/a.var
  31 *)
  32
  33 (* UNEXPORTED
  34 cic:/CoRN/tactics/DiffTactics2/Automatizing_Continuity/b.var
  35 *)
  36
  37 inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_function.ind".
  38
  39 inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_to_pfunct.con" as definition.
  40
  41 inline procedural "cic:/CoRN/tactics/DiffTactics2/continuous_cont.con" as lemma.
  42
  43 (* UNEXPORTED
  44 End Automatizing_Continuity
  45 *)
  46
  47 (* UNEXPORTED
  48 Ltac pfunct_to_cont a b f :=
  49   match constr:f with
  50   | ([-C-]?X3) => constr:(cconst a b X3)
  51   | FId => constr:(cid a b)
  52   | (?X3{+}?X4) =>
  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)
  55   | ({--}?X3) =>
  56       let t1 := pfunct_to_cont a b X3 in
  57       constr:(cinv a b t1)
  58   | (?X3{-}?X4) =>
  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)
  61   | (?X3{*}?X4) =>
  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)
  64   | (?X3{**}?X4) =>
  65       let t := pfunct_to_cont a b X4 in
  66       constr:(cscalmult a b X3 t)
  67   | (?X3{^}?X4) =>
  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
  71                   constr:(cabs a b t1)
  72   | ?X3 =>
  73       let t := constr:X3 in
  74       match goal with
  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)
  83       end
  84   end.
  85 *)
  86
  87 (* UNEXPORTED
  88 Ltac New_Contin :=
  89   match goal with
  90   |  |- (Continuous_I (a:=?X1) (b:=?X2) ?X4 ?X3) =>
  91       let r := pfunct_to_cont X1 X2 X3 in
  92       let a := constr:X1 in
  93       let b := constr:X2 in
  94       (apply Continuous_I_wd with (cont_to_pfunct a b r);
  95         [ unfold cont_to_pfunct in |- * | apply continuous_cont ])
  96   end.
  97 *)
  98
  99 (* UNEXPORTED
 100 Section Automatizing_Derivatives
 101 *)
 102
 103 (* UNEXPORTED
 104 cic:/CoRN/tactics/DiffTactics2/Automatizing_Derivatives/a.var
 105 *)
 106
 107 (* UNEXPORTED
 108 cic:/CoRN/tactics/DiffTactics2/Automatizing_Derivatives/b.var
 109 *)
 110
 111 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_function.ind".
 112
 113 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_to_pfunct.con" as definition.
 114
 115 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_deriv.con" as definition.
 116
 117 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_restr.con" as lemma.
 118
 119 inline procedural "cic:/CoRN/tactics/DiffTactics2/diffble_restr.con" as lemma.
 120
 121 (* UNEXPORTED
 122 End Automatizing_Derivatives
 123 *)
 124
 125 (* UNEXPORTED
 126 Ltac pfunct_to_restr a b f :=
 127   match constr:f with
 128   | ([-C-]?X3) => constr:(const a b X3)
 129   | FId => constr:(id a b)
 130   | (?X3{+}?X4) =>
 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)
 133   | ({--}?X3) =>
 134       let t1 := pfunct_to_restr a b X3 in
 135       constr:(rinv a b t1)
 136   | (?X3{-}?X4) =>
 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)
 139   | (?X3{*}?X4) =>
 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)
 142   | (?X3{**}?X4) =>
 143       let t := pfunct_to_restr a b X4 in
 144       constr:(rscalmult a b X3 t)
 145   | (?X3{^}?X4) =>
 146       let t1 := pfunct_to_restr a b X3 in
 147       constr:(rnth a b t1 X4)
 148   | ?X3 =>
 149       let t := constr:X3 in
 150       match goal with
 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:(
 154       hyp' a b X1 t H)
 155       end
 156   end.
 157 *)
 158
 159 (* UNEXPORTED
 160 Ltac New_Deriv :=
 161   match goal with
 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 ] ])
 169   end.
 170 *)
 171
 172 (* UNEXPORTED
 173 Ltac Differentiate :=
 174   match goal with
 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 |- * ])
 179   end.
 180 *)
 181
 182 (* UNEXPORTED
 183 Ltac derivative_of f :=
 184   match constr:f with
 185   | ([-C-]?X3) => constr:([-C-]ZeroR)
 186   | FId => constr:([-C-]OneR)
 187   | (?X3{+}?X4) =>
 188       let t1 := derivative_of X3 with t2 := derivative_of X4 in
 189       constr:(t1{+}t2)
 190   | ({--}?X3) => let t1 := derivative_of X3 in
 191                  constr:({--}t1)
 192   | (?X3{-}?X4) =>
 193       let t1 := derivative_of X3 with t2 := derivative_of X4 in
 194       constr:(t1{-}t2)
 195   | (?X3{*}?X4) =>
 196       let t1 := derivative_of X3
 197       with t2 := derivative_of X4
 198       with t3 := constr:X3
 199       with t4 := constr:X4 in
 200       constr:(t3{*}t2{+}t1{*}t4)
 201   | (?X3{**}?X4) =>
 202       let t1 := derivative_of X4 with t2 := constr:X3 in
 203       constr:(t2{**}t1)
 204   | (?X3{^}0) => constr:([-C-]ZeroR)
 205   | (?X3{^}S ?X4) =>
 206       let t1 := derivative_of X3 with t2 := constr:X3 with t3 := constr:X4 in
 207       constr:(nring _ (S t3){**}(t1{*}t2{^}t3))
 208   | ({1/}?X3) =>
 209       let t1 := derivative_of X3 with t2 := constr:X3 in
 210       constr:({--}(t1{/}t2{*}t2))
 211   | (?X3{/}?X4) =>
 212       let t1 := derivative_of X3
 213       with t2 := derivative_of X4
 214       with t3 := constr:X3
 215       with t4 := constr:X4 in
 216       constr:((t1{*}t4{-}t3{*}t2){/}t4{*}t4)
 217   | (?X3[o]?X4) =>
 218       let t1 := derivative_of X3
 219       with t2 := derivative_of X4
 220       with t3 := constr:X3 in
 221       constr:((t3[o]t2){*}t1)
 222   | ?X3 =>
 223       let t := constr:X3 in
 224       match goal with
 225       | H:(Derivative_I (b:=t) ?X4) |- _ =>
 226           let t1 := constr:X4 in
 227           constr:t1
 228       end
 229   end.
 230 *)
 231
 232 (* UNEXPORTED
 233 Ltac Deriv_I_substR :=
 234   match goal with
 235   |  |- (Derivative_I _ ?X1 _) =>
 236       let t := derivative_of X1 in
 237       apply Derivative_I_wdr with t
 238   end.
 239 *)
 240
 241 (* end hide *)
 242