exp and factorial

diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
new file mode 100644 (file)
index 0000000..1c7adf6
--- /dev/null
+++ b/matita/matita/lib/arithmetics/exp.ma
@@ -0,0 +1,140 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/div_and_mod.ma".
+
+let rec exp n m on m ≝ 
+ match m with 
+ [ O ⇒ 1
+ | S p ⇒ (exp n p) * n].
+
+interpretation "natural exponent" 'exp a b = (exp a b).
+
+theorem exp_plus_times : ∀n,p,q:nat. 
+  n^(p + q) = n^p * n^q.
+#n #p #q elim p normalize //
+qed.
+
+theorem exp_n_O : ∀n:nat. 1 = n^O. 
+//
+qed.
+
+theorem exp_n_1 : ∀n:nat. n = n^1. 
+#n normalize //
+qed.
+
+theorem exp_1_n : ∀n:nat. 1 = 1^n.
+#n (elim n) normalize //
+qed.
+
+theorem exp_2: ∀n. n^2 = n*n. 
+#n normalize //
+qed.
+
+theorem exp_exp_times : ∀n,p,q:nat. 
+  (n^p)^q = n^(p * q).
+#n #p #q (elim q) normalize 
+(* [applyS exp_n_O funziona ma non lo trova *)
+// <times_n_O // 
+qed.
+
+theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m. 
+#n #m (elim m) normalize // #a #Hind #posn 
+@(le_times 1 ? 1) /2/
+qed.
+
+theorem lt_m_exp_nm: ∀n,m:nat. 1 < n → m < n^m.
+#n #m #lt1n (elim m) normalize // 
+#n #Hind @(transitive_le ? ((S n)*2)) // @le_times //
+qed.
+
+theorem exp_to_eq_O: ∀n,m:nat. 1 < n → 
+  n^m = 1 → m = O.
+#n #m #ltin #eq1 @le_to_le_to_eq //
+@le_S_S_to_le <eq1 @lt_m_exp_nm //
+qed.
+
+theorem injective_exp_r: ∀b:nat. 1 < b → 
+  injective nat nat (λi:nat. b^i).
+#b #lt1b @nat_elim2 normalize 
+  [#n #H @sym_eq @(exp_to_eq_O b n lt1b) //
+  |#n #H @False_ind @(absurd (1 < 1) ? (not_le_Sn_n 1))
+   <H in ⊢ (??%) @(lt_to_le_to_lt ? (1*b)) //
+   @le_times // @lt_O_exp /2/
+  |#n #m #Hind #H @eq_f @Hind @(injective_times_l … H) /2/
+  ]
+qed.
+
+theorem le_exp: ∀n,m,p:nat. O < p →
+  n ≤m → p^n ≤ p^m.
+@nat_elim2 
+  [#n #m #ltm #len @lt_O_exp //
+  |#n #m #_ #len @False_ind /2/
+  |#n #m #Hind #p #posp #lenm normalize @le_times //
+   @Hind /2/
+  ]
+qed.
+
+theorem le_exp1: ∀n,m,a:nat. O < a →
+  n ≤m → n^a ≤ m^a.
+#n #m #a #posa #lenm (elim posa) //
+#a #posa #Hind @le_times //
+qed.
+
+theorem lt_exp: ∀n,m,p:nat. 1 < p → 
+  n < m → p^n < p^m.
+#n #m #p #lt1p #ltnm 
+cut (p \sup n ≤ p \sup m) [@le_exp /2/] #H 
+cases(le_to_or_lt_eq … H) // #eqexp
+@False_ind @(absurd (n=m)) /2/
+qed.
+
+theorem lt_exp1: ∀n,m,p:nat. 0 < p → 
+  n < m → n^p < m^p.
+#n #m #p #posp #ltnm (elim posp) //
+#p #posp #Hind @lt_times //
+qed.
+  
+theorem le_exp_to_le: 
+∀b,n,m. 1 < b → b^n ≤ b^m → n ≤ m.
+#b #n #m #lt1b #leexp cases(decidable_le n m) //
+#notle @False_ind @(absurd … leexp) @lt_to_not_le
+@lt_exp /2/
+qed.
+
+theorem le_exp_to_le1 : ∀n,m,p.O < p → 
+  n^p ≤ m^p → n ≤ m.
+#n #m #p #posp #leexp @not_lt_to_le 
+@(not_to_not … (lt_exp1 ??? posp)) @le_to_not_lt // 
+qed.
+     
+theorem lt_exp_to_lt: 
+∀a,n,m. 0 < a → a^n < a^m → n < m.
+#a #n #m #lt1a #ltexp cases(decidable_le (S n) m) //
+#H @False_ind @(absurd … ltexp) @le_to_not_lt 
+@le_exp // @not_lt_to_le @H
+qed.
+
+theorem lt_exp_to_lt1: 
+∀a,n,m. O < a → n^a < m^a → n < m.
+#a #n #m #posa #ltexp cases(decidable_le (S n) m) //
+#H @False_ind @(absurd … ltexp) @le_to_not_lt 
+@le_exp1 // @not_lt_to_le @H 
+qed.
+     
+theorem times_exp: ∀n,m,p. 
+  n^p * m^p = (n*m)^p.
+#n #m #p (elim p) // #p #Hind normalize //
+qed.
+
+  
+   
+   
\ No newline at end of file

diff --git a/matita/matita/lib/arithmetics/factorial.ma b/matita/matita/lib/arithmetics/factorial.ma
new file mode 100644 (file)
index 0000000..fc7b7de
--- /dev/null
+++ b/matita/matita/lib/arithmetics/factorial.ma
@@ -0,0 +1,196 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/exp.ma".
+
+let rec fact n ≝
+  match n with 
+  [ O ⇒ 1
+  | S m ⇒ fact m * S m].
+
+interpretation "factorial" 'fact n = (fact n).
+
+theorem le_1_fact : ∀n. 1 ≤ n!.
+#n (elim n) normalize /2/ 
+qed.
+
+theorem le_2_fact : ∀n. 1 < n → 2 ≤ n!.
+#n (cases n)
+  [#abs @False_ind /2/
+  |#m normalize #le2 @(le_times 1 ? 2) //
+  ]
+qed.
+
+theorem le_n_fact_n: ∀n. n ≤ n!.
+#n (elim n) normalize //
+#n #Hind @(transitive_le ? (1*(S n))) // @le_times //
+qed.
+
+theorem lt_n_fact_n: ∀n. 2 < n → n < n!.
+#n (cases n) 
+  [#H @False_ind /2/ 
+  |#m #lt2 normalize @(lt_to_le_to_lt ? (2*(S m))) //
+   @le_times // @le_2_fact /2/ 
+qed.
+
+(* approximations *)
+
+theorem fact_to_exp1: ∀n.O<n →
+ (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
+#n #posn (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H (elim posn) //
+#n #posn #Hind @(transitive_le ? ((2*n)!*(2*(S n))*(2*(S n))))
+  [>H normalize @le_times //
+  |cut (pred (2*(S n)) = S(S(pred(2*n))))
+    [>S_pred // @(le_times 1 ? 1) //] #H1
+   cut (2^(pred (2*(S n))) = 2^(pred(2*n))*2*2) 
+    [>H1 >H1 //] #H2 >H2
+   @(transitive_le ? ((2^(pred (2*n))) * n! * n! *(2*(S n))*(2*(S n))))
+    [@le_times[@le_times //]//
+    (* we generalize to hide the computational content *)
+    |normalize in match ((S n)!) generalize in match (S n)
+     #Sn generalize in match 2 #two //
+    ]
+  ]
+qed.  
+
+theorem fact_to_exp: ∀n.
+ (2*n)! ≤ (2^(pred (2*n))) * n! * n!.
+#n (cases n) [normalize // |#n @fact_to_exp1 //]
+qed.
+
+theorem exp_to_fact1: ∀n.O < n →
+  2^(2*n)*n!*n! < (S(2*n))!.
+#n #posn (elim posn) [normalize //]
+#n #posn #Hind (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H
+cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1
+@(le_to_lt_to_lt ? (2^(2*n)*n!*n!*(2*(S n))*(2*(S n))))
+  [normalize in match ((S n)!) generalize in match (S n) #Sn
+   generalize in match 2 #two //
+  |cut ((S(2*(S n)))! = (S(2*n))!*(S(S(2*n)))*(S(S(S(2*n)))))
+   [>H //] #H2 >H2 @lt_to_le_to_lt_times
+     [@lt_to_le_to_lt_times //|>H // | //]
+  ]
+qed.
+     
+(* a slightly better result 
+theorem fact3: \forall n.O < n \to
+(exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n).
+intros.
+elim H
+  [simplify.apply le_n
+  |rewrite > times_SSO.
+   rewrite > factS.
+   rewrite < times_exp.
+   change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))).
+   rewrite > assoc_times.
+   rewrite > assoc_times in ⊢ (? (? ? %) ?).
+   rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
+   rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?).
+   rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?).
+   apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!))))))
+    [apply le_times_r.
+     apply le_times_r.
+     apply le_times_r.
+     assumption
+    |rewrite > factS.
+     rewrite > factS.
+     rewrite < times_SSO.
+     rewrite > assoc_times in ⊢ (? ? %). 
+     apply le_times_r.
+     rewrite < assoc_times.
+     change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))).
+     rewrite < assoc_times in ⊢ (? (? % ?) ?).
+     rewrite < times_n_SO.
+     rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
+     rewrite < assoc_times in ⊢ (? ? %).
+     rewrite < assoc_times in ⊢ (? ? (? % ?)).
+     apply le_times_r.
+     apply le_times_l.
+     apply le_S.apply le_n
+    ]
+  ]
+qed.
+
+theorem le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5).
+simplify in \vdash (? (? %) ?).
+rewrite > factS in \vdash (? % ?).
+rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?).
+rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
+rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
+rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?).
+apply le_times_l.
+apply leb_true_to_le.reflexivity.
+qed.
+
+theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d).
+intros.
+rewrite > assoc_times.
+rewrite > assoc_times.
+apply eq_f.
+rewrite < assoc_times.
+rewrite < assoc_times.
+rewrite > sym_times in \vdash (? ? (? % ?) ?).
+reflexivity.
+qed.
+
+(* an even better result *)
+theorem lt_SSSSO_to_fact: \forall n.4<n \to
+fact (2*n) \le (exp 2 ((2*n)-2))*(fact n)*(fact n).
+intros.elim H
+  [apply le_fact_10
+  |rewrite > times_SSO.
+   change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O);
+   rewrite < minus_n_O.
+   rewrite > factS.
+   rewrite > factS.
+   rewrite < assoc_times.
+   rewrite > factS.
+   apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1))))
+    [apply le_times_l.
+     rewrite > times_SSO.
+     apply le_times_r.
+     apply le_n_Sn
+    |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!)))
+      [apply le_times_r.assumption
+      |rewrite > assoc_times.
+       rewrite > ab_times_cd in \vdash (? (? ? %) ?).
+       rewrite < assoc_times.
+       apply le_times_l.
+       rewrite < assoc_times in \vdash (? (? ? %) ?).
+       rewrite > ab_times_cd.
+       apply le_times_l.
+       rewrite < exp_S.
+       rewrite < exp_S.
+       apply le_exp
+        [apply lt_O_S
+        |rewrite > eq_minus_S_pred.
+         rewrite < S_pred
+          [rewrite > eq_minus_S_pred.
+           rewrite < S_pred
+            [rewrite < minus_n_O.
+             apply le_n
+            |elim H1;simplify
+              [apply lt_O_S
+              |apply lt_O_S
+              ]
+            ]
+          |elim H1;simplify
+            [apply lt_O_S
+            |rewrite < plus_n_Sm.
+             rewrite < minus_n_O.
+             apply lt_O_S
+            ]
+          ]
+        ]
+      ]
+    ]
+  ]
+qed. *)