Committing all the recent development of Andrea after the merge between his

[helm.git] / helm / matita / library / nat / exp.ma

diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
new file mode 100644 (file)
index 0000000..c0d3637
--- /dev/null
+++ b/helm/matita/library/nat/exp.ma
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/exp".
+
+include "nat/times.ma". 
+
+let rec exp n m on m\def 
+ match m with 
+ [ O \Rightarrow (S O)
+ | (S p) \Rightarrow (times n (exp n p)) ].
+
+theorem exp_plus_times : \forall n,p,q:nat. 
+eq nat (exp n (plus p q)) (times (exp n p) (exp n q)).
+intros.elim p.
+simplify.rewrite < plus_n_O.reflexivity.
+simplify.rewrite > H.symmetry.
+apply assoc_times.
+qed.
+
+theorem exp_n_O : \forall n:nat. eq nat (S O) (exp n O).
+intro.simplify.reflexivity.
+qed.
+
+theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)).
+intro.simplify.rewrite < times_n_SO.reflexivity.
+qed.
+
+theorem bad : \forall n,p,q:nat. 
+eq nat (exp (exp n p) q) (exp n (times p q)).
+intros.
+elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
+simplify.rewrite > H.rewrite < exp_plus_times.
+rewrite < times_n_Sm.reflexivity.
+qed.
\ No newline at end of file