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/iteration.ma".
17 include "nat/permutation.ma".
18 include "nat/count.ma".
20 lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
22 [intros.apply le_n_O_to_eq.assumption
23 |intros.apply sym_eq.apply le_n_O_to_eq.assumption
24 |intros.apply eq_f.apply H
25 [apply le_S_S_to_le.assumption
26 |apply le_S_S_to_le.assumption
31 let rec map_iter_P n p (g:nat \to nat) (a:nat) f \def
36 [true \Rightarrow f (g (S k)) (map_iter_P k p g a f)
37 |false \Rightarrow map_iter_P k p g a f]
40 theorem eq_map_iter_P: \forall g1,g2:nat \to nat.
41 \forall p:nat \to bool.
42 \forall f:nat \to nat \to nat. \forall a,n:nat.
43 (\forall m:nat. m \le n \to g1 m = g2 m) \to
44 map_iter_P n p g1 a f = map_iter_P n p g2 a f.
46 [simplify.reflexivity.
47 |simplify.elim (p (S n1))
50 |simplify.apply H.intros.apply H1.
53 |simplify.apply H.intros.apply H1.
59 (* useful since simply simpifies too much *)
61 theorem map_iter_P_O: \forall p.\forall g.\forall f. \forall a:nat.
62 map_iter_P O p g a f = a.
63 intros.simplify.reflexivity.
66 theorem map_iter_P_S_true: \forall p.\forall g.\forall f. \forall a,n:nat.
68 map_iter_P (S n) p g a f = f (g (S n)) (map_iter_P n p g a f).
69 intros.simplify.rewrite > H.reflexivity.
72 theorem map_iter_P_S_false: \forall p.\forall g.\forall f. \forall a,n:nat.
74 map_iter_P (S n) p g a f = map_iter_P n p g a f.
75 intros.simplify.rewrite > H.reflexivity.
78 (* map_iter examples *)
79 definition Pi_P \def \lambda p. \lambda n.
80 map_iter_P n p (\lambda n.n) (S O) times.
82 lemma Pi_P_S: \forall n.\forall p.
85 [true \Rightarrow (S n)*(Pi_P p n)
86 |false \Rightarrow (Pi_P p n)
91 lemma lt_O_Pi_P: \forall n.\forall p.
97 [change with (O < (S n1)*(Pi_P p n1)).
98 rewrite >(times_n_O n1).
99 apply lt_times[apply le_n|assumption]
105 let rec card n p \def
109 (bool_to_nat (p (S m))) + (card m p)].
111 lemma a_times_Pi_P: \forall p. \forall a,n.
112 exp a (card n p) * Pi_P p n = map_iter_P n p (\lambda n.a*n) (S O) times.
114 [simplify.reflexivity
115 |simplify.apply (bool_elim ? (p (S n1)))
118 (a*exp a (card n1 p) * ((S n1) * (Pi_P p n1)) =
119 a*(S n1)*map_iter_P n1 p (\lambda n.a*n) (S O) times).
127 definition permut_p \def \lambda f. \lambda p:nat\to bool. \lambda n.
128 \forall i. i \le n \to p i = true \to ((f i \le n \land p (f i) = true)
129 \land (\forall j. p j = true \to j \le n \to i \neq j \to (f i \neq f j))).
131 definition extentional_eq_n \def \lambda f,g:nat \to nat.\lambda n.
132 \forall x. x \le n \to f x = g x.
134 lemma extentional_eq_n_to_permut_p: \forall f,g. \forall p. \forall n.
135 extentional_eq_n f g n\to permut_p f p n \to permut_p g p n.
136 intros.unfold permut_p.
141 [rewrite < (H i H2).assumption
142 |rewrite < (H i H2).assumption
145 unfold.intro.apply (H5 j H6 H7 H8).
147 rewrite > (H j H7).assumption
151 theorem permut_p_compose: \forall f,g.\forall p.\forall n.
152 permut_p f p n \to permut_p g p n \to permut_p (compose ? ? ? g f) p n.
153 intros.unfold permut_p.intros.
156 elim (H1 (f i) H6 H7).
160 [unfold compose.assumption
161 |unfold compose.rewrite < H11.reflexivity
166 [elim (H j H13 H12).elim H15.rewrite < H18.reflexivity
167 |elim (H j H13 H12).elim H15.assumption.
168 |apply (H5 j H12 H13 H14)
173 theorem permut_p_S_to_permut_p: \forall f.\forall p.\forall n.
174 permut_p f p (S n) \to (f (S n)) = (S n) \to permut_p f p n.
179 [elim (H i (le_S i n H2) H3).split
181 elim (le_to_or_lt_eq (f i) (S n))
182 [apply le_S_S_to_le.assumption
183 |absurd (f i = (S n))
187 [rewrite < H8.assumption
189 |unfold.intro.rewrite > H8 in H2.
190 apply (not_le_Sn_n n).rewrite < H9.assumption
198 elim (H i (le_S i n H2) H3).
200 [assumption|apply le_S.assumption|assumption]
204 lemma permut_p_transpose: \forall p.\forall i,j,n.
205 i \le n \to j \le n \to p i = p j \to
206 permut_p (transpose i j) p n.
207 unfold permut_p.intros.
211 apply (eqb_elim i1 i)
213 apply (eqb_elim i1 j)
214 [simplify.intro.assumption
215 |simplify.intro.assumption
218 apply (eqb_elim i1 j)
219 [simplify.intro.assumption
220 |simplify.intro.assumption
224 apply (eqb_elim i1 i)
226 apply (eqb_elim i1 j)
227 [simplify.intro.rewrite < H6.assumption
228 |simplify.intro.rewrite < H2.rewrite < H5.assumption
231 apply (eqb_elim i1 j)
232 [simplify.intro.rewrite > H2.rewrite < H6.assumption
233 |simplify.intro.assumption
239 apply (injective_transpose ? ? ? ? H8).
243 theorem eq_map_iter_P_k: \forall f,g.\forall p.\forall a,k,n:nat.
244 p (S n-k) = true \to (\forall i. (S n)-k < i \to i \le (S n) \to (p i) = false) \to
245 map_iter_P (S n) p g a f = map_iter_P (S n-k) p g a f.
248 [rewrite < minus_n_O.reflexivity
251 rewrite > map_iter_P_S_false
253 |apply H2[simplify.apply lt_O_S.|apply le_n]
256 rewrite > map_iter_P_S_false
264 |apply H2[auto|apply le_n]
270 theorem eq_map_iter_p_a: \forall p.\forall f.\forall g. \forall a,n:nat.
271 (\forall i.i \le n \to p i = false) \to map_iter_P n p g a f = a.
274 [simplify.reflexivity
275 |rewrite > map_iter_P_S_false
278 apply H1.apply le_S.assumption
284 theorem eq_map_iter_p_transpose: \forall p.\forall f.associative nat f \to
285 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. k < n \to
286 (p (S n) = true) \to (p (n-k)) = true \to (\forall i. n-k < i \to i \le n \to (p i) = false)
287 \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.
290 [intro.absurd (k < O)
291 [assumption|apply le_to_not_lt.apply le_O_n]
293 rewrite > (map_iter_P_S_true ? ? ? ? ? H3).
294 rewrite > (map_iter_P_S_true ? ? ? ? ? H3).
295 rewrite > (eq_map_iter_P_k ? ? ? ? ? ? H4 H5).
296 rewrite > (eq_map_iter_P_k ? ? ? ? ? ? H4 H5).
297 generalize in match H4.
300 rewrite > (map_iter_P_S_true ? ? ? ? ? H6).
301 rewrite > (map_iter_P_S_true ? ? ? ? ? H6).
302 rewrite > transpose_i_j_j.
303 rewrite > transpose_i_j_i.
304 cut (map_iter_P (m-k) p g a f =
305 map_iter_P (m-k) p (\lambda x.g (transpose (S(m-k)) (S(S m)) x)) a f)
308 rewrite < H1 in \vdash (? ? (? % ?) ?).
311 |apply eq_map_iter_P.
312 intros.unfold transpose.
313 cut (eqb m1 (S (m-k)) =false)
314 [cut (eqb m1 (S (S m)) =false)
318 |apply not_eq_to_eqb_false.
320 apply (le_to_lt_to_lt ? m)
321 [apply (trans_le ? (m-k))
323 |apply le_S.apply le_n
326 |apply not_eq_to_eqb_false.
331 |apply le_S_S_to_le.assumption
336 theorem eq_map_iter_p_transpose1: \forall p.\forall f.associative nat f \to
337 symmetric2 nat nat f \to \forall g. \forall a,k1,k2,n:nat. O < k1 \to k1 < k2 \to k2 \le n \to
338 (p k1) = true \to (p k2) = true \to (\forall i. k1 < i \to i < k2 \to (p i) = false)
339 \to map_iter_P n p g a f = map_iter_P n p (\lambda m. g (transpose k1 k2 m)) a f.
343 [assumption|apply lt_to_not_le.apply (trans_lt ? k1 ? H2 H3)]
344 |apply (eqb_elim (S n1) k2)
348 cut (k1 = n1 - (n1 -k1))
350 apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1))
351 [cut (k1 \le n1)[auto|auto]
353 |rewrite < Hcut.assumption
354 |rewrite < Hcut.intros.
355 apply (H9 i H10).unfold.auto
363 [apply (bool_elim ? (p (S n1)))
365 rewrite > map_iter_P_S_true
366 [rewrite > map_iter_P_S_true
367 [cut ((transpose k1 k2 (S n1)) = (S n1))
371 [elim (le_to_or_lt_eq ? ? H6)
373 |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
380 rewrite > (not_eq_to_eqb_false ? ? Hcut).
381 rewrite > (not_eq_to_eqb_false ? ? H4).
389 rewrite > map_iter_P_S_false
390 [rewrite > map_iter_P_S_false
392 [elim (le_to_or_lt_eq ? ? H6)
394 |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
417 lemma decidable_n:\forall p.\forall n.
418 (\forall m. m \le n \to (p m) = false) \lor
419 (\exists m. m \le n \land (p m) = true \land
420 \forall i. m < i \to i \le n \to (p i) = false).
423 [apply (bool_elim ? (p O))
425 apply (ex_intro ? ? O).
427 [split[apply le_n|assumption]
428 |intros.absurd (O<i)[assumption|apply le_to_not_lt.assumption]
431 intros.apply (le_n_O_elim m H1).assumption
433 |apply (bool_elim ? (p (S n1)))
435 apply (ex_intro ? ? (S n1)).
437 [split[apply le_n|assumption]
438 |intros.absurd (S n1<i)[assumption|apply le_to_not_lt.assumption]
443 elim (le_to_or_lt_eq m (S n1) H3)
444 [apply H1.apply le_S_S_to_le.assumption
445 |rewrite > H4.assumption
448 elim H1.elim H3.elim H4.
449 apply (ex_intro ? ? a).
451 [split[apply le_S.assumption|assumption]
452 |intros.elim (le_to_or_lt_eq i (S n1) H9)
453 [apply H5[assumption|apply le_S_S_to_le.assumption]
454 |rewrite > H10.assumption
462 lemma decidable_n1:\forall p.\forall n,j. j \le n \to (p j)=true \to
463 (\forall m. j < m \to m \le n \to (p m) = false) \lor
464 (\exists m. j < m \land m \le n \land (p m) = true \land
465 \forall i. m < i \to i \le n \to (p i) = false).
467 elim (decidable_n p n)
471 apply not_eq_true_false.
476 apply (nat_compare_elim j a)
479 apply (ex_intro ? ? a).
485 [assumption|assumption]
498 apply not_eq_true_false.
501 apply (H6 j H2).assumption
507 lemma decidable_n2:\forall p.\forall n,j. j \le n \to (p j)=true \to
508 (\forall m. j < m \to m \le n \to (p m) = false) \lor
509 (\exists m. j < m \land m \le n \land (p m) = true \land
510 \forall i. j < i \to i < m \to (p i) = false).
514 apply (le_n_O_elim j H).intros.
516 [assumption|apply lt_to_not_le.assumption]
517 |elim (le_to_or_lt_eq ? ? H1)
520 [apply (bool_elim ? (p (S n1)))
523 apply (ex_intro ? ? (S n1)).
527 [assumption|apply le_n]
538 elim (le_to_or_lt_eq ? ? H7)
540 [assumption|apply le_S_S_to_le.assumption]
541 |rewrite > H8.assumption
549 apply (ex_intro ? ? a).
552 [split[assumption|apply le_S.assumption]
573 (* tutti d spostare *)
574 theorem lt_minus_to_lt_plus:
575 \forall n,m,p. n - m < p \to n < m + p.
577 apply (nat_elim2 ? ? ? ? n m)
578 [simplify.intros.auto.
579 |intros 2.rewrite < minus_n_O.
591 theorem lt_plus_to_lt_minus:
592 \forall n,m,p. m \le n \to n < m + p \to n - m < p.
594 apply (nat_elim2 ? ? ? ? n m)
596 apply (le_n_O_elim ? H).
597 simplify.intros.assumption
598 |simplify.intros.assumption.
602 [apply le_S_S_to_le.assumption
603 |apply le_S_S_to_le.apply H2
608 theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
615 theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
616 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
617 (p (S n) = true) \to (p k) = true
618 \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.
620 cut (k = (S n)-(S n -k))
621 [generalize in match H3.clear H3.
622 generalize in match g.
623 generalize in match H2.clear H2.
625 (*generalize in match Hcut.clear Hcut.*)
626 (* generalize in match H3.clear H3.*)
627 (* something wrong here
628 rewrite > Hcut in \vdash (?\rarr ?\rarr %). *)
629 apply (nat_elim1 (S n - k)).
631 elim (decidable_n2 p n (S n -m) H4 H6)
632 [apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
639 [assumption|apply le_S_S_to_le.assumption]
646 (map_iter_P (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f))
648 (map_iter_P (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f))
649 [cut (a1 = (S n -(S n -a1)))
652 [apply lt_plus_to_lt_minus
653 [apply le_S.assumption
655 apply lt_minus_to_lt_plus.
659 apply (trans_lt ? (S n -m))[assumption|assumption]
660 |rewrite < Hcut1.assumption
662 |rewrite < Hcut1.assumption
664 |apply minus_m_minus_mn.
665 apply le_S.assumption
667 |apply (eq_map_iter_p_transpose1 p f H H1)
670 |apply le_S.assumption
677 (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))
678 [cut (a1 = (S n) -(S n -a1))
680 [apply lt_plus_to_lt_minus
681 [apply le_S.assumption
683 apply lt_minus_to_lt_plus.
687 apply (trans_lt ? (S n -m))[assumption|assumption]
688 |rewrite < Hcut1.assumption
690 |rewrite < Hcut1.assumption
692 |apply minus_m_minus_mn.
693 apply le_S.assumption
695 |apply eq_map_iter_P.
696 cut (a1 = (S n) -(S n -a1))
700 rewrite < transpose_i_j_j_i.
701 rewrite > (transpose_i_j_j_i (S n -m)).
702 rewrite > (transpose_i_j_j_i a1 (S n)).
703 rewrite > (transpose_i_j_j_i (S n -m)).
707 apply (not_le_Sn_n n).
708 rewrite < H12.assumption
710 apply (not_le_Sn_n n).
711 rewrite > H12.assumption
713 apply (not_le_Sn_n a1).
714 rewrite < H12 in \vdash (? (? %) ?).assumption
716 |apply minus_m_minus_mn.
717 apply le_S.assumption
722 |apply minus_m_minus_mn.
723 apply le_S.assumption
727 theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to
728 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to
729 (p (S n) = true) \to (p k) = true
730 \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.
732 elim (le_to_or_lt_eq ? ? H3)
733 [apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2)
734 [apply le_S_S_to_le.assumption|assumption|assumption]
738 apply eq_f.apply sym_eq. apply transpose_i_i.
742 lemma permut_p_O: \forall p.\forall h.\forall n.
743 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).
744 intros.unfold permut_p in H.
745 apply not_le_to_lt.unfold.intro.
746 elim (H (S m) H2 H3).
748 absurd (p (h (S m)) = true)
750 |apply (le_n_O_elim ? H4).
752 apply not_eq_true_false.
753 rewrite < H9.rewrite < H1.reflexivity
757 theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to
758 symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat.
759 permut_p h p n \to p O = false \to
760 map_iter_P n p g a f = map_iter_P n p (compose ? ? ? g h) a f .
763 [simplify.reflexivity
764 |apply (bool_elim ? (p (S n1)))
766 apply (trans_eq ? ? (map_iter_P (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f))
767 [unfold permut_p in H3.
768 elim (H3 (S n1) (le_n ?) H5).
770 apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1)
771 [apply (permut_p_O ? ? ? H3 H4)
772 [apply le_n|assumption]
777 |apply (trans_eq ? ? (map_iter_P (S n1) p (\lambda m.
778 (g(transpose (h (S n1)) (S n1)
779 (transpose (h (S n1)) (S n1) (h m)))) ) a f))
780 [rewrite > (map_iter_P_S_true ? ? ? ? ? H5).
781 rewrite > (map_iter_P_S_true ? ? ? ? ? H5).
783 [rewrite > transpose_i_j_j.
784 rewrite > transpose_i_j_i.
785 rewrite > transpose_i_j_j.
787 |apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?)
792 unfold permut_p in H3.
793 elim (H3 i (le_S ? ? H6) H7).
795 elim (le_to_or_lt_eq ? ? H10)
797 rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)).
798 cut (h i \neq h (S n1))
799 [rewrite > (not_eq_to_eqb_false ? ? Hcut).
807 unfold.apply le_S_S.assumption
811 apply (eqb_elim (S n1) (h (S n1)))
813 absurd (h i = h (S n1))
820 unfold.apply le_S_S.assumption
825 rewrite > (not_eq_to_eqb_false ? ? H12).
826 rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))).
828 elim (H3 (S n1) (le_n ? ) H5).
830 elim (le_to_or_lt_eq ? ? H15)
831 [apply le_S_S_to_le.assumption
834 apply sym_eq.assumption
839 unfold permut_p in H3.
841 apply (eqb_elim (h i) (S n1))
843 apply (eqb_elim (h i) (h (S n1)))
844 [intro.simplify.assumption
846 elim (H3 (S n1) (le_n ? ) H5).
850 apply (eqb_elim (h i) (h (S n1)))
851 [intro.simplify.assumption
853 elim (H3 i (le_S ? ? H6) H7).
858 |simplify.intros.unfold Not.intro.
859 unfold permut_p in H3.
860 elim (H3 i (le_S i ? H6) H7).
861 apply (H13 j H8 (le_S j ? H9) H10).
862 apply (injective_transpose ? ? ? ? H11)
867 |apply eq_map_iter_P.
869 rewrite > transpose_transpose.reflexivity
873 rewrite > (map_iter_P_S_false ? ? ? ? ? H5).
874 rewrite > (map_iter_P_S_false ? ? ? ? ? H5).
877 unfold permut_p in H3.
879 elim (H3 i (le_S i ? H6) H7).
883 [elim (le_to_or_lt_eq ? ? H10)
884 [apply le_S_S_to_le.assumption
885 |absurd (p (h i) = true)
889 unfold.intro.apply not_eq_true_false.
890 apply sym_eq.assumption
897 [assumption|apply (le_S ? ? H13)|assumption]