X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Flibrary_auto%2Fauto%2Fnat%2Fcount.ma;fp=matita%2Fcontribs%2Flibrary_auto%2Fauto%2Fnat%2Fcount.ma;h=de2e52807c201a6e336b15954afbeb4be8095da0;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/library_auto/auto/nat/count.ma b/matita/contribs/library_auto/auto/nat/count.ma
new file mode 100644
index 000000000..de2e52807
--- /dev/null
+++ b/matita/contribs/library_auto/auto/nat/count.ma
@@ -0,0 +1,347 @@
+(**************************************************************************)
+(*       __                                                               *)
+(*      ||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/count".
+
+include "auto/nat/relevant_equations.ma".
+include "auto/nat/sigma_and_pi.ma".
+include "auto/nat/permutation.ma".
+
+theorem sigma_f_g : \forall n,m:nat.\forall f,g:nat \to nat.
+sigma n (\lambda p.f p + g p) m = sigma n f m + sigma n g m.
+intros.
+elim n;simplify
+[ reflexivity
+| rewrite > H.
+  autobatch
+  (*rewrite > assoc_plus.
+  rewrite < (assoc_plus (g (S (n1+m)))).
+  rewrite > (sym_plus (g (S (n1+m)))).
+  rewrite > (assoc_plus (sigma n1 f m)).
+  rewrite < assoc_plus.
+  reflexivity*)
+]
+qed.
+
+theorem sigma_plus: \forall n,p,m:nat.\forall f:nat \to nat.
+sigma (S (p+n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
+intros. 
+elim p;simplify
+[ autobatch
+  (*rewrite < (sym_plus n m).
+  reflexivity*)
+| rewrite > assoc_plus in \vdash (? ? ? %).
+  rewrite < H.
+  autobatch
+  (*simplify.
+  rewrite < plus_n_Sm.
+  rewrite > (sym_plus n).
+  rewrite > assoc_plus.
+  rewrite < (sym_plus m).
+  rewrite < (assoc_plus n1).
+  reflexivity*)
+]
+qed.
+
+theorem sigma_plus1: \forall n,p,m:nat.\forall f:nat \to nat.
+sigma (p+(S n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
+intros.
+elim p;simplify
+[ reflexivity
+| rewrite > assoc_plus in \vdash (? ? ? %).
+  rewrite < H.
+  rewrite < plus_n_Sm.
+  autobatch
+  (*rewrite < plus_n_Sm.simplify.
+  rewrite < (sym_plus n).
+  rewrite > assoc_plus.
+  rewrite < (sym_plus m).
+  rewrite < (assoc_plus n).
+  reflexivity*)
+]
+qed.
+
+theorem eq_sigma_sigma : \forall n,m:nat.\forall f:nat \to nat.
+sigma (pred ((S n)*(S m))) f O =
+sigma m (\lambda a.(sigma n (\lambda b.f (b*(S m) + a)) O)) O.
+intro.
+elim n;simplify
+[ rewrite < plus_n_O.
+  apply eq_sigma.  
+  intros.
+  reflexivity
+| rewrite > sigma_f_g.
+  rewrite < plus_n_O.
+  rewrite < H.
+  autobatch
+  
+  (*rewrite > (S_pred ((S n1)*(S m)))
+  [ apply sigma_plus1
+  | simplify.
+    unfold lt.
+    apply le_S_S.
+    apply le_O_n
+  ]*)
+]
+qed.
+
+theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat.
+sigma (pred ((S n)*(S m))) f O =
+sigma n (\lambda a.(sigma m (\lambda b.f (b*(S n) + a)) O)) O.
+intros.
+rewrite > sym_times.
+apply eq_sigma_sigma.
+qed.
+
+theorem sigma_times: \forall n,m,p:nat.\forall f:nat \to nat.
+(sigma n f m)*p = sigma n (\lambda i.(f i) * p) m.
+intro.
+elim n;simplify
+[ reflexivity
+| rewrite < H.
+  apply times_plus_l
+]
+qed.
+
+definition bool_to_nat: bool \to nat \def
+\lambda b. match b with
+[ true \Rightarrow (S O)
+| false \Rightarrow O ].
+
+theorem bool_to_nat_andb: \forall a,b:bool.
+bool_to_nat (andb a b) = (bool_to_nat a)*(bool_to_nat b).
+intros. 
+elim a;autobatch.
+(*[elim b
+  [ simplify.
+    reflexivity
+  | reflexivity
+  ] 
+| reflexivity
+]*)
+qed.
+
+definition count : nat \to (nat \to bool) \to nat \def
+\lambda n.\lambda f. sigma (pred n) (\lambda n.(bool_to_nat (f n))) O.
+
+theorem count_times:\forall n,m:nat. 
+\forall f,f1,f2:nat \to bool.
+\forall g:nat \to nat \to nat. 
+\forall g1,g2: nat \to nat.
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
+(count ((S n)*(S m)) f) = (count (S n) f1)*(count (S m) f2).
+intros.unfold count.
+rewrite < eq_map_iter_i_sigma.
+rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? 
+           (\lambda i.g (div i (S n)) (mod i (S n))))
+[ rewrite > eq_map_iter_i_sigma.
+  rewrite > eq_sigma_sigma1.
+  apply (trans_eq ? ?
+  (sigma n (\lambda a.
+    sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O))
+  [ apply eq_sigma.intros.
+    apply eq_sigma.intros.
+    rewrite > (div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) 
+                                          ((i1*(S n) + i) \mod (S n)) i1 i)
+    [ rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) 
+                                           ((i1*(S n) + i) \mod (S n)) i1 i)
+      [ rewrite > H3;autobatch (*qui autobatch impiega parecchio tempo*)
+        (*[ apply bool_to_nat_andb
+        | unfold lt.
+          apply le_S_S.
+          assumption
+        | unfold lt.
+          apply le_S_S.
+          assumption
+        ]*)
+      | autobatch
+        (*apply div_mod_spec_div_mod.
+        unfold lt.
+        apply le_S_S.
+        apply le_O_n*)
+      | constructor 1;autobatch
+        (*[ unfold lt.
+          apply le_S_S.
+          assumption
+        | reflexivity
+        ]*)
+      ]  
+    | autobatch
+      (*apply div_mod_spec_div_mod.
+      unfold lt.
+      apply le_S_S.
+      apply le_O_n*)
+    | constructor 1;autobatch
+      (*[ unfold lt.
+        apply le_S_S.
+        assumption
+      | reflexivity
+      ]*)
+    ]
+  | apply (trans_eq ? ? 
+    (sigma n (\lambda n.((bool_to_nat (f1 n)) *
+    (sigma m (\lambda n.bool_to_nat (f2 n)) O))) O))
+    [ apply eq_sigma.
+      intros.
+      autobatch
+      (*rewrite > sym_times.
+      apply (trans_eq ? ? 
+      (sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O))
+      [ reflexivity.
+      | apply sym_eq. 
+        apply sigma_times
+      ]*)
+    | autobatch
+      (*simplify.
+      apply sym_eq. 
+      apply sigma_times*)
+    ]
+  ]
+| unfold permut.
+  split
+  [ intros.
+    rewrite < plus_n_O.
+    apply le_S_S_to_le.
+    rewrite < S_pred in \vdash (? ? %)
+    [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
+      apply H
+      [ autobatch
+        (*apply lt_mod_m_m.
+        unfold lt. 
+        apply le_S_S.
+        apply le_O_n*)
+      | apply (lt_times_to_lt_l n).
+        apply (le_to_lt_to_lt ? i)
+        [ autobatch
+          (*rewrite > (div_mod i (S n)) in \vdash (? ? %)
+          [ rewrite > sym_plus.
+            apply le_plus_n
+          | unfold lt. 
+            apply le_S_S.
+            apply le_O_n
+          ]*)
+        | unfold lt.       
+          rewrite > S_pred in \vdash (? ? %)
+          [ apply le_S_S.
+            autobatch
+            (*rewrite > plus_n_O in \vdash (? ? %).
+            rewrite > sym_times. 
+            assumption*)
+          | autobatch
+            (*rewrite > (times_n_O O).
+            apply lt_times;
+            unfold lt;apply le_S_S;apply le_O_n*)            
+          ]
+        ]
+      ]
+    | autobatch
+      (*rewrite > (times_n_O O).
+      apply lt_times;
+      unfold lt;apply le_S_S;apply le_O_n *)     
+    ]
+  | rewrite < plus_n_O.
+    unfold injn.
+    intros.
+    cut (i < (S n)*(S m))
+    [ cut (j < (S n)*(S m))
+      [ cut ((i \mod (S n)) < (S n))
+        [ cut ((i/(S n)) < (S m))
+          [ cut ((j \mod (S n)) < (S n))
+            [ cut ((j/(S n)) < (S m))
+              [ rewrite > (div_mod i (S n))
+                [ rewrite > (div_mod j (S n))
+                  [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
+                    rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
+                    rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
+                    rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
+                    autobatch
+                    (*rewrite > H6.
+                    reflexivity*)
+                  | autobatch                 
+                    (*unfold lt. 
+                    apply le_S_S.
+                    apply le_O_n*)
+                  ]
+                | autobatch
+                  (*unfold lt. 
+                  apply le_S_S.
+                  apply le_O_n*)
+                ]
+              | apply (lt_times_to_lt_l n).
+                apply (le_to_lt_to_lt ? j)
+                [ autobatch.
+                  (*rewrite > (div_mod j (S n)) in \vdash (? ? %)
+                  [ rewrite > sym_plus.
+                    apply le_plus_n
+                  | unfold lt. 
+                    apply le_S_S.
+                    apply le_O_n
+                  ]*)
+                | rewrite < sym_times. 
+                  assumption
+                ]
+              ]
+            | autobatch
+              (*apply lt_mod_m_m.
+              unfold lt. apply le_S_S.
+              apply le_O_n*)
+            ]
+          | apply (lt_times_to_lt_l n).
+            apply (le_to_lt_to_lt ? i)
+            [ autobatch 
+              (*rewrite > (div_mod i (S n)) in \vdash (? ? %)
+              [ rewrite > sym_plus.
+                apply le_plus_n
+              | unfold lt. 
+                apply le_S_S.
+                apply le_O_n
+              ]*)
+            | rewrite < sym_times.
+              assumption
+            ]
+          ]
+        | autobatch
+          (*apply lt_mod_m_m.
+          unfold lt. apply le_S_S.
+          apply le_O_n*)
+        ]
+      | unfold lt.
+        autobatch
+        (*rewrite > S_pred in \vdash (? ? %)
+        [ apply le_S_S.
+          assumption
+        | rewrite > (times_n_O O).
+          apply lt_times;
+            unfold lt; apply le_S_S;apply le_O_n        
+        ]*)
+      ]
+    | unfold lt.
+      autobatch
+      (*rewrite > S_pred in \vdash (? ? %)
+      [ apply le_S_S.
+        assumption
+      | rewrite > (times_n_O O).
+        apply lt_times;
+          unfold lt; apply le_S_S;apply le_O_n        
+      ]*)
+    ]
+  ]
+| intros.
+  apply False_ind.
+  apply (not_le_Sn_O m1 H4)
+]
+qed.