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.
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.
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.
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.
(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.
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.