X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpower_derivative.ma;h=4f1b44000889a1df1b765d98a29977b8a3b2a432;hb=5649890273cf8e660bba744e84ce5fee1e5efe69;hp=dc3f4c828f25c26e716678abdbd13e69c2a132f0;hpb=0034d878cbd23062c7312e13d654ac7fd23a01cf;p=helm.git

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index dc3f4c828..4f1b44000 100644
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -121,7 +121,7 @@ lemma Fmult_one_f: ∀f:R→R.1·f=f.
  simplify;
  apply f_eq_extensional;
  intro;
- auto.
+ autobatch.
 qed.
 
 lemma Fmult_zero_f: ∀f:R→R.0·f=0.
@@ -130,7 +130,7 @@ lemma Fmult_zero_f: ∀f:R→R.0·f=0.
  simplify;
  apply f_eq_extensional;
  intro;
- auto.
+ autobatch.
 qed.
 
 lemma Fmult_commutative: symmetric ? Fmult.
@@ -139,7 +139,7 @@ lemma Fmult_commutative: symmetric ? Fmult.
  unfold Fmult;
  apply f_eq_extensional;
  intros;
- auto.
+ autobatch.
 qed.
 
 lemma Fmult_associative: associative ? Fmult.
@@ -149,7 +149,7 @@ lemma Fmult_associative: associative ? Fmult.
  unfold Fmult;
  apply f_eq_extensional;
  intros;
- auto.
+ autobatch.
 qed.
 
 lemma Fmult_Fplus_distr: distributive ? Fmult Fplus.
@@ -160,7 +160,7 @@ lemma Fmult_Fplus_distr: distributive ? Fmult Fplus.
  apply f_eq_extensional;
  intros;
  simplify;
- auto.
+ autobatch.
 qed.
 
 lemma monomio_product:
@@ -173,13 +173,13 @@ lemma monomio_product:
   [ simplify;
     apply f_eq_extensional;
     intro;
-    auto
+    autobatch
   | simplify;
     apply f_eq_extensional;
     intro;
     cut (x\sup (n1+m) = x \sup n1 · x \sup m);
      [ rewrite > Hcut;
-       auto
+       autobatch
      | change in ⊢ (? ? % ?) with ((λx:R.x\sup(n1+m)) x);
        rewrite > H;
        reflexivity
@@ -196,7 +196,7 @@ lemma costante_sum:
  intros;
  elim n;
   [ simplify;
-    auto
+    autobatch
   | simplify;
     clear x;
     clear H;
@@ -205,19 +205,19 @@ lemma costante_sum:
      [ simplify;
        elim m;
         [ simplify;
-          auto
+          autobatch
         | simplify;
           rewrite < H;
-          auto
+          autobatch
         ]
      | simplify;
        rewrite < H;
        clear H;
        elim n;
         [ simplify;
-          auto
+          autobatch
         | simplify;
-          auto
+          autobatch
         ]
      ]
    ].
@@ -251,8 +251,9 @@ alias symbol "times" = "Fmult".
 
 theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n).
  assume n:nat.
- we proceed by induction on n to prove
- (D[x \sup n] = n · x \sup (pred n)).
+ (*we proceed by induction on n to prove
+ (D[x \sup n] = n · x \sup (pred n)).*)
+ elim n 0.
  case O.
    the thesis becomes (D[x \sup 0] = 0·x \sup (pred 0)).
    by _
@@ -276,13 +277,12 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n).
       suppose (0=m) (m_zero). by _ done.
   conclude
      (D[x \sup (1+m)])
-   = (D[x · x \sup m]) by _.
-   = (D[x] · x \sup m + x · D[x \sup m]) by _.
-   = (x \sup m + x · (m · x \sup (pred m))) by _.
-clear H.
-   = (x \sup m + m · (x \sup (1 + pred m))) by _.
-   = (x \sup m + m · x \sup m) by _.
-   = ((1+m) · x \sup m) by _ (timeout=30)
+   = (D[x · x \sup m]).
+   = (D[x] · x \sup m + x · D[x \sup m]).
+   = (x \sup m + x · (m · x \sup (pred m))).
+   = (x \sup m + m · (x \sup (1 + pred m))).
+   = (x \sup m + m · x \sup m).
+   = ((1+m) · x \sup m) by Fmult_one_f Fmult_commutative Fmult_Fplus_distr costante_sum
   done.
 qed.
 
@@ -306,8 +306,8 @@ interpretation "Rderivative" 'derivative f =
 
 theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n.
  assume n:nat.
- we proceed by induction on n to prove
- (D[x \sup (1+n)] = (1+n) · x \sup n).
+ (*we proceed by induction on n to prove
+ (D[x \sup (1+n)] = (1+n) · x \sup n).*) elim n 0.
  case O.
    the thesis becomes (D[x \sup 1] = 1 · x \sup 0).
    by _
@@ -319,11 +319,79 @@ theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n.
    (D[x \sup (2+m)] = (2+m) · x \sup (1+m)).
   conclude
      (D[x \sup (2+m)])
