branch for universe

[helm.git] / matita / contribs / library_auto / auto / nat / exp.ma

diff --git a/matita/contribs/library_auto/auto/nat/exp.ma b/matita/contribs/library_auto/auto/nat/exp.ma
new file mode 100644 (file)
index 0000000..69667b7
--- /dev/null
+++ b/matita/contribs/library_auto/auto/nat/exp.ma
@@ -0,0 +1,154 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||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/library_autobatch/nat/exp".
+
+include "auto/nat/div_and_mod.ma".
+
+let rec exp n m on m\def 
+ match m with 
+ [ O \Rightarrow (S O)
+ | (S p) \Rightarrow (times n (exp n p)) ].
+
+interpretation "natural exponent" 'exp a b = (cic:/matita/library_autobatch/nat/exp/exp.con a b).
+
+theorem exp_plus_times : \forall n,p,q:nat. 
+n \sup (p + q) = (n \sup p) * (n \sup q).
+intros.
+elim p;simplify;autobatch.
+(*[ rewrite < plus_n_O.
+  reflexivity
+| rewrite > H.
+  symmetry.
+  apply assoc_times
+]*)
+qed.
+
+theorem exp_n_O : \forall n:nat. S O = n \sup O.
+intro.
+autobatch.
+(*simplify.
+reflexivity.*)
+qed.
+
+theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
+intro.
+autobatch.
+(*simplify.
+rewrite < times_n_SO.
+reflexivity.*)
+qed.
+
+theorem exp_exp_times : \forall n,p,q:nat. 
+(n \sup p) \sup q = n \sup (p * q).
+intros.
+elim q;simplify
+[ autobatch.
+  (*rewrite < times_n_O.
+  simplify.
+  reflexivity*)
+| rewrite > H.
+  rewrite < exp_plus_times.
+  autobatch
+  (*rewrite < times_n_Sm.
+  reflexivity*)
+]
+qed.
+
+theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
+intros.
+elim m;simplify;autobatch.
+                (*unfold lt
+[ apply le_n
+| rewrite > times_n_SO.
+  apply le_times;assumption
+]*)
+qed.
+
+theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
+intros.
+elim m;simplify;unfold lt;
+[ apply le_n.
+| apply (trans_le ? ((S(S O))*(S n1)))
+  [ simplify.
+    rewrite < plus_n_Sm.    
+    apply le_S_S.
+    autobatch
+    (*apply le_S_S.
+    rewrite < sym_plus.
+    apply le_plus_n*)
+  | autobatch
+    (*apply le_times;assumption*)
+  ]
+]
+qed.
+
+theorem exp_to_eq_O: \forall n,m:nat. (S O) < n 
+\to n \sup m = (S O) \to m = O.
+intros.
+apply antisym_le
+[ apply le_S_S_to_le.
+  rewrite < H1.
+  autobatch
+  (*change with (m < n \sup m).
+  apply lt_m_exp_nm.
+  assumption*)
+| apply le_O_n
+]
+qed.
+
+theorem injective_exp_r: \forall n:nat. (S O) < n \to 
+injective nat nat (\lambda m:nat. n \sup m).
+simplify.
+intros 4.
+apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y))
+[ intros.
+  autobatch
+  (*apply sym_eq.
+  apply (exp_to_eq_O n)
+  [ assumption
+  | rewrite < H1.
+    reflexivity
+  ]*)
+| intros.
+  apply (exp_to_eq_O n);assumption
+| intros.
+  apply eq_f.
+  apply H1.
+  (* esprimere inj_times senza S *)
+  cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b)
+  [ apply Hcut
+    [ autobatch
+      (*simplify.
+      unfold lt.
+      apply le_S_S_to_le. 
+      apply le_S. 
+      assumption*)
+    | (*NB qui autobatch non chiude il goal, chiuso invece chiamando solo la tattica assumption*)
+      assumption
+    ]
+  | intros 2.
+    apply (nat_case n);intros;autobatch
+    (*[ apply False_ind.
+      apply (not_le_Sn_O O H3)
+    | apply (inj_times_r m1).
+      assumption
+    ]*)
+  ]
+]
+qed.
+
+variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
+p \sup n = p \sup m \to n = m \def
+injective_exp_r.