X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fcount.ma;h=20913fa6041c103527cfd73e7a5c7708b15924de;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b1cb31cf36c35723b25240620a2b772b50988515;hpb=65312e560c25b49336241762107e401e7f9c5c3c;p=helm.git diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma index b1cb31cf3..20913fa60 100644 --- a/helm/matita/library/nat/count.ma +++ b/helm/matita/library/nat/count.ma @@ -24,9 +24,9 @@ intros.elim n. simplify.reflexivity. simplify.rewrite > H. 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 (g (S (n1+m)))). +rewrite > (sym_plus (g (S (n1+m)))). +rewrite > (assoc_plus (sigma n1 f m)). rewrite < assoc_plus. reflexivity. qed. @@ -35,16 +35,16 @@ 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. -rewrite < sym_plus n m.reflexivity. +rewrite < (sym_plus n m).reflexivity. simplify. rewrite > assoc_plus in \vdash (? ? ? %). rewrite < H. simplify. rewrite < plus_n_Sm. -rewrite > sym_plus n. +rewrite > (sym_plus n). rewrite > assoc_plus. -rewrite < sym_plus m. -rewrite < assoc_plus n1. +rewrite < (sym_plus m). +rewrite < (assoc_plus n1). reflexivity. qed. @@ -57,10 +57,10 @@ rewrite > assoc_plus in \vdash (? ? ? %). rewrite < H. rewrite < plus_n_Sm. rewrite < plus_n_Sm.simplify. -rewrite < sym_plus n. +rewrite < (sym_plus n). rewrite > assoc_plus. -rewrite < sym_plus m. -rewrite < assoc_plus n. +rewrite < (sym_plus m). +rewrite < (assoc_plus n). reflexivity. qed. @@ -71,14 +71,14 @@ intro.elim n.simplify. rewrite < plus_n_O. apply eq_sigma.intros.reflexivity. change with -sigma (m+(S n1)*(S m)) f O = -sigma m (\lambda a.(f ((S(n1+O))*(S m)+a)) + (sigma n1 (\lambda b.f (b*(S m)+a)) O)) O. +(sigma (m+(S n1)*(S m)) f O = +sigma m (\lambda a.(f ((S(n1+O))*(S m)+a)) + (sigma n1 (\lambda b.f (b*(S m)+a)) O)) O). rewrite > sigma_f_g. rewrite < plus_n_O. rewrite < H. -rewrite > S_pred ((S n1)*(S m)). +rewrite > (S_pred ((S n1)*(S m))). apply sigma_plus1. -simplify.apply le_S_S.apply le_O_n. +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. @@ -123,36 +123,39 @@ theorem count_times:\forall n,m:nat. (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 > (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 ? ? +apply (trans_eq ? ? (sigma n (\lambda a. - sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O). + 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 > (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. apply bool_to_nat_andb. -simplify.apply le_S_S.assumption. -simplify.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. +unfold lt.apply le_S_S.assumption. apply div_mod_spec_div_mod. -simplify.apply le_S_S.apply le_O_n. -constructor 1.simplify.apply le_S_S.assumption. +unfold lt.apply le_S_S.apply le_O_n. +constructor 1.unfold lt.apply le_S_S.assumption. reflexivity. apply div_mod_spec_div_mod. -simplify.apply le_S_S.apply le_O_n. -constructor 1.simplify.apply le_S_S.assumption. +unfold lt.apply le_S_S.apply le_O_n. +constructor 1.unfold lt.apply le_S_S.assumption. reflexivity. -apply trans_eq ? ? +apply (trans_eq ? ? (sigma n (\lambda n.((bool_to_nat (f1 n)) * -(sigma m (\lambda n.bool_to_nat (f2 n)) O))) O). +(sigma m (\lambda n.bool_to_nat (f2 n)) O))) O)). apply eq_sigma. intros. rewrite > sym_times. -apply trans_eq ? ? -(sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O). +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. change in match (pred (S n)) with n. @@ -167,77 +170,77 @@ rewrite < S_pred in \vdash (? ? %). change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)). apply H. apply lt_mod_m_m. -simplify. apply le_S_S.apply le_O_n. -apply lt_times_to_lt_l n. -apply le_to_lt_to_lt ? i. -rewrite > div_mod i (S n) in \vdash (? ? %). +unfold lt. apply le_S_S.apply le_O_n. +apply (lt_times_to_lt_l n). +apply (le_to_lt_to_lt ? i). +rewrite > (div_mod i (S n)) in \vdash (? ? %). rewrite > sym_plus. apply le_plus_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. unfold lt. rewrite > S_pred in \vdash (? ? %). apply le_S_S. rewrite > plus_n_O in \vdash (? ? %). rewrite > sym_times. assumption. -rewrite > times_n_O O. +rewrite > (times_n_O O). apply lt_times. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. -rewrite > times_n_O O. +unfold lt. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +rewrite > (times_n_O O). apply lt_times. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +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 (? ? ? (? % ?)). +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 (? ? ? (? % ?)). rewrite > H6.reflexivity. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. -apply lt_times_to_lt_l n. -apply le_to_lt_to_lt ? j. -rewrite > div_mod j (S n) in \vdash (? ? %). +unfold lt. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +apply (lt_times_to_lt_l n). +apply (le_to_lt_to_lt ? j). +rewrite > (div_mod j (S n)) in \vdash (? ? %). rewrite > sym_plus. apply le_plus_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. rewrite < sym_times. assumption. apply lt_mod_m_m. -simplify. apply le_S_S.apply le_O_n. -apply lt_times_to_lt_l n. -apply le_to_lt_to_lt ? i. -rewrite > div_mod i (S n) in \vdash (? ? %). +unfold lt. apply le_S_S.apply le_O_n. +apply (lt_times_to_lt_l n). +apply (le_to_lt_to_lt ? i). +rewrite > (div_mod i (S n)) in \vdash (? ? %). rewrite > sym_plus. apply le_plus_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. rewrite < sym_times. assumption. apply lt_mod_m_m. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. unfold lt. rewrite > S_pred in \vdash (? ? %). apply le_S_S.assumption. -rewrite > times_n_O O. +rewrite > (times_n_O O). apply lt_times. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. unfold lt. rewrite > S_pred in \vdash (? ? %). apply le_S_S.assumption. -rewrite > times_n_O O. +rewrite > (times_n_O O). apply lt_times. -simplify. apply le_S_S.apply le_O_n. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. intros. apply False_ind. -apply not_le_Sn_O m1 H4. +apply (not_le_Sn_O m1 H4). qed.