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