-   = (D[x · x \sup (1+m)]) by _.
-   = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]) by _.
-   = (x \sup (1+m) + x · (costante (1+m) · x \sup m)) by _.
-clear H.
-   = (x \sup (1+m) + costante (1+m) · x \sup (1+m)) by _.
-   = (x \sup (1+m) · (costante (2 + m))) by _
-  done.
-qed.
\ No newline at end of file
+   = (D[x · x \sup (1+m)]).
+   = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]).
+   = (x \sup (1+m) + x · (costante (1+m) · x \sup m)).
+   = (x \sup (1+m) + costante (1+m) · x \sup (1+m)).
+
+
+
+  conclude (x \sup (1+m) + costante (1+m) · x \sup (1+m))
+  = (costante 1 · x \sup (1+m) + costante (1+m) ·(x) \sup (1+m)) proof.
+   by (Fmult_one_f ((x)\sup(1+m)))
+   we proved (costante 1·(x)\sup(1+m)=(x)\sup(1+m)) (previous).
+   by (eq_OF_eq ? ? (λfoo:(R→R).foo+costante (1+m)·(x)\sup(1+m)) (costante 1
+                                                                                                                                                                                                                                       ·(x)\sup(1
+                                                                                                                                                                                                                                                    +m)) ((x)\sup(1
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             +m)) previous)
+   done.
+  = ((x)\sup(1+m)·costante 1+costante (1+m)·(x)\sup(1+m)) proof.
+   by (Fmult_commutative (costante 1) ((x)\sup(1+m)))
+   we proved (costante 1·(x)\sup(1+m)=(x)\sup(1+m)·costante 1) (previous).
+   by (eq_f ? ? (λfoo:(R→R).foo+costante (1+m)·(x)\sup(1+m)) (costante 1
+                                                                                                                                                                                                       ·(x)\sup(1+m)) ((x)\sup(1
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         +m)
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              ·costante
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                1) previous)
+   done.
+  = ((x)\sup(1+m)·costante 1+(x)\sup(1+m)·costante (1+m)) proof.
+   by (Fmult_commutative ((x)\sup(1+m)) (costante (1+m)))
+   we proved ((x)\sup(1+m)·costante (1+m)=costante (1+m)·(x)\sup(1+m))
+    
+   (previous)
+   .
+   by (eq_OF_eq ? ? (λfoo:(R→R).(x)\sup(1+m)·costante 1+foo) ((x)\sup(1+m)
+                                                                                                                                                                                                                               ·costante
+                                                                                                                                                                                                                                 (1+m)) (costante
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        (1
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         +m)
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        ·(x)\sup(1
+                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     +m)) previous)
+   done.
+  = ((x)\sup(1+m)·(costante 1+costante (1+m))) proof.
+   by (Fmult_Fplus_distr ((x)\sup(1+m)) (costante 1) (costante (1+m)))
+   we proved
+   ((x)\sup(1+m)·(costante 1+costante (1+m))
+    =(x)\sup(1+m)·costante 1+(x)\sup(1+m)·costante (1+m))
+    
+   (previous)
+   .
+   by (sym_eq ? ((x)\sup(1+m)·(costante 1+costante (1+m))) ((x)\sup(1+m)
+                                                                                                                                                                            ·costante 1
+                                                                                                                                                                            +(x)\sup(1+m)
+                                                                                                                                                                             ·costante (1+m)) previous)
+   done.
+  = ((costante 1+costante (1+m))·(x)\sup(1+m)) 
+  exact (Fmult_commutative ((x)\sup(1+m)) (costante 1+costante (1+m))).
+  = (costante (1+(1+m))·(x)\sup(1+m)) proof.
+   by (costante_sum 1 (1+m))
+   we proved (costante 1+costante (1+m)=costante (1+(1+m))) (previous).
+   by (eq_f ? ? (λfoo:(R→R).foo·(x)\sup(1+m)) (costante 1+costante (1+m)) (costante
+                                                                                                                                                                                                                                                                                                                              (1
+                                                                                                                                                                                                                                                                                                                               +(1
+                                                                                                                                                                                                                                                                                                                                 +m))) previous)
+   done.
+  = (costante (1+1+m)·(x)\sup(1+m)) proof.
+   by (assoc_plus 1 1 m)
+   we proved (1+1+m=1+(1+m)) (previous).
+   by (eq_OF_eq ? ? (λfoo:nat.costante foo·(x)\sup(1+m)) ? ? previous)
+   done.
+  = (costante (2+m)·(x)\sup(1+m)) proof done.
+   by (plus_n_SO 1)
+   we proved (2=1+1) (previous).
+   by (eq_OF_eq ? ? (λfoo:nat.costante (foo+m)·(x)\sup(1+m)) ? ? previous)
+   done.
+  
+ 
+(* end auto($Revision: 8206 $) proof: TIME=0.06 SIZE=100 DEPTH=100 *)  done.
+qed.