helm/software/matita/contribs/CoRN-Procedural/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 alias id "a" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Continuity/a.var".
  30
  31 alias id "b" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Continuity/b.var".
  32
  33 inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_function.ind".
  34
  35 inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_to_pfunct.con".
  36
  37 inline procedural "cic:/CoRN/tactics/DiffTactics2/continuous_cont.con".
  38
  39 (* UNEXPORTED
  40 End Automatizing_Continuity
  41 *)
  42
  43 (* UNEXPORTED
  44 Ltac pfunct_to_cont a b f :=
  45   match constr:f with
  46   | ([-C-]?X3) => constr:(cconst a b X3)
  47   | FId => constr:(cid a b)
  48   | (?X3{+}?X4) =>
  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)
  51   | ({--}?X3) =>
  52       let t1 := pfunct_to_cont a b X3 in
  53       constr:(cinv a b t1)
  54   | (?X3{-}?X4) =>
  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)
  57   | (?X3{*}?X4) =>
  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)
  60   | (?X3{**}?X4) =>
  61       let t := pfunct_to_cont a b X4 in
  62       constr:(cscalmult a b X3 t)
  63   | (?X3{^}?X4) =>
  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
  67                   constr:(cabs a b t1)
  68   | ?X3 =>
  69       let t := constr:X3 in
  70       match goal with
  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)
  79       end
  80   end.
  81 *)
  82
  83 (* UNEXPORTED
  84 Ltac New_Contin :=
  85   match goal with
  86   |  |- (Continuous_I (a:=?X1) (b:=?X2) ?X4 ?X3) =>
  87       let r := pfunct_to_cont X1 X2 X3 in
  88       let a := constr:X1 in
  89       let b := constr:X2 in
  90       (apply Continuous_I_wd with (cont_to_pfunct a b r);
  91         [ unfold cont_to_pfunct in |- * | apply continuous_cont ])
  92   end.
  93 *)
  94
  95 (* UNEXPORTED
  96 Section Automatizing_Derivatives
  97 *)
  98
  99 alias id "a" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Derivatives/a.var".
 100
 101 alias id "b" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Derivatives/b.var".
 102
 103 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_function.ind".
 104
 105 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_to_pfunct.con".
 106
 107 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_deriv.con".
 108
 109 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_restr.con".
 110
 111 inline procedural "cic:/CoRN/tactics/DiffTactics2/diffble_restr.con".
 112
 113 (* UNEXPORTED
 114 End Automatizing_Derivatives
 115 *)
 116
 117 (* UNEXPORTED
 118 Ltac pfunct_to_restr a b f :=
 119   match constr:f with
 120   | ([-C-]?X3) => constr:(const a b X3)
 121   | FId => constr:(id a b)
 122   | (?X3{+}?X4) =>
 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)
 125   | ({--}?X3) =>
 126       let t1 := pfunct_to_restr a b X3 in
 127       constr:(rinv a b t1)
 128   | (?X3{-}?X4) =>
 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)
 131   | (?X3{*}?X4) =>
 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)
 134   | (?X3{**}?X4) =>
 135       let t := pfunct_to_restr a b X4 in
 136       constr:(rscalmult a b X3 t)
 137   | (?X3{^}?X4) =>
 138       let t1 := pfunct_to_restr a b X3 in
 139       constr:(rnth a b t1 X4)
 140   | ?X3 =>
 141       let t := constr:X3 in
 142       match goal with
 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:(
 146       hyp' a b X1 t H)
 147       end
 148   end.
 149 *)
 150
 151 (* UNEXPORTED
 152 Ltac New_Deriv :=
 153   match goal with
 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 ] ])
 161   end.
 162 *)
 163
 164 (* UNEXPORTED
 165 Ltac Differentiate :=
 166   match goal with
 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 |- * ])
 171   end.
 172 *)
 173
 174 (* UNEXPORTED
 175 Ltac derivative_of f :=
 176   match constr:f with
 177   | ([-C-]?X3) => constr:([-C-]ZeroR)
 178   | FId => constr:([-C-]OneR)
 179   | (?X3{+}?X4) =>
 180       let t1 := derivative_of X3 with t2 := derivative_of X4 in
 181       constr:(t1{+}t2)
 182   | ({--}?X3) => let t1 := derivative_of X3 in
 183                  constr:({--}t1)
 184   | (?X3{-}?X4) =>
 185       let t1 := derivative_of X3 with t2 := derivative_of X4 in
 186       constr:(t1{-}t2)
 187   | (?X3{*}?X4) =>
 188       let t1 := derivative_of X3
 189       with t2 := derivative_of X4
 190       with t3 := constr:X3
 191       with t4 := constr:X4 in
 192       constr:(t3{*}t2{+}t1{*}t4)
 193   | (?X3{**}?X4) =>
 194       let t1 := derivative_of X4 with t2 := constr:X3 in
 195       constr:(t2{**}t1)
 196   | (?X3{^}0) => constr:([-C-]ZeroR)
 197   | (?X3{^}S ?X4) =>
 198       let t1 := derivative_of X3 with t2 := constr:X3 with t3 := constr:X4 in
 199       constr:(nring _ (S t3){**}(t1{*}t2{^}t3))
 200   | ({1/}?X3) =>
 201       let t1 := derivative_of X3 with t2 := constr:X3 in
 202       constr:({--}(t1{/}t2{*}t2))
 203   | (?X3{/}?X4) =>
 204       let t1 := derivative_of X3
 205       with t2 := derivative_of X4
 206       with t3 := constr:X3
 207       with t4 := constr:X4 in
 208       constr:((t1{*}t4{-}t3{*}t2){/}t4{*}t4)
 209   | (?X3[o]?X4) =>
 210       let t1 := derivative_of X3
 211       with t2 := derivative_of X4
 212       with t3 := constr:X3 in
 213       constr:((t3[o]t2){*}t1)
 214   | ?X3 =>
 215       let t := constr:X3 in
 216       match goal with
 217       | H:(Derivative_I (b:=t) ?X4) |- _ =>
 218           let t1 := constr:X4 in
 219           constr:t1
 220       end
 221   end.
 222 *)
 223
 224 (* UNEXPORTED
 225 Ltac Deriv_I_substR :=
 226   match goal with
 227   |  |- (Derivative_I _ ?X1 _) =>
 228       let t := derivative_of X1 in
 229       apply Derivative_I_wdr with t
 230   end.
 231 *)
 232
 233 (* end hide *)
 234