matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma

   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 set "baseuri" "cic:/matita/CoRN-Decl/ftc/DerivativeOps".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: DerivativeOps.v,v 1.3 2004/04/23 10:00:58 lcf Exp $ *)
  22
  23 include "ftc/Derivative.ma".
  24
  25 (* UNEXPORTED
  26 Section Lemmas
  27 *)
  28
  29 (*#* **Algebraic Operations
  30
  31 We will now prove the main results about deriving functions built from
  32 the algebraic operators#. #%\footnote{%Composition presents some
  33 tricky questions, and is therefore discussed in a separated
  34 context.%}.%
  35
  36 [F'] and [G'] will be the derivatives, respectively, of [F] and [G].
  37
  38 We begin with some technical stuff that will be necessary for division.
  39 *)
  40
  41 alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/a.var".
  42
  43 alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/b.var".
  44
  45 alias id "Hab" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/Hab.var".
  46
  47 (* begin hide *)
  48
  49 inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/I.con" "Lemmas__".
  50
  51 (* end hide *)
  52
  53 alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/F.var".
  54
  55 (* begin hide *)
  56
  57 inline "cic:/CoRN/ftc/DerivativeOps/Lemmas/P.con" "Lemmas__".
  58
  59 (* end hide *)
  60
  61 (* begin show *)
  62
  63 alias id "Fbnd" = "cic:/CoRN/ftc/DerivativeOps/Lemmas/Fbnd.var".
  64
  65 (* end show *)
  66
  67 inline "cic:/CoRN/ftc/DerivativeOps/bnd_away_zero_square.con".
  68
  69 (* UNEXPORTED
  70 End Lemmas
  71 *)
  72
  73 (* UNEXPORTED
  74 Hint Resolve bnd_away_zero_square: included.
  75 *)
  76
  77 (* UNEXPORTED
  78 Section Local_Results
  79 *)
  80
  81 (*#* **Local Results
  82
  83 We can now derive all the usual rules for deriving constant and identity functions, sums, inverses and products of functions with a known derivative.
  84 *)
  85
  86 alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/a.var".
  87
  88 alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/b.var".
  89
  90 alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab'.var".
  91
  92 (* begin hide *)
  93
  94 inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/Hab.con" "Local_Results__".
  95
  96 inline "cic:/CoRN/ftc/DerivativeOps/Local_Results/I.con" "Local_Results__".
  97
  98 (* end hide *)
  99
 100 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_const.con".
 101
 102 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_id.con".
 103
 104 alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/F.var".
 105
 106 alias id "F'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/F'.var".
 107
 108 alias id "G" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/G.var".
 109
 110 alias id "G'" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/G'.var".
 111
 112 alias id "derF" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/derF.var".
 113
 114 alias id "derG" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/derG.var".
 115
 116 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_plus.con".
 117
 118 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_inv.con".
 119
 120 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_mult.con".
 121
 122 (*#*
 123 As was the case for continuity, the rule for the reciprocal function has a side condition.
 124 *)
 125
 126 (* begin show *)
 127
 128 alias id "Fbnd" = "cic:/CoRN/ftc/DerivativeOps/Local_Results/Fbnd.var".
 129
 130 (* end show *)
 131
 132 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_recip.con".
 133
 134 (* UNEXPORTED
 135 End Local_Results
 136 *)
 137
 138 (* UNEXPORTED
 139 Hint Immediate derivative_imp_inc derivative_imp_inc': included.
 140 *)
 141
 142 (* UNEXPORTED
 143 Hint Resolve Derivative_I_const Derivative_I_id Derivative_I_plus
 144   Derivative_I_inv Derivative_I_mult Derivative_I_recip: derivate.
 145 *)
 146
 147 (* UNEXPORTED
 148 Section Corolaries
 149 *)
 150
 151 alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/a.var".
 152
 153 alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/b.var".
 154
 155 alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab'.var".
 156
 157 (* begin hide *)
 158
 159 inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/Hab.con" "Corolaries__".
 160
 161 inline "cic:/CoRN/ftc/DerivativeOps/Corolaries/I.con" "Corolaries__".
 162
 163 (* end hide *)
 164
 165 alias id "F" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/F.var".
 166
 167 alias id "F'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/F'.var".
 168
 169 alias id "G" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/G.var".
 170
 171 alias id "G'" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/G'.var".
 172
 173 alias id "derF" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/derF.var".
 174
 175 alias id "derG" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/derG.var".
 176
 177 (*#*
 178 From this lemmas the rules for the other algebraic operations follow directly.
 179 *)
 180
 181 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_minus.con".
 182
 183 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_scal.con".
 184
 185 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_nth.con".
 186
 187 alias id "Gbnd" = "cic:/CoRN/ftc/DerivativeOps/Corolaries/Gbnd.var".
 188
 189 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_div.con".
 190
 191 (* UNEXPORTED
 192 End Corolaries
 193 *)
 194
 195 (* UNEXPORTED
 196 Hint Resolve Derivative_I_minus Derivative_I_nth Derivative_I_scal
 197   Derivative_I_div: derivate.
 198 *)
 199
 200 (* UNEXPORTED
 201 Section Derivative_Sums
 202 *)
 203
 204 (*#* The derivation rules for families of functions are easily proved by
 205 induction using the constant and addition rules.
 206 *)
 207
 208 alias id "a" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/a.var".
 209
 210 alias id "b" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/b.var".
 211
 212 alias id "Hab" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab.var".
 213
 214 alias id "Hab'" = "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/Hab'.var".
 215
 216 (* begin hide *)
 217
 218 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_Sums/I.con" "Derivative_Sums__".
 219
 220 (* end hide *)
 221
 222 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum0.con".
 223
 224 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sumx.con".
 225
 226 inline "cic:/CoRN/ftc/DerivativeOps/Derivative_I_Sum.con".
 227
 228 (* UNEXPORTED
 229 End Derivative_Sums
 230 *)
 231
 232 (* UNEXPORTED
 233 Hint Resolve Derivative_I_Sum0 Derivative_I_Sum Derivative_I_Sumx: derivate.
 234 *)
 235