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 (* $Id: DerivativeOps.v,v 1.3 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 Derivative
  23 *)
  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 inline cic:/CoRN/ftc/DerivativeOps/a.var.
  42
  43 inline cic:/CoRN/ftc/DerivativeOps/b.var.
  44
  45 inline cic:/CoRN/ftc/DerivativeOps/Hab.var.
  46
  47 (* begin hide *)
  48
  49 inline cic:/CoRN/ftc/DerivativeOps/I.con.
  50
  51 (* end hide *)
  52
  53 inline cic:/CoRN/ftc/DerivativeOps/F.var.
  54
  55 (* begin hide *)
  56
  57 inline cic:/CoRN/ftc/DerivativeOps/P.con.
  58
  59 (* end hide *)
  60
  61 (* begin show *)
  62
  63 inline cic:/CoRN/ftc/DerivativeOps/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 inline cic:/CoRN/ftc/DerivativeOps/a.var.
  87
  88 inline cic:/CoRN/ftc/DerivativeOps/b.var.
  89
  90 inline cic:/CoRN/ftc/DerivativeOps/Hab'.var.
  91
  92 (* begin hide *)
  93
  94 inline cic:/CoRN/ftc/DerivativeOps/Hab.con.
  95
  96 inline cic:/CoRN/ftc/DerivativeOps/I.con.
  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 inline cic:/CoRN/ftc/DerivativeOps/F.var.
 105
 106 inline cic:/CoRN/ftc/DerivativeOps/F'.var.
 107
 108 inline cic:/CoRN/ftc/DerivativeOps/G.var.
 109
 110 inline cic:/CoRN/ftc/DerivativeOps/G'.var.
 111
 112 inline cic:/CoRN/ftc/DerivativeOps/derF.var.
 113
 114 inline cic:/CoRN/ftc/DerivativeOps/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 inline cic:/CoRN/ftc/DerivativeOps/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 inline cic:/CoRN/ftc/DerivativeOps/a.var.
 152
 153 inline cic:/CoRN/ftc/DerivativeOps/b.var.
 154
 155 inline cic:/CoRN/ftc/DerivativeOps/Hab'.var.
 156
 157 (* begin hide *)
 158
 159 inline cic:/CoRN/ftc/DerivativeOps/Hab.con.
 160
 161 inline cic:/CoRN/ftc/DerivativeOps/I.con.
 162
 163 (* end hide *)
 164
 165 inline cic:/CoRN/ftc/DerivativeOps/F.var.
 166
 167 inline cic:/CoRN/ftc/DerivativeOps/F'.var.
 168
 169 inline cic:/CoRN/ftc/DerivativeOps/G.var.
 170
 171 inline cic:/CoRN/ftc/DerivativeOps/G'.var.
 172
 173 inline cic:/CoRN/ftc/DerivativeOps/derF.var.
 174
 175 inline cic:/CoRN/ftc/DerivativeOps/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 inline cic:/CoRN/ftc/DerivativeOps/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 inline cic:/CoRN/ftc/DerivativeOps/a.var.
 209
 210 inline cic:/CoRN/ftc/DerivativeOps/b.var.
 211
 212 inline cic:/CoRN/ftc/DerivativeOps/Hab.var.
 213
 214 inline cic:/CoRN/ftc/DerivativeOps/Hab'.var.
 215
 216 (* begin hide *)
 217
 218 inline cic:/CoRN/ftc/DerivativeOps/I.con.
 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