matitaB/matita/contribs/dama/dama_didactic/ex_deriv.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
  16
  17 include "deriv.ma".
  18
  19 theorem p_plus_p_p: ∀f:F. ∀g:F. (fpari f ∧ fpari g) → fpari (f + g).
  20  assume f:F.
  21  assume g:F.
  22  suppose (fpari f ∧ fpari g) (h).
  23  by h we have (fpari f) (H) and (fpari g) (K).
  24  we need to prove (fpari (f + g))
  25  or equivalently ((f + g) = (f + g) ∘ ρ).
  26  conclude
  27     (f + g)
  28   = (f + (g ∘ ρ)) by _.
  29   = ((f ∘ ρ) + (g ∘ ρ)) by _.
  30   = ((f + g) ∘ ρ) by _
  31  done.
  32 qed.
  33
  34 theorem p_mult_p_p: ∀f:F. ∀g:F. (fpari f ∧ fpari g) → fpari (f · g).
  35  assume f:F.
  36  assume g:F.
  37  suppose (fpari f ∧ fpari g) (h).
  38  by h we have (fpari f) (H) and (fpari g) (K).
  39  we need to prove (fpari (f · g))
  40  or equivalently ((f · g) = (f · g) ∘ ρ).
  41  conclude
  42     (f · g)
  43   = (f · (g ∘ ρ)) by _.
  44   = ((f ∘ ρ) · (g ∘ ρ)) by _.
  45   = ((f · g) ∘ ρ) by _
  46  done.
  47 qed.
  48
  49 theorem d_plus_d_d: ∀f:F. ∀g:F. (fdispari f ∧ fdispari g) → fdispari (f + g).
  50  assume f:F.
  51  assume g:F.
  52  suppose (fdispari f ∧ fdispari g) (h).
  53  by h we have (fdispari f) (H) and (fdispari g) (K).
  54  we need to prove (fdispari (f + g))
  55  or equivalently ((f + g) = (ρ ∘ ((f + g) ∘ ρ))).
  56  conclude
  57     (f + g)
  58   = (f + (ρ ∘ (g ∘ ρ))) by _.
  59   = ((ρ ∘ (f ∘ ρ)) + (ρ ∘ (g ∘ ρ))) by _.
  60   = (((-R1) · (f ∘ ρ)) + (ρ ∘ (g ∘ ρ))) by _.
  61   = (((i (-R1)) · (f ∘ ρ)) + ((i (-R1)) · (g ∘ ρ))) by _.
  62   = (((f ∘ ρ) · (i (-R1))) + ((g ∘ ρ) · (i (-R1)))) by _.
  63   = (((f ∘ ρ) + (g ∘ ρ)) · (i (-R1))) by _.
  64   = ((i (-R1)) · ((f + g) ∘ ρ)) by _.
  65   = (ρ ∘ ((f + g) ∘ ρ)) by _
  66  done.
  67 qed.
  68
  69 theorem d_mult_d_p: ∀f:F. ∀g:F. (fdispari f ∧ fdispari g) → fpari (f · g).
  70  assume f:F.
  71  assume g:F.
  72  suppose (fdispari f ∧ fdispari g) (h).
  73  by h we have (fdispari f) (h1) and (fdispari g) (h2).
  74  we need to prove (fpari (f · g))
  75  or equivalently ((f · g) = (f · g) ∘ ρ).
  76  conclude
  77     (f · g)
  78   = (f · (ρ ∘ (g ∘ ρ))) by _.
  79   = ((ρ ∘ (f ∘ ρ)) · (ρ ∘ (g ∘ ρ))) by _.
  80   = (((-R1) · (f ∘ ρ)) · (ρ ∘ (g ∘ ρ))) by _.
  81   = (((-R1) · (f ∘ ρ)) · ((-R1) · (g ∘ ρ))) by _.
  82   = ((-R1) · (f ∘ ρ) · (-R1) · (g ∘ ρ)) by _.
  83   = ((-R1) · ((f ∘ ρ) · (-R1)) · (g ∘ ρ)) by _.
  84   = ((-R1) · (-R1) · (f ∘ ρ) · (g ∘ ρ)) by _.
  85   = (R1 · ((f ∘ ρ) · (g ∘ ρ))) by _.
  86   = (((f ∘ ρ) · (g ∘ ρ))) by _.
  87   = ((f · g) ∘ ρ) by _
  88  done.
  89 qed.
  90
  91 theorem p_mult_d_p: ∀f:F. ∀g:F. (fpari f ∧ fdispari g) → fdispari (f · g).
  92  assume f:F.
  93  assume g:F.
  94  suppose (fpari f ∧ fdispari g) (h).
  95  by h we have (fpari f) (h1) and (fdispari g) (h2).
  96  we need to prove (fdispari (f · g))
  97  or equivalently ((f · g) = ρ ∘ ((f · g) ∘ ρ)).
  98  conclude
  99     (f · g)
 100   = (f · (ρ ∘ (g ∘ ρ))) by _.
 101   = ((f ∘ ρ) · (ρ ∘ (g ∘ ρ))) by _.
 102   = ((f ∘ ρ) · ((-R1) · (g ∘ ρ))) by _.
 103   = ((-R1) · ((f ∘ ρ) · (g ∘ ρ))) by _.
 104   = ((-R1) · ((f · g) ∘ ρ)) by _.
 105   = (ρ ∘ ((f · g) ∘ ρ)) by _
 106  done.
 107 qed.
 108
 109 theorem p_plus_c_p: ∀f:F. ∀x:R. fpari f → fpari (f + (i x)).
 110  assume f:F.
 111  assume x:R.
 112  suppose (fpari f) (h).
 113  we need to prove (fpari (f + (i x)))
 114  or equivalently (f + (i x) = (f + (i x)) ∘ ρ).
 115  by _ done.
 116 qed.
 117
 118 theorem p_mult_c_p: ∀f:F. ∀x:R. fpari f → fpari (f · (i x)).
 119  assume f:F.
 120  assume x:R.
 121  suppose (fpari f) (h).
 122  we need to prove (fpari (f · (i x)))
 123  or equivalently ((f · (i x)) = (f · (i x)) ∘ ρ).
 124  by _ done.
 125 qed.
 126
 127 theorem d_mult_c_d: ∀f:F. ∀x:R. fdispari f → fdispari (f · (i x)).
 128  assume f:F.
 129  assume x:R.
 130  suppose (fdispari f) (h).
 131  rewrite < fmult_commutative.
 132  by _ done.
 133 qed.
 134
 135 theorem d_comp_d_d: ∀f,g:F. fdispari f → fdispari g → fdispari (f ∘ g).
 136  assume f:F.
 137  assume g:F.
 138  suppose (fdispari f) (h1).
 139  suppose (fdispari g) (h2).
 140  we need to prove (fdispari (f ∘ g))
 141  or equivalently (f ∘ g = ρ ∘ ((f ∘ g) ∘ ρ)).
 142  conclude
 143     (f ∘ g)
 144   = (ρ ∘ (f ∘ ρ) ∘ g) by _.
 145   = (ρ ∘ (f ∘ ρ) ∘ ρ ∘ (g ∘ ρ)) by _.
 146   = (ρ ∘ f ∘ (ρ ∘ ρ) ∘ (g ∘ ρ)) by _.
 147   = (ρ ∘ f ∘ id ∘ (g ∘ ρ)) by _.
 148   = (ρ ∘ ((f ∘ g) ∘ ρ)) by _
 149  done.
 150 qed.
 151
 152 theorem pari_in_dispari: ∀ f:F. fpari f → fdispari f '.
 153  assume f:F.
 154  suppose (fpari f) (h1).
 155  we need to prove (fdispari f ')
 156  or equivalently (f ' = ρ ∘ (f ' ∘ ρ)).
 157  conclude
 158     (f ')
 159   = ((f ∘ ρ) ') by _. (*h1*)
 160   = ((f ' ∘ ρ) · ρ ') by _. (*demult*)
 161   = ((f ' ∘ ρ) · -R1) by _. (*deinv*)
 162   = ((-R1) · (f ' ∘ ρ)) by _. (*fmult_commutative*)
 163   = (ρ ∘ (f ' ∘ ρ)) (*reflex_ok*) by _
 164  done.
 165 qed.
 166
 167 theorem dispari_in_pari: ∀ f:F. fdispari f → fpari f '.
 168  assume f:F.
 169  suppose (fdispari f) (h1).
 170  we need to prove (fpari f ')
 171  or equivalently (f ' = f ' ∘ ρ).
 172  conclude
 173     (f ')
 174   = ((ρ ∘ (f ∘ ρ)) ') by _.
 175   = ((ρ ' ∘ (f ∘ ρ)) · ((f ∘ ρ) ')) by _.
 176   = (((-R1) ∘ (f ∘ ρ)) · ((f ∘ ρ) ')) by _.
 177   = (((-R1) ∘ (f ∘ ρ)) · ((f ' ∘ ρ) · (-R1))) by _.
 178   = ((-R1) · ((f ' ∘ ρ) · (-R1))) by _.
 179   = (((f ' ∘ ρ) · (-R1)) · (-R1)) by _.
 180   = ((f ' ∘ ρ) · ((-R1) · (-R1))) by _.
 181   = ((f ' ∘ ρ) · R1) by _.
 182   = (f ' ∘ ρ) by _
 183  done.
 184 qed.
 185
 186 alias symbol "plus" = "natural plus".
 187 alias num (instance 0) = "natural number".
 188 theorem de_prodotto_funzioni:
 189  ∀ n:nat. (id ^ (n + 1)) ' = ((n + 1)) · (id ^ n).
 190  assume n:nat.
 191  we proceed by induction on n to prove
 192    ((id ^ (n + 1)) ' = (i (n + 1)) · (id ^ n)).
 193  case O.
 194   we need to prove ((id ^ (0 + 1)) ' = (i 1) · (id ^ 0)).
 195   conclude
 196      ((id ^ (0 + 1)) ')
 197    = ((id ^ 1) ') by _.
 198    = ((id · (id ^ 0)) ') by _.
 199    = ((id · R1) ') by _.
 200    = (id ') by _.
 201    = (i R1) by _.
 202    = (i R1 · R1) by _.
 203    = (i (R0 + R1) · R1) by _.
 204    = (1 · (id ^ 0)) by _
 205  done.
 206  case S (n:nat).
 207   by induction hypothesis we know
 208      ((id ^ (n + 1)) ' = ((n + 1)) · (id ^ n)) (H).
 209   we need to prove
 210      ((id ^ ((n + 1)+1)) '
 211    = (i ((n + 1)+1)) · (id ^ (n+1))).
 212   conclude
 213      ((id ^ ((n + 1) + 1)) ')
 214    = ((id ^ ((n + (S 1)))) ') by _.
 215    = ((id ^ (S (n + 1))) ') by _.
 216    = ((id · (id ^ (n + 1))) ') by _.
 217    = ((id ' · (id ^ (n + 1))) + (id · (id ^ (n + 1)) ')) by _.
 218    alias symbol "plus" (instance 1) = "function plus".
 219    = ((R1 · (id ^ (n + 1))) + (id · (((n + 1)) · (id ^ n)))) by _.
 220    = ((R1 · (id ^ (n + 1))) + (((n + 1) · id · (id ^ n)))) by _.
 221    = ((R1 · (id ^ (n + 1))) + ((n + 1) · (id ^ (1 + n)))) by _.
 222    = ((R1 · (id ^ (n + 1))) + ((n + 1) · (id ^ (n + 1)))) by _.
 223    alias symbol "plus" (instance 2) = "function plus".
 224    = (((R1 + (n + 1))) · (id ^ (n + 1))) by _.
 225    = ((1 + (n + 1)) · (id ^ (n + 1))) by _;
 226    = ((n + 1 + 1) · (id ^ (n + 1))) by _
 227   done.
 228 qed.
 229
 230 let rec times (n:nat) (x:R) on n: R ≝
 231  match n with
 232  [ O ⇒ R0
 233  | S n ⇒ Rplus x (times n x)
 234  ].
 235
 236 axiom invS: nat→R.
 237 axiom invS1: ∀n:nat. Rmult (invS n) (real_of_nat (n + 1)) = R1.
 238 axiom invS2: invS 1 + invS 1 = R1. (*forse*)
 239
 240 axiom e:F.
 241 axiom deriv_e: e ' = e.
 242 axiom e1: e · (e ∘ ρ) = R1.
 243
 244 (*
 245 theorem decosh_senh:
 246    (invS 1 · (e + (e ∘ ρ)))' = (invS 1 · (e + (ρ ∘ (e ∘ ρ)))).
 247 *)