1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/map_iter_p.ma".
17 include "nat/permutation.ma".
18 include "nat/count.ma".
20 let rec map_iter_p n p (g:nat \to nat) (a:nat) f \def
25 [true \Rightarrow f (g (S k)) (map_iter_p k p g a f)
26 |false \Rightarrow map_iter_p k p g a f]
29 theorem eq_map_iter_p: \forall g1,g2:nat \to nat.
30 \forall p:nat \to bool.
31 \forall f:nat \to nat \to nat. \forall a,n:nat.
32 (\forall m:nat. m \le n \to g1 m = g2 m) \to
33 map_iter_p n p g1 a f = map_iter_p n p g2 a f.
35 [simplify.reflexivity.
36 |simplify.elim (p (S n1))
39 |simplify.apply H.intros.apply H1.
42 |simplify.apply H.intros.apply H1.
48 (* useful since simplify simpifies too much *)
50 theorem map_iter_p_O: \forall p.\forall g.\forall f. \forall a:nat.
51 map_iter_p O p g a f = a.
52 intros.simplify.reflexivity.
55 theorem map_iter_p_S_true: \forall p.\forall g.\forall f. \forall a,n:nat.
57 map_iter_p (S n) p g a f = f (g (S n)) (map_iter_p n p g a f).
58 intros.simplify.rewrite > H.reflexivity.
61 theorem map_iter_p_S_false: \forall p.\forall g.\forall f. \forall a,n:nat.
63 map_iter_p (S n) p g a f = map_iter_p n p g a f.
64 intros.simplify.rewrite > H.reflexivity.
67 (* map_iter examples *)
68 definition pi_p \def \lambda p. \lambda n.
69 map_iter_p n p (\lambda n.n) (S O) times.
71 lemma pi_p_S: \forall n.\forall p.
74 [true \Rightarrow (S n)*(pi_p p n)
75 |false \Rightarrow (pi_p p n)
80 lemma lt_O_pi_p: \forall n.\forall p.
86 [change with (O < (S n1)*(pi_p p n1)).
87 rewrite >(times_n_O n1).
88 apply lt_times[apply le_n|assumption]
98 (bool_to_nat (p (S m))) + (card m p)].
100 lemma count_card: \forall p.\forall n.
101 p O = false \to count (S n) p = card n p.
103 [simplify.rewrite > H. reflexivity
106 apply eq_f.assumption
110 lemma count_card1: \forall p.\forall n.
111 p O = false \to p n = false \to count n p = card n p.
112 intros 3.apply (nat_case n)
113 [intro.simplify.rewrite > H. reflexivity
114 |intros.rewrite > (count_card ? ? H).
115 simplify.rewrite > H1.reflexivity
119 lemma a_times_pi_p: \forall p. \forall a,n.
120 exp a (card n p) * pi_p p n = map_iter_p n p (\lambda n.a*n) (S O) times.
122 [simplify.reflexivity
123 |simplify.apply (bool_elim ? (p (S n1)))
126 (a*exp a (card n1 p) * ((S n1) * (pi_p p n1)) =
127 a*(S n1)*map_iter_p n1 p (\lambda n.a*n) (S O) times).
135 definition permut_p \def \lambda f. \lambda p:nat\to bool. \lambda n.
136 \forall i. i \le n \to p i = true \to ((f i \le n \land p (f i) = true)
137 \land (\forall j. p j = true \to j \le n \to i \neq j \to (f i \neq f j))).
139 definition extentional_eq_n \def \lambda f,g:nat \to nat.\lambda n.
140 \forall x. x \le n \to f x = g x.
142 lemma extentional_eq_n_to_permut_p: \forall f,g. \forall p. \forall n.
143 extentional_eq_n f g n\to permut_p f p n \to permut_p g p n.
144 intros.unfold permut_p.
149 [rewrite < (H i H2).assumption
150 |rewrite < (H i H2).assumption
153 unfold.intro.apply (H5 j H6 H7 H8).
155 rewrite > (H j H7).assumption
159 theorem permut_p_compose: \forall f,g.\forall p.\forall n.
160 permut_p f p n \to permut_p g p n \to permut_p (compose ? ? ? g f) p n.
161 intros.unfold permut_p.intros.
164 elim (H1 (f i) H6 H7).
168 [unfold compose.assumption
169 |unfold compose.rewrite < H11.reflexivity
174 [elim (H j H13 H12).elim H15.rewrite < H18.reflexivity
175 |elim (H j H13 H12).elim H15.assumption.
176 |apply (H5 j H12 H13 H14)
181 theorem permut_p_S_to_permut_p: \forall f.\forall p.\forall n.
182 permut_p f p (S n) \to (f (S n)) = (S n) \to permut_p f p n.
187 [elim (H i (le_S i n H2) H3).split
189 elim (le_to_or_lt_eq (f i) (S n))
190 [apply le_S_S_to_le.assumption
191 |absurd (f i = (S n))
195 [rewrite < H8.assumption
197 |unfold.intro.rewrite > H8 in H2.
198 apply (not_le_Sn_n n).rewrite < H9.assumption
206 elim (H i (le_S i n H2) H3).
208 [assumption|apply le_S.assumption|assumption]
212 lemma permut_p_transpose: \forall p.\forall i,j,n.
213 i \le n \to j \le n \to p i = p j \to
214 permut_p (transpose i j) p n.
215 unfold permut_p.intros.
219 apply (eqb_elim i1 i)
221 apply (eqb_elim i1 j)
222 [simplify.intro.assumption
223 |simplify.intro.assumption
226 apply (eqb_elim i1 j)
227 [simplify.intro.assumption
228 |simplify.intro.assumption
232 apply (eqb_elim i1 i)
234 apply (eqb_elim i1 j)
235 [simplify.intro.rewrite < H6.assumption
236 |simplify.intro.rewrite < H2.rewrite < H5.assumption
239 apply (eqb_elim i1 j)
240 [simplify.intro.rewrite > H2.rewrite < H6.assumption
241 |simplify.intro.assumption
247 apply (injective_transpose ? ? ? ? H8).
251 theorem eq_map_iter_p_k: \forall f,g.\forall p.\forall a,k,n:nat.
252 p (S n-k) = true \to (\forall i. (S n)-k < i \to i \le (S n) \to (p i) = false) \to
253 map_iter_p (S n) p g a f = map_iter_p (S n-k) p g a f.
256 [rewrite < minus_n_O.reflexivity
259 rewrite > map_iter_p_S_false
261 |apply H2[simplify.apply lt_O_S.|apply le_n]
264 rewrite > map_iter_p_S_false
272 |apply H2[autobatch|apply le_n]
278 theorem eq_map_iter_p_a: \forall p.\forall f.\forall g. \forall a,n:nat.
279 (\forall i.i \le n \to p i = false) \to map_iter_p n p g a f = a.
282 [simplify.reflexivity
283 |rewrite > map_iter_p_S_false
286 apply H1.apply le_S.assumption
292 theorem eq_map_iter_p_transpose: \forall p.\forall f.associative nat f \to
293 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. k < n \to
294 (p (S n) = true) \to (p (n-k)) = true \to (\forall i. n-k < i \to i \le n \to (p i) = false)
295 \to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose (n-k) (S n) m)) a f.
298 [intro.absurd (k < O)
299 [assumption|apply le_to_not_lt.apply le_O_n]
301 rewrite > (map_iter_p_S_true ? ? ? ? ? H3).
302 rewrite > (map_iter_p_S_true ? ? ? ? ? H3).
303 rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5).
304 rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5).
305 generalize in match H4.
308 rewrite > (map_iter_p_S_true ? ? ? ? ? H6).
309 rewrite > (map_iter_p_S_true ? ? ? ? ? H6).
310 rewrite > transpose_i_j_j.
311 rewrite > transpose_i_j_i.
312 cut (map_iter_p (m-k) p g a f =
313 map_iter_p (m-k) p (\lambda x.g (transpose (S(m-k)) (S(S m)) x)) a f)
316 rewrite < H1 in \vdash (? ? (? % ?) ?).
319 |apply eq_map_iter_p.
320 intros.unfold transpose.
321 cut (eqb m1 (S (m-k)) =false)
322 [cut (eqb m1 (S (S m)) =false)
326 |apply not_eq_to_eqb_false.
328 apply (le_to_lt_to_lt ? m)
329 [apply (trans_le ? (m-k))
330 [assumption|autobatch]
331 |apply le_S.apply le_n
334 |apply not_eq_to_eqb_false.
339 |apply le_S_S_to_le.assumption
344 theorem eq_map_iter_p_transpose1: \forall p.\forall f.associative nat f \to
345 symmetric2 nat nat f \to \forall g. \forall a,k1,k2,n:nat. O < k1 \to k1 < k2 \to k2 \le n \to
346 (p k1) = true \to (p k2) = true \to (\forall i. k1 < i \to i < k2 \to (p i) = false)
347 \to map_iter_p n p g a f = map_iter_p n p (\lambda m. g (transpose k1 k2 m)) a f.
351 [assumption|apply lt_to_not_le.apply (trans_lt ? k1 ? H2 H3)]
352 |apply (eqb_elim (S n1) k2)
356 cut (k1 = n1 - (n1 -k1))
358 apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1))
359 [cut (k1 \le n1)[autobatch|autobatch]
361 |rewrite < Hcut.assumption
362 |rewrite < Hcut.intros.
363 apply (H9 i H10).unfold.autobatch
371 [apply (bool_elim ? (p (S n1)))
373 rewrite > map_iter_p_S_true
374 [rewrite > map_iter_p_S_true
375 [cut ((transpose k1 k2 (S n1)) = (S n1))
379 [elim (le_to_or_lt_eq ? ? H6)
381 |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
388 rewrite > (not_eq_to_eqb_false ? ? Hcut).
389 rewrite > (not_eq_to_eqb_false ? ? H4).
397 rewrite > map_iter_p_S_false
398 [rewrite > map_iter_p_S_false
400 [elim (le_to_or_lt_eq ? ? H6)
402 |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
425 lemma decidable_n:\forall p.\forall n.
426 (\forall m. m \le n \to (p m) = false) \lor
427 (\exists m. m \le n \land (p m) = true \land
428 \forall i. m < i \to i \le n \to (p i) = false).
431 [apply (bool_elim ? (p O))
433 apply (ex_intro ? ? O).
435 [split[apply le_n|assumption]
436 |intros.absurd (O<i)[assumption|apply le_to_not_lt.assumption]
439 intros.apply (le_n_O_elim m H1).assumption
441 |apply (bool_elim ? (p (S n1)))
443 apply (ex_intro ? ? (S n1)).
445 [split[apply le_n|assumption]
446 |intros.absurd (S n1<i)[assumption|apply le_to_not_lt.assumption]
451 elim (le_to_or_lt_eq m (S n1) H3)
452 [apply H1.apply le_S_S_to_le.assumption
453 |rewrite > H4.assumption
456 elim H1.elim H3.elim H4.
457 apply (ex_intro ? ? a).
459 [split[apply le_S.assumption|assumption]
460 |intros.elim (le_to_or_lt_eq i (S n1) H9)
461 [apply H5[assumption|apply le_S_S_to_le.assumption]
462 |rewrite > H10.assumption
470 lemma decidable_n1:\forall p.\forall n,j. j \le n \to (p j)=true \to
471 (\forall m. j < m \to m \le n \to (p m) = false) \lor
472 (\exists m. j < m \land m \le n \land (p m) = true \land
473 \forall i. m < i \to i \le n \to (p i) = false).
475 elim (decidable_n p n)
479 apply not_eq_true_false.
484 apply (nat_compare_elim j a)
487 apply (ex_intro ? ? a).
493 [assumption|assumption]
506 apply not_eq_true_false.
509 apply (H6 j H2).assumption
515 lemma decidable_n2:\forall p.\forall n,j. j \le n \to (p j)=true \to
516 (\forall m. j < m \to m \le n \to (p m) = false) \lor
517 (\exists m. j < m \land m \le n \land (p m) = true \land
518 \forall i. j < i \to i < m \to (p i) = false).
522 apply (le_n_O_elim j H).intros.
524 [assumption|apply lt_to_not_le.assumption]
525 |elim (le_to_or_lt_eq ? ? H1)
528 [apply (bool_elim ? (p (S n1)))
531 apply (ex_intro ? ? (S n1)).
535 [assumption|apply le_n]
546 elim (le_to_or_lt_eq ? ? H7)
548 [assumption|apply le_S_S_to_le.assumption]
549 |rewrite > H8.assumption
557 apply (ex_intro ? ? a).
560 [split[assumption|apply le_S.assumption]
581 (* tutti d spostare *)
582 theorem lt_minus_to_lt_plus:
583 \forall n,m,p. n - m < p \to n < m + p.
585 apply (nat_elim2 ? ? ? ? n m)
586 [simplify.intros.autobatch.
587 |intros 2.rewrite < minus_n_O.
599 theorem lt_plus_to_lt_minus:
600 \forall n,m,p. m \le n \to n < m + p \to n - m < p.
602 apply (nat_elim2 ? ? ? ? n m)
604 apply (le_n_O_elim ? H).
605 simplify.intros.assumption
606 |simplify.intros.assumption.
610 [apply le_S_S_to_le.assumption
611 |apply le_S_S_to_le.apply H2
616 theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
623 theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
624 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
625 (p (S n) = true) \to (p k) = true
626 \to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose k (S n) m)) a f.
628 cut (k = (S n)-(S n -k))
629 [generalize in match H3.clear H3.
630 generalize in match g.
631 generalize in match H2.clear H2.
633 (*generalize in match Hcut.clear Hcut.*)
634 (* generalize in match H3.clear H3.*)
635 (* something wrong here
636 rewrite > Hcut in \vdash (?\rarr ?\rarr %). *)
637 apply (nat_elim1 (S n - k)).
639 elim (decidable_n2 p n (S n -m) H4 H6)
640 [apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
647 [assumption|apply le_S_S_to_le.assumption]
654 (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f))
656 (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f))
657 [cut (a1 = (S n -(S n -a1)))
660 [apply lt_plus_to_lt_minus
661 [apply le_S.assumption
663 apply lt_minus_to_lt_plus.
667 apply (trans_lt ? (S n -m))[assumption|assumption]
668 |rewrite < Hcut1.assumption
670 |rewrite < Hcut1.assumption
672 |apply minus_m_minus_mn.
673 apply le_S.assumption
675 |apply (eq_map_iter_p_transpose1 p f H H1)
678 |apply le_S.assumption
685 (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 (transpose (S n -(S n -a1)) (S n) i)))) a f))
686 [cut (a1 = (S n) -(S n -a1))
688 [apply lt_plus_to_lt_minus
689 [apply le_S.assumption
691 apply lt_minus_to_lt_plus.
695 apply (trans_lt ? (S n -m))[assumption|assumption]
696 |rewrite < Hcut1.assumption
698 |rewrite < Hcut1.assumption
700 |apply minus_m_minus_mn.
701 apply le_S.assumption
703 |apply eq_map_iter_p.
704 cut (a1 = (S n) -(S n -a1))
708 rewrite < transpose_i_j_j_i.
709 rewrite > (transpose_i_j_j_i (S n -m)).
710 rewrite > (transpose_i_j_j_i a1 (S n)).
711 rewrite > (transpose_i_j_j_i (S n -m)).
715 apply (not_le_Sn_n n).
716 rewrite < H12.assumption
718 apply (not_le_Sn_n n).
719 rewrite > H12.assumption
721 apply (not_le_Sn_n a1).
722 rewrite < H12 in \vdash (? (? %) ?).assumption
724 |apply minus_m_minus_mn.
725 apply le_S.assumption
730 |apply minus_m_minus_mn.
731 apply le_S.assumption
735 theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to
736 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to
737 (p (S n) = true) \to (p k) = true
738 \to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose k (S n) m)) a f.
740 elim (le_to_or_lt_eq ? ? H3)
741 [apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2)
742 [apply le_S_S_to_le.assumption|assumption|assumption]
746 apply eq_f.apply sym_eq. apply transpose_i_i.
750 lemma permut_p_O: \forall p.\forall h.\forall n.
751 permut_p h p n \to p O = false \to \forall m. (S m) \le n \to p (S m) = true \to O < h(S m).
752 intros.unfold permut_p in H.
753 apply not_le_to_lt.unfold.intro.
754 elim (H (S m) H2 H3).
756 absurd (p (h (S m)) = true)
758 |apply (le_n_O_elim ? H4).
760 apply not_eq_true_false.
761 rewrite < H9.rewrite < H1.reflexivity
765 theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to
766 symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat.
767 permut_p h p n \to p O = false \to
768 map_iter_p n p g a f = map_iter_p n p (compose ? ? ? g h) a f .
771 [simplify.reflexivity
772 |apply (bool_elim ? (p (S n1)))
774 apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f))
775 [unfold permut_p in H3.
776 elim (H3 (S n1) (le_n ?) H5).
778 apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1)
779 [apply (permut_p_O ? ? ? H3 H4)
780 [apply le_n|assumption]
785 |apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.
786 (g(transpose (h (S n1)) (S n1)
787 (transpose (h (S n1)) (S n1) (h m)))) ) a f))
788 [rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
789 rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
791 [rewrite > transpose_i_j_j.
792 rewrite > transpose_i_j_i.
793 rewrite > transpose_i_j_j.
795 |apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?)
800 unfold permut_p in H3.
801 elim (H3 i (le_S ? ? H6) H7).
803 elim (le_to_or_lt_eq ? ? H10)
805 rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)).
806 cut (h i \neq h (S n1))
807 [rewrite > (not_eq_to_eqb_false ? ? Hcut).
815 unfold.apply le_S_S.assumption
819 apply (eqb_elim (S n1) (h (S n1)))
821 absurd (h i = h (S n1))
828 unfold.apply le_S_S.assumption
833 rewrite > (not_eq_to_eqb_false ? ? H12).
834 rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))).
836 elim (H3 (S n1) (le_n ? ) H5).
838 elim (le_to_or_lt_eq ? ? H15)
839 [apply le_S_S_to_le.assumption
842 apply sym_eq.assumption
847 unfold permut_p in H3.
849 apply (eqb_elim (h i) (S n1))
851 apply (eqb_elim (h i) (h (S n1)))
852 [intro.simplify.assumption
854 elim (H3 (S n1) (le_n ? ) H5).
858 apply (eqb_elim (h i) (h (S n1)))
859 [intro.simplify.assumption
861 elim (H3 i (le_S ? ? H6) H7).
866 |simplify.intros.unfold Not.intro.
867 unfold permut_p in H3.
868 elim (H3 i (le_S i ? H6) H7).
869 apply (H13 j H8 (le_S j ? H9) H10).
870 apply (injective_transpose ? ? ? ? H11)
875 |apply eq_map_iter_p.
877 rewrite > transpose_transpose.reflexivity
881 rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
882 rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
885 unfold permut_p in H3.
887 elim (H3 i (le_S i ? H6) H7).
891 [elim (le_to_or_lt_eq ? ? H10)
892 [apply le_S_S_to_le.assumption
893 |absurd (p (h i) = true)
897 unfold.intro.apply not_eq_true_false.
898 apply sym_eq.assumption
905 [assumption|apply (le_S ? ? H13)|assumption]