matita/library/demo/power_derivative.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 set "baseuri" "cic:/matita/demo/power_derivative".
  16
  17 include "nat/plus.ma".
  18 include "nat/orders.ma".
  19 include "nat/compare.ma".
  20
  21 axiom R: Type.
  22 axiom R0: R.
  23 axiom R1: R.
  24 axiom Rplus: R→R→R.
  25 axiom Rmult: R→R→R.
  26
  27 notation "0" with precedence 89
  28 for @{ 'zero }.
  29 interpretation "Rzero" 'zero =
  30  (cic:/matita/demo/power_derivative/R0.con).
  31 interpretation "Nzero" 'zero =
  32  (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)).
  33
  34 notation "1" with precedence 89
  35 for @{ 'one }.
  36 interpretation "Rone" 'one =
  37  (cic:/matita/demo/power_derivative/R1.con).
  38 interpretation "None" 'one =
  39  (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
  40    cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)).
  41
  42 interpretation "Rplus" 'plus x y =
  43  (cic:/matita/demo/power_derivative/Rplus.con x y).
  44
  45 notation "hvbox(a break \middot b)"
  46   left associative with precedence 55
  47 for @{ 'times $a $b }.
  48
  49 interpretation "Rmult" 'times x y =
  50  (cic:/matita/demo/power_derivative/Rmult.con x y).
  51
  52 definition Fplus ≝
  53  λf,g:R→R.λx:R.f x + g x.
  54
  55 definition Fmult ≝
  56  λf,g:R→R.λx:R.f x · g x.
  57
  58 interpretation "Fplus" 'plus x y =
  59  (cic:/matita/demo/power_derivative/Fplus.con x y).
  60 interpretation "Fmult" 'times x y =
  61  (cic:/matita/demo/power_derivative/Fmult.con x y).
  62
  63 notation "2" with precedence 89
  64 for @{ 'two }.
  65 interpretation "Rtwo" 'two =
  66  (cic:/matita/demo/power_derivative/Rplus.con
  67    cic:/matita/demo/power_derivative/R1.con
  68    cic:/matita/demo/power_derivative/R1.con).
  69 interpretation "Ntwo" 'two =
  70  (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
  71    (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
  72      (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))).
  73
  74 let rec Rpower (x:R) (n:nat) on n ≝
  75  match n with
  76   [ O ⇒ 1
  77   | S n ⇒ x · (Rpower x n)
  78   ].
  79
  80 interpretation "Rpower" 'exp x n =
  81  (cic:/matita/demo/power_derivative/Rpower.con x n).
  82
  83 let rec inj (n:nat) on n : R ≝
  84  match n with
  85   [ O ⇒ 0
  86   | S n ⇒
  87      match n with
  88       [ O ⇒ 1
  89       | S m ⇒ 1 + inj n
  90       ]
  91   ].
  92
  93 coercion cic:/matita/demo/power_derivative/inj.con.
  94
  95 axiom Rplus_Rzero_x: ∀x:R.0+x=x.
  96 axiom Rplus_comm: symmetric ? Rplus.
  97 axiom Rplus_assoc: associative ? Rplus.
  98 axiom Rmult_Rone_x: ∀x:R.1*x=x.
  99 axiom Rmult_Rzero_x: ∀x:R.0*x=0.
 100 axiom Rmult_assoc: associative ? Rmult.
 101 axiom Rmult_comm: symmetric ? Rmult.
 102 axiom Rmult_Rplus_distr: distributive ? Rmult Rplus.
 103
 104 alias symbol "times" = "Rmult".
 105 alias symbol "plus" = "natural plus".
 106
 107 definition monomio ≝
 108  λn.λx:R.x\sup n.
 109
 110 definition costante : nat → R → R ≝
 111  λa:nat.λx:R.inj a.
 112
 113 coercion cic:/matita/demo/power_derivative/costante.con 1.
 114
 115 axiom f_eq_extensional:
 116  ∀f,g:R→R.(∀x:R.f x = g x) → f=g.
 117
 118 lemma Fmult_one_f: ∀f:R→R.1·f=f.
 119  intro;
 120  unfold Fmult;
 121  simplify;
 122  apply f_eq_extensional;
 123  intro;
 124  autobatch.
 125 qed.
 126
 127 lemma Fmult_zero_f: ∀f:R→R.0·f=0.
 128  intro;
 129  unfold Fmult;
 130  simplify;
 131  apply f_eq_extensional;
 132  intro;
 133  autobatch.
 134 qed.
 135
 136 lemma Fmult_commutative: symmetric ? Fmult.
 137  unfold;
 138  intros;
 139  unfold Fmult;
 140  apply f_eq_extensional;
 141  intros;
 142  autobatch.
 143 qed.
 144
 145 lemma Fmult_associative: associative ? Fmult.
 146  unfold;
 147  intros;
 148  unfold Fmult;
 149  unfold Fmult;
 150  apply f_eq_extensional;
 151  intros;
 152  autobatch.
 153 qed.
 154
 155 lemma Fmult_Fplus_distr: distributive ? Fmult Fplus.
 156  unfold;
 157  intros;
 158  unfold Fmult;
 159  unfold Fplus;
 160  apply f_eq_extensional;
 161  intros;
 162  simplify;
 163  autobatch.
 164 qed.
 165
 166 lemma monomio_product:
 167  ∀n,m.monomio (n+m) = monomio n · monomio m.
 168  intros;
 169  unfold monomio;
 170  unfold Fmult;
 171  simplify;
 172  elim n;
 173   [ simplify;
 174     apply f_eq_extensional;
 175     intro;
 176     autobatch
 177   | simplify;
 178     apply f_eq_extensional;
 179     intro;
 180     cut (x\sup (n1+m) = x \sup n1 · x \sup m);
 181      [ rewrite > Hcut;
 182        autobatch
 183      | change in ⊢ (? ? % ?) with ((λx:R.x\sup(n1+m)) x);
 184        rewrite > H;
 185        reflexivity
 186      ]
 187   ].
 188 qed.
 189
 190 lemma costante_sum:
 191  ∀n,m.costante n + costante m = costante (n+m).
 192  intros;
 193  unfold Fplus;
 194  unfold costante;
 195  apply f_eq_extensional;
 196  intros;
 197  elim n;
 198   [ simplify;
 199     autobatch
 200   | simplify;
 201     clear x;
 202     clear H;
 203     clear n;
 204     elim n1;
 205      [ simplify;
 206        elim m;
 207         [ simplify;
 208           autobatch
 209         | simplify;
 210           rewrite < H;
 211           autobatch
 212         ]
 213      | simplify;
 214        rewrite < H;
 215        clear H;
 216        elim n;
 217         [ simplify;
 218           autobatch
 219         | simplify;
 220           autobatch
 221         ]
 222      ]
 223    ].
 224 qed.
 225
 226 axiom derivative: (R→R) → R → R.
 227
 228 notation "hvbox('D'[f])"
 229   non associative with precedence 90
 230 for @{ 'derivative $f }.
 231
 232 interpretation "Rderivative" 'derivative f =
 233  (cic:/matita/demo/power_derivative/derivative.con f).
 234
 235 notation "hvbox('x' \sup n)"
 236   non associative with precedence 60
 237 for @{ 'monomio $n }.
 238
 239 notation "hvbox('x')"
 240   non associative with precedence 60
 241 for @{ 'monomio 1 }.
 242
 243 interpretation "Rmonomio" 'monomio n =
 244  (cic:/matita/demo/power_derivative/monomio.con n).
 245
 246 axiom derivative_x0: D[x \sup 0] = 0.
 247 axiom derivative_x1: D[x] = 1.
 248 axiom derivative_mult: ∀f,g:R→R. D[f·g] = D[f]·g + f·D[g].
 249
 250 alias symbol "times" = "Fmult".
 251
 252 theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n).
 253  assume n:nat.
 254  (*we proceed by induction on n to prove
 255  (D[x \sup n] = n · x \sup (pred n)).*)
 256  elim n 0.
 257  case O.
 258    the thesis becomes (D[x \sup 0] = 0·x \sup (pred 0)).
 259    by _
 260   done.
 261  case S (m:nat).
 262   by induction hypothesis we know
 263    (D[x \sup m] = m·x \sup (pred m)) (H).
 264   the thesis becomes
 265    (D[x \sup (1+m)] = (1+m) · x \sup m).
 266   we need to prove
 267    (m · (x \sup (1+ pred m)) = m · x \sup m) (Ppred).
 268    by _ we proved (0 < m ∨ 0=m) (cases).
 269    we proceed by induction on cases
 270    to prove (m · (x \sup (1+ pred m)) = m · x \sup m).
 271     case left.
 272       suppose (0 < m) (m_pos).
 273       by (S_pred m m_pos) we proved (m = 1 + pred m) (H1).
 274       by _
 275      done.
 276     case right.
 277       suppose (0=m) (m_zero). by _ done.
 278   conclude
 279      (D[x \sup (1+m)])
 280    = (D[x · x \sup m]).
 281    = (D[x] · x \sup m + x · D[x \sup m]).
 282    = (x \sup m + x · (m · x \sup (pred m))).
 283    = (x \sup m + m · (x \sup (1 + pred m))).
 284    = (x \sup m + m · x \sup m).
 285    = ((1+m) · x \sup m) by Fmult_one_f Fmult_commutative Fmult_Fplus_distr costante_sum
 286   done.
 287 qed.
 288
 289 (*
 290 notation "hvbox(\frac 'd' ('d' ident i) break p)"
 291   right associative with precedence 90
 292 for @{ 'derivative ${default
 293   @{\lambda ${ident i} : $ty. $p)}
 294   @{\lambda ${ident i} . $p}}}.
 295
 296 interpretation "Rderivative" 'derivative \eta.f =
 297  (cic:/matita/demo/power_derivative/derivative.con f).
 298 *)
 299
 300 notation "hvbox(\frac 'd' ('d' 'x') break p)"
 301   right associative with precedence 90
 302 for @{ 'derivative $p}.
 303
 304 interpretation "Rderivative" 'derivative f =
 305  (cic:/matita/demo/power_derivative/derivative.con f).
 306
 307 theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n.
 308  assume n:nat.
 309  (*we proceed by induction on n to prove
 310  (D[x \sup (1+n)] = (1+n) · x \sup n).*) elim n 0.
 311  case O.
 312    the thesis becomes (D[x \sup 1] = 1 · x \sup 0).
 313    by _
 314   done.
 315  case S (m:nat).
 316   by induction hypothesis we know
 317    (D[x \sup (1+m)] = (1+m) · x \sup m) (H).
 318   the thesis becomes
 319    (D[x \sup (2+m)] = (2+m) · x \sup (1+m)).
 320   conclude
 321      (D[x \sup (2+m)])
 322    = (D[x · x \sup (1+m)]).
 323    = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]).
 324    = (x \sup (1+m) + x · (costante (1+m) · x \sup m)).
 325    = (x \sup (1+m) + costante (1+m) · x \sup (1+m)).
 326    = ((2+m) · x \sup (1+m)) by Fmult_one_f Fmult_commutative
 327      Fmult_Fplus_distr assoc_plus plus_n_SO costante_sum
 328   done.
 329 qed.