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