From: Andrea Asperti Date: Mon, 18 Dec 2006 11:52:57 +0000 (+0000) Subject: Renamed iterative into map_iter_p and moved around a few theorems. X-Git-Tag: 0.4.95@7852~724 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=96d58f0c965040b5fecbb8c36ceb52277b1c78db;p=helm.git Renamed iterative into map_iter_p and moved around a few theorems. --- diff --git a/matita/library/nat/euler_theorem.ma b/matita/library/nat/euler_theorem.ma index 0655fb968..d58f7c2b0 100644 --- a/matita/library/nat/euler_theorem.ma +++ b/matita/library/nat/euler_theorem.ma @@ -14,58 +14,10 @@ set "baseuri" "cic:/matita/nat/euler_theorem". -include "nat/iteration.ma". +include "nat/map_iter_p.ma". include "nat/totient.ma". -(* da spostare *) -lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m. -apply nat_elim2 - [intros.apply le_n_O_to_eq.assumption - |intros.apply sym_eq.apply le_n_O_to_eq.assumption - |intros.apply eq_f.apply H - [apply le_S_S_to_le.assumption - |apply le_S_S_to_le.assumption - ] - ] -qed. - -lemma gcd_n_n: \forall n.gcd n n = n. -intro.elim n - [reflexivity - |apply le_to_le_to_eq - [apply divides_to_le - [apply lt_O_S - |apply divides_gcd_n - ] - |apply divides_to_le - [apply lt_O_gcd.apply lt_O_S - |apply divides_d_gcd - [apply divides_n_n|apply divides_n_n] - ] - ] - ] -qed. - - -lemma count_card: \forall p.\forall n. -p O = false \to count (S n) p = card n p. -intros.elim n - [simplify.rewrite > H. reflexivity - |simplify. - rewrite < plus_n_O. - apply eq_f.assumption - ] -qed. - -lemma count_card1: \forall p.\forall n. -p O = false \to p n = false \to count n p = card n p. -intros 3.apply (nat_case n) - [intro.simplify.rewrite > H. reflexivity - |intros.rewrite > (count_card ? ? H). - simplify.rewrite > H1.reflexivity - ] -qed. - +(* a reformulation of totient using card insted of count *) lemma totient_card: \forall n. totient n = card n (\lambda i.eqb (gcd i n) (S O)). intro.apply (nat_case n) @@ -80,106 +32,50 @@ intro.apply (nat_case n) ] qed. -(* da spostare *) -lemma gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n. -intro.apply (nat_case n) - [intros.reflexivity - |intros. - apply le_to_le_to_eq - [apply divides_to_le - [apply lt_O_S|apply divides_gcd_n] - |apply divides_to_le - [apply lt_O_gcd.rewrite > (times_n_O O). - apply lt_times[apply lt_O_S|assumption] - |apply divides_d_gcd - [apply (witness ? ? m1).reflexivity - |apply divides_n_n - ] - ] - ] - ] -qed. - -(* da spostare *) -lemma eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to -(gcd n m) = (S O) \to \lnot (divides n m). -intros.unfold.intro. -elim H2. -generalize in match H1. -rewrite > H3. -intro. -cut (O < n2) - [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4) - [cut (gcd n (n*n2) = n) - [apply (lt_to_not_eq (S O) n) - [assumption|rewrite < H4.assumption] - |apply gcd_n_times_nm.assumption - ] - |apply (trans_lt ? (S O))[apply le_n|assumption] - |assumption - ] - |elim (le_to_or_lt_eq O n2 (le_O_n n2)) - [assumption - |apply False_ind. - apply (le_to_not_lt n (S O)) - [rewrite < H4. - apply divides_to_le - [rewrite > H4.apply lt_O_S - |apply divides_d_gcd - [apply (witness ? ? n2).reflexivity - |apply divides_n_n - ] - ] - |assumption - ] - ] - ] -qed. - -theorem gcd_Pi_P: \forall n,k. O < k \to k \le n \to -gcd n (Pi_P (\lambda i.eqb (gcd i n) (S O)) k) = (S O). +theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to +gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O). intros 3.elim H - [rewrite > Pi_P_S. + [rewrite > pi_p_S. cut (eqb (gcd (S O) n) (S O) = true) [rewrite > Hcut. change with ((gcd n (S O)) = (S O)).auto |apply eq_to_eqb_true.auto ] - |rewrite > Pi_P_S. + |rewrite > pi_p_S. apply eqb_elim [intro. change with - ((gcd n ((S n1)*(Pi_P (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)). + ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)). apply eq_gcd_times_SO [unfold.apply le_S.assumption - |apply lt_O_Pi_P. + |apply lt_O_pi_p. |rewrite > sym_gcd. assumption. |apply H2. apply (trans_le ? (S n1))[apply le_n_Sn|assumption] ] |intro. change with - (gcd n (Pi_P (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)). + (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)). apply H2. apply (trans_le ? (S n1))[apply le_n_Sn|assumption] ] ] qed. -theorem congruent_map_iter_P_times:\forall f:nat \to nat. \forall a,n:nat. +theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat. O < a \to congruent -(map_iter_P n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times) -(map_iter_P n (\lambda i.eqb (gcd i a) (S O)) +(map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times) +(map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x \mod a) (S O) times) a. intros. elim n - [rewrite > map_iter_P_O. + [rewrite > map_iter_p_O. apply (congruent_n_n ? a) |apply (eqb_elim (gcd (S n1) a) (S O)) [intro. - rewrite > map_iter_P_S_true - [rewrite > map_iter_P_S_true + rewrite > map_iter_p_S_true + [rewrite > map_iter_p_S_true [apply congruent_times [assumption |apply congruent_n_mod_n.assumption @@ -190,8 +86,8 @@ elim n |apply eq_to_eqb_true.assumption ] |intro. - rewrite > map_iter_P_S_false - [rewrite > map_iter_P_S_false + rewrite > map_iter_p_S_false + [rewrite > map_iter_p_S_false [assumption |apply not_eq_to_eqb_false.assumption ] @@ -201,44 +97,6 @@ elim n ] qed. -theorem lt_S_to_lt: \forall n,m. S n < m \to n < m. -intros. -apply (trans_lt ? (S n)) - [apply le_n|assumption] -qed. - -theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to -O < i. -intros. -elim (le_to_or_lt_eq ? ? (le_O_n i)) - [assumption - |absurd ((gcd i n) = (S O)) - [assumption - |rewrite < H2. - simplify. - unfold.intro. - apply (lt_to_not_eq (S O) n H). - apply sym_eq.assumption - ] - ] -qed. - -theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to -i < n. -intros. -elim (le_to_or_lt_eq ? ? H1) - [assumption - |absurd ((gcd i n) = (S O)) - [assumption - |rewrite > H3. - rewrite > gcd_n_n. - unfold.intro. - apply (lt_to_not_eq (S O) n H). - apply sym_eq.assumption - ] - ] -qed. - theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n. intros. @@ -335,9 +193,9 @@ cut (O < a) [apply divides_to_congruent [apply (trans_lt ? (S O)).apply lt_O_S. assumption |change with (O < exp a (totient n)).apply lt_O_exp.assumption - |apply (gcd_SO_to_divides_times_to_divides (Pi_P (\lambda i.eqb (gcd i n) (S O)) n)) + |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n)) [apply (trans_lt ? (S O)).apply lt_O_S. assumption - |apply gcd_Pi_P + |apply gcd_pi_p [apply (trans_lt ? (S O)).apply lt_O_S. assumption |apply le_n ] @@ -346,17 +204,17 @@ cut (O < a) rewrite > (sym_times (S O)). rewrite < times_n_SO. rewrite > totient_card. - rewrite > a_times_Pi_P. + rewrite > a_times_pi_p. apply congruent_to_divides [apply (trans_lt ? (S O)).apply lt_O_S. assumption | apply (transitive_congruent n ? - (map_iter_P n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times)) - [apply (congruent_map_iter_P_times ? n n). + (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times)) + [apply (congruent_map_iter_p_times ? n n). apply (trans_lt ? (S O)) [apply lt_O_S|assumption] - |unfold Pi_P. - cut ( (map_iter_P n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times) - = (map_iter_P n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times)) + |unfold pi_p. + cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times) + = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times)) [rewrite < Hcut1.apply congruent_n_n |apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m)) [apply assoc_times diff --git a/matita/library/nat/gcd.ma b/matita/library/nat/gcd.ma index cb29da2f8..6da8e13d0 100644 --- a/matita/library/nat/gcd.ma +++ b/matita/library/nat/gcd.ma @@ -384,6 +384,74 @@ rewrite < H4 in \vdash (? ? %).assumption. intros.unfold lt.apply le_S_S.apply le_O_n. qed. +theorem gcd_n_n: \forall n.gcd n n = n. +intro.elim n + [reflexivity + |apply le_to_le_to_eq + [apply divides_to_le + [apply lt_O_S + |apply divides_gcd_n + ] + |apply divides_to_le + [apply lt_O_gcd.apply lt_O_S + |apply divides_d_gcd + [apply divides_n_n|apply divides_n_n] + ] + ] + ] +qed. + +theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to +O < i. +intros. +elim (le_to_or_lt_eq ? ? (le_O_n i)) + [assumption + |absurd ((gcd i n) = (S O)) + [assumption + |rewrite < H2. + simplify. + unfold.intro. + apply (lt_to_not_eq (S O) n H). + apply sym_eq.assumption + ] + ] +qed. + +theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to +i < n. +intros. +elim (le_to_or_lt_eq ? ? H1) + [assumption + |absurd ((gcd i n) = (S O)) + [assumption + |rewrite > H3. + rewrite > gcd_n_n. + unfold.intro. + apply (lt_to_not_eq (S O) n H). + apply sym_eq.assumption + ] + ] +qed. + +theorem gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n. +intro.apply (nat_case n) + [intros.reflexivity + |intros. + apply le_to_le_to_eq + [apply divides_to_le + [apply lt_O_S|apply divides_gcd_n] + |apply divides_to_le + [apply lt_O_gcd.rewrite > (times_n_O O). + apply lt_times[apply lt_O_S|assumption] + |apply divides_d_gcd + [apply (witness ? ? m1).reflexivity + |apply divides_n_n + ] + ] + ] + ] +qed. + theorem symmetric_gcd: symmetric nat gcd. (*CSC: bug here: unfold symmetric does not work *) change with @@ -440,6 +508,41 @@ qed. (* for the "converse" of the previous result see the end of this development *) +theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to +(gcd n m) = (S O) \to \lnot (divides n m). +intros.unfold.intro. +elim H2. +generalize in match H1. +rewrite > H3. +intro. +cut (O < n2) + [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4) + [cut (gcd n (n*n2) = n) + [apply (lt_to_not_eq (S O) n) + [assumption|rewrite < H4.assumption] + |apply gcd_n_times_nm.assumption + ] + |apply (trans_lt ? (S O))[apply le_n|assumption] + |assumption + ] + |elim (le_to_or_lt_eq O n2 (le_O_n n2)) + [assumption + |apply False_ind. + apply (le_to_not_lt n (S O)) + [rewrite < H4. + apply divides_to_le + [rewrite > H4.apply lt_O_S + |apply divides_d_gcd + [apply (witness ? ? n2).reflexivity + |apply divides_n_n + ] + ] + |assumption + ] + ] + ] +qed. + theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O). intro. apply antisym_le.apply divides_to_le.unfold lt.apply le_n. diff --git a/matita/library/nat/iteration.ma b/matita/library/nat/iteration.ma deleted file mode 100644 index 404cbbded..000000000 --- a/matita/library/nat/iteration.ma +++ /dev/null @@ -1,904 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/nat/iteration.ma". - -include "nat/permutation.ma". -include "nat/count.ma". - -lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m. -apply nat_elim2 - [intros.apply le_n_O_to_eq.assumption - |intros.apply sym_eq.apply le_n_O_to_eq.assumption - |intros.apply eq_f.apply H - [apply le_S_S_to_le.assumption - |apply le_S_S_to_le.assumption - ] - ] -qed. - -let rec map_iter_P n p (g:nat \to nat) (a:nat) f \def - match n with - [ O \Rightarrow a - | (S k) \Rightarrow - match p (S k) with - [true \Rightarrow f (g (S k)) (map_iter_P k p g a f) - |false \Rightarrow map_iter_P k p g a f] - ]. - -theorem eq_map_iter_P: \forall g1,g2:nat \to nat. -\forall p:nat \to bool. -\forall f:nat \to nat \to nat. \forall a,n:nat. -(\forall m:nat. m \le n \to g1 m = g2 m) \to -map_iter_P n p g1 a f = map_iter_P n p g2 a f. -intros 6.elim n - [simplify.reflexivity. - |simplify.elim (p (S n1)) - [simplify.apply eq_f2 - [apply H1.apply le_n - |simplify.apply H.intros.apply H1. - apply le_S.assumption - ] - |simplify.apply H.intros.apply H1. - apply le_S.assumption - ] - ] -qed. - -(* useful since simply simpifies too much *) - -theorem map_iter_P_O: \forall p.\forall g.\forall f. \forall a:nat. -map_iter_P O p g a f = a. -intros.simplify.reflexivity. -qed. - -theorem map_iter_P_S_true: \forall p.\forall g.\forall f. \forall a,n:nat. -p (S n) = true \to -map_iter_P (S n) p g a f = f (g (S n)) (map_iter_P n p g a f). -intros.simplify.rewrite > H.reflexivity. -qed. - -theorem map_iter_P_S_false: \forall p.\forall g.\forall f. \forall a,n:nat. -p (S n) = false \to -map_iter_P (S n) p g a f = map_iter_P n p g a f. -intros.simplify.rewrite > H.reflexivity. -qed. - -(* map_iter examples *) -definition Pi_P \def \lambda p. \lambda n. -map_iter_P n p (\lambda n.n) (S O) times. - -lemma Pi_P_S: \forall n.\forall p. -Pi_P p (S n) = - match p (S n) with - [true \Rightarrow (S n)*(Pi_P p n) - |false \Rightarrow (Pi_P p n) - ]. -intros.reflexivity. -qed. - -lemma lt_O_Pi_P: \forall n.\forall p. -O < Pi_P p n. -intros.elim n - [simplify.apply le_n - |rewrite > Pi_P_S. - elim p (S n1) - [change with (O < (S n1)*(Pi_P p n1)). - rewrite >(times_n_O n1). - apply lt_times[apply le_n|assumption] - | assumption - ] - ] -qed. - -let rec card n p \def - match n with - [O \Rightarrow O - |(S m) \Rightarrow - (bool_to_nat (p (S m))) + (card m p)]. - -lemma a_times_Pi_P: \forall p. \forall a,n. -exp a (card n p) * Pi_P p n = map_iter_P n p (\lambda n.a*n) (S O) times. -intros.elim n - [simplify.reflexivity - |simplify.apply (bool_elim ? (p (S n1))) - [intro. - change with - (a*exp a (card n1 p) * ((S n1) * (Pi_P p n1)) = - a*(S n1)*map_iter_P n1 p (\lambda n.a*n) (S O) times). - rewrite < H. - auto - |intro.assumption - ] - ] -qed. - -definition permut_p \def \lambda f. \lambda p:nat\to bool. \lambda n. -\forall i. i \le n \to p i = true \to ((f i \le n \land p (f i) = true) -\land (\forall j. p j = true \to j \le n \to i \neq j \to (f i \neq f j))). - -definition extentional_eq_n \def \lambda f,g:nat \to nat.\lambda n. -\forall x. x \le n \to f x = g x. - -lemma extentional_eq_n_to_permut_p: \forall f,g. \forall p. \forall n. -extentional_eq_n f g n\to permut_p f p n \to permut_p g p n. -intros.unfold permut_p. -intros. -elim (H1 i H2 H3). -split - [elim H4.split - [rewrite < (H i H2).assumption - |rewrite < (H i H2).assumption - ] - |intros. - unfold.intro.apply (H5 j H6 H7 H8). - rewrite > (H i H2). - rewrite > (H j H7).assumption - ] -qed. - -theorem permut_p_compose: \forall f,g.\forall p.\forall n. -permut_p f p n \to permut_p g p n \to permut_p (compose ? ? ? g f) p n. -intros.unfold permut_p.intros. -elim (H i H2 H3). -elim H4. -elim (H1 (f i) H6 H7). -elim H8. -split - [split - [unfold compose.assumption - |unfold compose.rewrite < H11.reflexivity - ] - |intros. - unfold compose. - apply (H9 (f j)) - [elim (H j H13 H12).elim H15.rewrite < H18.reflexivity - |elim (H j H13 H12).elim H15.assumption. - |apply (H5 j H12 H13 H14) - ] - ] -qed. - -theorem permut_p_S_to_permut_p: \forall f.\forall p.\forall n. -permut_p f p (S n) \to (f (S n)) = (S n) \to permut_p f p n. -intros. -unfold permut_p. -intros. -split - [elim (H i (le_S i n H2) H3).split - [elim H4. - elim (le_to_or_lt_eq (f i) (S n)) - [apply le_S_S_to_le.assumption - |absurd (f i = (S n)) - [assumption - |rewrite < H1. - apply H5 - [rewrite < H8.assumption - |apply le_n - |unfold.intro.rewrite > H8 in H2. - apply (not_le_Sn_n n).rewrite < H9.assumption - ] - ] - |assumption - ] - |elim H4.assumption - ] - |intros. - elim (H i (le_S i n H2) H3). - apply H8 - [assumption|apply le_S.assumption|assumption] - ] -qed. - -lemma permut_p_transpose: \forall p.\forall i,j,n. -i \le n \to j \le n \to p i = p j \to -permut_p (transpose i j) p n. -unfold permut_p.intros. -split - [split - [unfold transpose. - apply (eqb_elim i1 i) - [intro. - apply (eqb_elim i1 j) - [simplify.intro.assumption - |simplify.intro.assumption - ] - |intro. - apply (eqb_elim i1 j) - [simplify.intro.assumption - |simplify.intro.assumption - ] - ] - |unfold transpose. - apply (eqb_elim i1 i) - [intro. - apply (eqb_elim i1 j) - [simplify.intro.rewrite < H6.assumption - |simplify.intro.rewrite < H2.rewrite < H5.assumption - ] - |intro. - apply (eqb_elim i1 j) - [simplify.intro.rewrite > H2.rewrite < H6.assumption - |simplify.intro.assumption - ] - ] - ] - |intros.unfold Not. - intro.apply H7. - apply (injective_transpose ? ? ? ? H8). - ] -qed. - -theorem eq_map_iter_P_k: \forall f,g.\forall p.\forall a,k,n:nat. -p (S n-k) = true \to (\forall i. (S n)-k < i \to i \le (S n) \to (p i) = false) \to -map_iter_P (S n) p g a f = map_iter_P (S n-k) p g a f. -intros 5. -elim k 3 - [rewrite < minus_n_O.reflexivity - |apply (nat_case n1) - [intros. - rewrite > map_iter_P_S_false - [reflexivity - |apply H2[simplify.apply lt_O_S.|apply le_n] - ] - |intros. - rewrite > map_iter_P_S_false - [rewrite > (H m H1) - [reflexivity - |intros. - apply (H2 i H3). - apply le_S. - assumption - ] - |apply H2[auto|apply le_n] - ] - ] - ] -qed. - -theorem eq_map_iter_p_a: \forall p.\forall f.\forall g. \forall a,n:nat. -(\forall i.i \le n \to p i = false) \to map_iter_P n p g a f = a. -intros 5. -elim n - [simplify.reflexivity - |rewrite > map_iter_P_S_false - [apply H. - intros. - apply H1.apply le_S.assumption - |apply H1.apply le_n - ] - ] -qed. - -theorem eq_map_iter_p_transpose: \forall p.\forall f.associative nat f \to -symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. k < n \to -(p (S n) = true) \to (p (n-k)) = true \to (\forall i. n-k < i \to i \le n \to (p i) = false) -\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. -intros 8. -apply (nat_case n) - [intro.absurd (k < O) - [assumption|apply le_to_not_lt.apply le_O_n] - |intros. - rewrite > (map_iter_P_S_true ? ? ? ? ? H3). - rewrite > (map_iter_P_S_true ? ? ? ? ? H3). - rewrite > (eq_map_iter_P_k ? ? ? ? ? ? H4 H5). - rewrite > (eq_map_iter_P_k ? ? ? ? ? ? H4 H5). - generalize in match H4. - rewrite > minus_Sn_m - [intro. - rewrite > (map_iter_P_S_true ? ? ? ? ? H6). - rewrite > (map_iter_P_S_true ? ? ? ? ? H6). - rewrite > transpose_i_j_j. - rewrite > transpose_i_j_i. - cut (map_iter_P (m-k) p g a f = - map_iter_P (m-k) p (\lambda x.g (transpose (S(m-k)) (S(S m)) x)) a f) - [rewrite < Hcut. - rewrite < H. - rewrite < H1 in \vdash (? ? (? % ?) ?). - rewrite > H. - reflexivity - |apply eq_map_iter_P. - intros.unfold transpose. - cut (eqb m1 (S (m-k)) =false) - [cut (eqb m1 (S (S m)) =false) - [rewrite > Hcut. - rewrite > Hcut1. - reflexivity - |apply not_eq_to_eqb_false. - apply lt_to_not_eq. - apply (le_to_lt_to_lt ? m) - [apply (trans_le ? (m-k)) - [assumption|auto] - |apply le_S.apply le_n - ] - ] - |apply not_eq_to_eqb_false. - apply lt_to_not_eq. - unfold.auto - ] - ] - |apply le_S_S_to_le.assumption - ] - ] -qed. - -theorem eq_map_iter_p_transpose1: \forall p.\forall f.associative nat f \to -symmetric2 nat nat f \to \forall g. \forall a,k1,k2,n:nat. O < k1 \to k1 < k2 \to k2 \le n \to -(p k1) = true \to (p k2) = true \to (\forall i. k1 < i \to i < k2 \to (p i) = false) -\to map_iter_P n p g a f = map_iter_P n p (\lambda m. g (transpose k1 k2 m)) a f. -intros 10. -elim n 2 - [absurd (k2 \le O) - [assumption|apply lt_to_not_le.apply (trans_lt ? k1 ? H2 H3)] - |apply (eqb_elim (S n1) k2) - [intro. - rewrite < H4. - intros. - cut (k1 = n1 - (n1 -k1)) - [rewrite > Hcut. - apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1)) - [cut (k1 \le n1)[auto|auto] - |assumption - |rewrite < Hcut.assumption - |rewrite < Hcut.intros. - apply (H9 i H10).unfold.auto - ] - |apply sym_eq. - apply plus_to_minus. - auto. - ] - |intros. - cut ((S n1) \neq k1) - [apply (bool_elim ? (p (S n1))) - [intro. - rewrite > map_iter_P_S_true - [rewrite > map_iter_P_S_true - [cut ((transpose k1 k2 (S n1)) = (S n1)) - [rewrite > Hcut1. - apply eq_f. - apply (H3 H5) - [elim (le_to_or_lt_eq ? ? H6) - [auto - |absurd (S n1=k2)[apply sym_eq.assumption|assumption] - ] - |assumption - |assumption - |assumption - ] - |unfold transpose. - rewrite > (not_eq_to_eqb_false ? ? Hcut). - rewrite > (not_eq_to_eqb_false ? ? H4). - reflexivity - ] - |assumption - ] - |assumption - ] - |intro. - rewrite > map_iter_P_S_false - [rewrite > map_iter_P_S_false - [apply (H3 H5) - [elim (le_to_or_lt_eq ? ? H6) - [auto - |absurd (S n1=k2)[apply sym_eq.assumption|assumption] - ] - |assumption - |assumption - |assumption - ] - |assumption - ] - |assumption - ] - ] - |unfold.intro. - absurd (k1 < k2) - [assumption - |apply le_to_not_lt. - rewrite < H10. - assumption - ] - ] - ] - ] -qed. - -lemma decidable_n:\forall p.\forall n. -(\forall m. m \le n \to (p m) = false) \lor -(\exists m. m \le n \land (p m) = true \land -\forall i. m < i \to i \le n \to (p i) = false). -intros. -elim n - [apply (bool_elim ? (p O)) - [intro.right. - apply (ex_intro ? ? O). - split - [split[apply le_n|assumption] - |intros.absurd (O H4.assumption - ] - |right. - elim H1.elim H3.elim H4. - apply (ex_intro ? ? a). - split - [split[apply le_S.assumption|assumption] - |intros.elim (le_to_or_lt_eq i (S n1) H9) - [apply H5[assumption|apply le_S_S_to_le.assumption] - |rewrite > H10.assumption - ] - ] - ] - ] - ] -qed. - -lemma decidable_n1:\forall p.\forall n,j. j \le n \to (p j)=true \to -(\forall m. j < m \to m \le n \to (p m) = false) \lor -(\exists m. j < m \land m \le n \land (p m) = true \land -\forall i. m < i \to i \le n \to (p i) = false). -intros. -elim (decidable_n p n) - [absurd ((p j)=true) - [assumption - |unfold.intro. - apply not_eq_true_false. - rewrite < H3. - apply H2.assumption - ] - |elim H2.clear H2. - apply (nat_compare_elim j a) - [intro. - right. - apply (ex_intro ? ? a). - elim H3.clear H3. - elim H4.clear H4. - split - [split - [split - [assumption|assumption] - |assumption - ] - |assumption - ] - |intro. - rewrite > H2. - left. - elim H3 2.assumption - |intro. - absurd (p j = true) - [assumption - |unfold.intro. - apply not_eq_true_false. - rewrite < H4. - elim H3.clear H3. - apply (H6 j H2).assumption - ] - ] - ] -qed. - -lemma decidable_n2:\forall p.\forall n,j. j \le n \to (p j)=true \to -(\forall m. j < m \to m \le n \to (p m) = false) \lor -(\exists m. j < m \land m \le n \land (p m) = true \land -\forall i. j < i \to i < m \to (p i) = false). -intros 3. -elim n - [left. - apply (le_n_O_elim j H).intros. - absurd (m \le O) - [assumption|apply lt_to_not_le.assumption] - |elim (le_to_or_lt_eq ? ? H1) - [cut (j \le n1) - [elim (H Hcut H2) - [apply (bool_elim ? (p (S n1))) - [intro. - right. - apply (ex_intro ? ? (S n1)). - split - [split - [split - [assumption|apply le_n] - |assumption - ] - |intros. - apply (H4 i H6). - apply le_S_S_to_le. - assumption - ] - |intro. - left. - intros. - elim (le_to_or_lt_eq ? ? H7) - [apply H4 - [assumption|apply le_S_S_to_le.assumption] - |rewrite > H8.assumption - ] - ] - |right. - elim H4.clear H4. - elim H5.clear H5. - elim H4.clear H4. - elim H5.clear H5. - apply (ex_intro ? ? a). - split - [split - [split[assumption|apply le_S.assumption] - |assumption - ] - |assumption - ] - ] - |apply le_S_S_to_le. - assumption - ] - |left. - intros. - absurd (j < m) - [assumption - |apply le_to_not_lt. - rewrite > H3. - assumption - ] - ] - ] -qed. - -(* tutti d spostare *) -theorem lt_minus_to_lt_plus: -\forall n,m,p. n - m < p \to n < m + p. -intros 2. -apply (nat_elim2 ? ? ? ? n m) - [simplify.intros.auto. - |intros 2.rewrite < minus_n_O. - intro.assumption - |intros. - simplify. - cut (n1 < m1+p) - [auto - |apply H. - apply H1 - ] - ] -qed. - -theorem lt_plus_to_lt_minus: -\forall n,m,p. m \le n \to n < m + p \to n - m < p. -intros 2. -apply (nat_elim2 ? ? ? ? n m) - [simplify.intros 3. - apply (le_n_O_elim ? H). - simplify.intros.assumption - |simplify.intros.assumption. - |intros. - simplify. - apply H - [apply le_S_S_to_le.assumption - |apply le_S_S_to_le.apply H2 - ] - ] -qed. - -theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n). -intros. -apply sym_eq. -apply plus_to_minus. -auto. -qed. - -theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to -symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to -(p (S n) = true) \to (p k) = true -\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. -intros 10. -cut (k = (S n)-(S n -k)) - [generalize in match H3.clear H3. - generalize in match g. - generalize in match H2.clear H2. - rewrite > Hcut. - (*generalize in match Hcut.clear Hcut.*) - (* generalize in match H3.clear H3.*) - (* something wrong here - rewrite > Hcut in \vdash (?\rarr ?\rarr %). *) - apply (nat_elim1 (S n - k)). - intros. - elim (decidable_n2 p n (S n -m) H4 H6) - [apply (eq_map_iter_p_transpose1 p f H H1 f1 a) - [assumption. - |unfold.auto. - |apply le_n - |assumption - |assumption - |intros.apply H7 - [assumption|apply le_S_S_to_le.assumption] - ] - |elim H7.clear H7. - elim H8.clear H8. - elim H7.clear H7. - elim H8.clear H8. - apply (trans_eq ? ? - (map_iter_P (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f)) - [apply (trans_eq ? ? - (map_iter_P (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f)) - [cut (a1 = (S n -(S n -a1))) - [rewrite > Hcut1. - apply H2 - [apply lt_plus_to_lt_minus - [apply le_S.assumption - |rewrite < sym_plus. - apply lt_minus_to_lt_plus. - assumption - ] - |rewrite < Hcut1. - apply (trans_lt ? (S n -m))[assumption|assumption] - |rewrite < Hcut1.assumption - |assumption - |rewrite < Hcut1.assumption - ] - |apply minus_m_minus_mn. - apply le_S.assumption - ] - |apply (eq_map_iter_p_transpose1 p f H H1) - [assumption - |assumption - |apply le_S.assumption - |assumption - |assumption - |assumption - ] - ] - |apply (trans_eq ? ? - (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)) - [cut (a1 = (S n) -(S n -a1)) - [apply H2 - [apply lt_plus_to_lt_minus - [apply le_S.assumption - |rewrite < sym_plus. - apply lt_minus_to_lt_plus. - assumption - ] - |rewrite < Hcut1. - apply (trans_lt ? (S n -m))[assumption|assumption] - |rewrite < Hcut1.assumption - |assumption - |rewrite < Hcut1.assumption - ] - |apply minus_m_minus_mn. - apply le_S.assumption - ] - |apply eq_map_iter_P. - cut (a1 = (S n) -(S n -a1)) - [intros. - apply eq_f. - rewrite < Hcut1. - rewrite < transpose_i_j_j_i. - rewrite > (transpose_i_j_j_i (S n -m)). - rewrite > (transpose_i_j_j_i a1 (S n)). - rewrite > (transpose_i_j_j_i (S n -m)). - apply sym_eq. - apply eq_transpose - [unfold.intro. - apply (not_le_Sn_n n). - rewrite < H12.assumption - |unfold.intro. - apply (not_le_Sn_n n). - rewrite > H12.assumption - |unfold.intro. - apply (not_le_Sn_n a1). - rewrite < H12 in \vdash (? (? %) ?).assumption - ] - |apply minus_m_minus_mn. - apply le_S.assumption - ] - ] - ] - ] - |apply minus_m_minus_mn. - apply le_S.assumption - ] -qed. - -theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to -symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to -(p (S n) = true) \to (p k) = true -\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. -intros. -elim (le_to_or_lt_eq ? ? H3) - [apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2) - [apply le_S_S_to_le.assumption|assumption|assumption] - |rewrite > H6. - apply eq_map_iter_P. - intros. - apply eq_f.apply sym_eq. apply transpose_i_i. - ] -qed. - -lemma permut_p_O: \forall p.\forall h.\forall n. -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). -intros.unfold permut_p in H. -apply not_le_to_lt.unfold.intro. -elim (H (S m) H2 H3). -elim H5. -absurd (p (h (S m)) = true) - [assumption - |apply (le_n_O_elim ? H4). - unfold.intro. - apply not_eq_true_false. - rewrite < H9.rewrite < H1.reflexivity - ] -qed. - -theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to -symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat. -permut_p h p n \to p O = false \to -map_iter_P n p g a f = map_iter_P n p (compose ? ? ? g h) a f . -intros 5. -elim n - [simplify.reflexivity - |apply (bool_elim ? (p (S n1))) - [intro. - apply (trans_eq ? ? (map_iter_P (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f)) - [unfold permut_p in H3. - elim (H3 (S n1) (le_n ?) H5). - elim H6. clear H6. - apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1) - [apply (permut_p_O ? ? ? H3 H4) - [apply le_n|assumption] - |assumption - |assumption - |assumption - ] - |apply (trans_eq ? ? (map_iter_P (S n1) p (\lambda m. - (g(transpose (h (S n1)) (S n1) - (transpose (h (S n1)) (S n1) (h m)))) ) a f)) - [rewrite > (map_iter_P_S_true ? ? ? ? ? H5). - rewrite > (map_iter_P_S_true ? ? ? ? ? H5). - apply eq_f2 - [rewrite > transpose_i_j_j. - rewrite > transpose_i_j_i. - rewrite > transpose_i_j_j. - reflexivity - |apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?) - [unfold.intros. - split - [split - [simplify. - unfold permut_p in H3. - elim (H3 i (le_S ? ? H6) H7). - elim H8. clear H8. - elim (le_to_or_lt_eq ? ? H10) - [unfold transpose. - rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)). - cut (h i \neq h (S n1)) - [rewrite > (not_eq_to_eqb_false ? ? Hcut). - simplify. - apply le_S_S_to_le. - assumption - |apply H9 - [apply H5 - |apply le_n - |apply lt_to_not_eq. - unfold.apply le_S_S.assumption - ] - ] - |rewrite > H8. - apply (eqb_elim (S n1) (h (S n1))) - [intro. - absurd (h i = h (S n1)) - [rewrite > H8. - assumption - |apply H9 - [assumption - |apply le_n - |apply lt_to_not_eq. - unfold.apply le_S_S.assumption - ] - ] - |intro. - unfold transpose. - rewrite > (not_eq_to_eqb_false ? ? H12). - rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))). - simplify. - elim (H3 (S n1) (le_n ? ) H5). - elim H13.clear H13. - elim (le_to_or_lt_eq ? ? H15) - [apply le_S_S_to_le.assumption - |apply False_ind. - apply H12. - apply sym_eq.assumption - ] - ] - ] - |simplify. - unfold permut_p in H3. - unfold transpose. - apply (eqb_elim (h i) (S n1)) - [intro. - apply (eqb_elim (h i) (h (S n1))) - [intro.simplify.assumption - |intro.simplify. - elim (H3 (S n1) (le_n ? ) H5). - elim H10. assumption - ] - |intro. - apply (eqb_elim (h i) (h (S n1))) - [intro.simplify.assumption - |intro.simplify. - elim (H3 i (le_S ? ? H6) H7). - elim H10. assumption - ] - ] - ] - |simplify.intros.unfold Not.intro. - unfold permut_p in H3. - elim (H3 i (le_S i ? H6) H7). - apply (H13 j H8 (le_S j ? H9) H10). - apply (injective_transpose ? ? ? ? H11) - ] - |assumption - ] - ] - |apply eq_map_iter_P. - intros. - rewrite > transpose_transpose.reflexivity - ] - ] - |intro. - rewrite > (map_iter_P_S_false ? ? ? ? ? H5). - rewrite > (map_iter_P_S_false ? ? ? ? ? H5). - apply H2 - [unfold permut_p. - unfold permut_p in H3. - intros. - elim (H3 i (le_S i ? H6) H7). - elim H8. - split - [split - [elim (le_to_or_lt_eq ? ? H10) - [apply le_S_S_to_le.assumption - |absurd (p (h i) = true) - [assumption - |rewrite > H12. - rewrite > H5. - unfold.intro.apply not_eq_true_false. - apply sym_eq.assumption - ] - ] - |assumption - ] - |intros. - apply H9 - [assumption|apply (le_S ? ? H13)|assumption] - ] - |assumption - ] - ] - ] -qed. - diff --git a/matita/library/nat/map_iter_p.ma b/matita/library/nat/map_iter_p.ma new file mode 100644 index 000000000..c263076aa --- /dev/null +++ b/matita/library/nat/map_iter_p.ma @@ -0,0 +1,912 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat/map_iter_p.ma". + +include "nat/permutation.ma". +include "nat/count.ma". + +let rec map_iter_p n p (g:nat \to nat) (a:nat) f \def + match n with + [ O \Rightarrow a + | (S k) \Rightarrow + match p (S k) with + [true \Rightarrow f (g (S k)) (map_iter_p k p g a f) + |false \Rightarrow map_iter_p k p g a f] + ]. + +theorem eq_map_iter_p: \forall g1,g2:nat \to nat. +\forall p:nat \to bool. +\forall f:nat \to nat \to nat. \forall a,n:nat. +(\forall m:nat. m \le n \to g1 m = g2 m) \to +map_iter_p n p g1 a f = map_iter_p n p g2 a f. +intros 6.elim n + [simplify.reflexivity. + |simplify.elim (p (S n1)) + [simplify.apply eq_f2 + [apply H1.apply le_n + |simplify.apply H.intros.apply H1. + apply le_S.assumption + ] + |simplify.apply H.intros.apply H1. + apply le_S.assumption + ] + ] +qed. + +(* useful since simplify simpifies too much *) + +theorem map_iter_p_O: \forall p.\forall g.\forall f. \forall a:nat. +map_iter_p O p g a f = a. +intros.simplify.reflexivity. +qed. + +theorem map_iter_p_S_true: \forall p.\forall g.\forall f. \forall a,n:nat. +p (S n) = true \to +map_iter_p (S n) p g a f = f (g (S n)) (map_iter_p n p g a f). +intros.simplify.rewrite > H.reflexivity. +qed. + +theorem map_iter_p_S_false: \forall p.\forall g.\forall f. \forall a,n:nat. +p (S n) = false \to +map_iter_p (S n) p g a f = map_iter_p n p g a f. +intros.simplify.rewrite > H.reflexivity. +qed. + +(* map_iter examples *) +definition pi_p \def \lambda p. \lambda n. +map_iter_p n p (\lambda n.n) (S O) times. + +lemma pi_p_S: \forall n.\forall p. +pi_p p (S n) = + match p (S n) with + [true \Rightarrow (S n)*(pi_p p n) + |false \Rightarrow (pi_p p n) + ]. +intros.reflexivity. +qed. + +lemma lt_O_pi_p: \forall n.\forall p. +O < pi_p p n. +intros.elim n + [simplify.apply le_n + |rewrite > pi_p_S. + elim p (S n1) + [change with (O < (S n1)*(pi_p p n1)). + rewrite >(times_n_O n1). + apply lt_times[apply le_n|assumption] + | assumption + ] + ] +qed. + +let rec card n p \def + match n with + [O \Rightarrow O + |(S m) \Rightarrow + (bool_to_nat (p (S m))) + (card m p)]. + +lemma count_card: \forall p.\forall n. +p O = false \to count (S n) p = card n p. +intros.elim n + [simplify.rewrite > H. reflexivity + |simplify. + rewrite < plus_n_O. + apply eq_f.assumption + ] +qed. + +lemma count_card1: \forall p.\forall n. +p O = false \to p n = false \to count n p = card n p. +intros 3.apply (nat_case n) + [intro.simplify.rewrite > H. reflexivity + |intros.rewrite > (count_card ? ? H). + simplify.rewrite > H1.reflexivity + ] +qed. + +lemma a_times_pi_p: \forall p. \forall a,n. +exp a (card n p) * pi_p p n = map_iter_p n p (\lambda n.a*n) (S O) times. +intros.elim n + [simplify.reflexivity + |simplify.apply (bool_elim ? (p (S n1))) + [intro. + change with + (a*exp a (card n1 p) * ((S n1) * (pi_p p n1)) = + a*(S n1)*map_iter_p n1 p (\lambda n.a*n) (S O) times). + rewrite < H. + auto + |intro.assumption + ] + ] +qed. + +definition permut_p \def \lambda f. \lambda p:nat\to bool. \lambda n. +\forall i. i \le n \to p i = true \to ((f i \le n \land p (f i) = true) +\land (\forall j. p j = true \to j \le n \to i \neq j \to (f i \neq f j))). + +definition extentional_eq_n \def \lambda f,g:nat \to nat.\lambda n. +\forall x. x \le n \to f x = g x. + +lemma extentional_eq_n_to_permut_p: \forall f,g. \forall p. \forall n. +extentional_eq_n f g n\to permut_p f p n \to permut_p g p n. +intros.unfold permut_p. +intros. +elim (H1 i H2 H3). +split + [elim H4.split + [rewrite < (H i H2).assumption + |rewrite < (H i H2).assumption + ] + |intros. + unfold.intro.apply (H5 j H6 H7 H8). + rewrite > (H i H2). + rewrite > (H j H7).assumption + ] +qed. + +theorem permut_p_compose: \forall f,g.\forall p.\forall n. +permut_p f p n \to permut_p g p n \to permut_p (compose ? ? ? g f) p n. +intros.unfold permut_p.intros. +elim (H i H2 H3). +elim H4. +elim (H1 (f i) H6 H7). +elim H8. +split + [split + [unfold compose.assumption + |unfold compose.rewrite < H11.reflexivity + ] + |intros. + unfold compose. + apply (H9 (f j)) + [elim (H j H13 H12).elim H15.rewrite < H18.reflexivity + |elim (H j H13 H12).elim H15.assumption. + |apply (H5 j H12 H13 H14) + ] + ] +qed. + +theorem permut_p_S_to_permut_p: \forall f.\forall p.\forall n. +permut_p f p (S n) \to (f (S n)) = (S n) \to permut_p f p n. +intros. +unfold permut_p. +intros. +split + [elim (H i (le_S i n H2) H3).split + [elim H4. + elim (le_to_or_lt_eq (f i) (S n)) + [apply le_S_S_to_le.assumption + |absurd (f i = (S n)) + [assumption + |rewrite < H1. + apply H5 + [rewrite < H8.assumption + |apply le_n + |unfold.intro.rewrite > H8 in H2. + apply (not_le_Sn_n n).rewrite < H9.assumption + ] + ] + |assumption + ] + |elim H4.assumption + ] + |intros. + elim (H i (le_S i n H2) H3). + apply H8 + [assumption|apply le_S.assumption|assumption] + ] +qed. + +lemma permut_p_transpose: \forall p.\forall i,j,n. +i \le n \to j \le n \to p i = p j \to +permut_p (transpose i j) p n. +unfold permut_p.intros. +split + [split + [unfold transpose. + apply (eqb_elim i1 i) + [intro. + apply (eqb_elim i1 j) + [simplify.intro.assumption + |simplify.intro.assumption + ] + |intro. + apply (eqb_elim i1 j) + [simplify.intro.assumption + |simplify.intro.assumption + ] + ] + |unfold transpose. + apply (eqb_elim i1 i) + [intro. + apply (eqb_elim i1 j) + [simplify.intro.rewrite < H6.assumption + |simplify.intro.rewrite < H2.rewrite < H5.assumption + ] + |intro. + apply (eqb_elim i1 j) + [simplify.intro.rewrite > H2.rewrite < H6.assumption + |simplify.intro.assumption + ] + ] + ] + |intros.unfold Not. + intro.apply H7. + apply (injective_transpose ? ? ? ? H8). + ] +qed. + +theorem eq_map_iter_p_k: \forall f,g.\forall p.\forall a,k,n:nat. +p (S n-k) = true \to (\forall i. (S n)-k < i \to i \le (S n) \to (p i) = false) \to +map_iter_p (S n) p g a f = map_iter_p (S n-k) p g a f. +intros 5. +elim k 3 + [rewrite < minus_n_O.reflexivity + |apply (nat_case n1) + [intros. + rewrite > map_iter_p_S_false + [reflexivity + |apply H2[simplify.apply lt_O_S.|apply le_n] + ] + |intros. + rewrite > map_iter_p_S_false + [rewrite > (H m H1) + [reflexivity + |intros. + apply (H2 i H3). + apply le_S. + assumption + ] + |apply H2[auto|apply le_n] + ] + ] + ] +qed. + +theorem eq_map_iter_p_a: \forall p.\forall f.\forall g. \forall a,n:nat. +(\forall i.i \le n \to p i = false) \to map_iter_p n p g a f = a. +intros 5. +elim n + [simplify.reflexivity + |rewrite > map_iter_p_S_false + [apply H. + intros. + apply H1.apply le_S.assumption + |apply H1.apply le_n + ] + ] +qed. + +theorem eq_map_iter_p_transpose: \forall p.\forall f.associative nat f \to +symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. k < n \to +(p (S n) = true) \to (p (n-k)) = true \to (\forall i. n-k < i \to i \le n \to (p i) = false) +\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. +intros 8. +apply (nat_case n) + [intro.absurd (k < O) + [assumption|apply le_to_not_lt.apply le_O_n] + |intros. + rewrite > (map_iter_p_S_true ? ? ? ? ? H3). + rewrite > (map_iter_p_S_true ? ? ? ? ? H3). + rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5). + rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5). + generalize in match H4. + rewrite > minus_Sn_m + [intro. + rewrite > (map_iter_p_S_true ? ? ? ? ? H6). + rewrite > (map_iter_p_S_true ? ? ? ? ? H6). + rewrite > transpose_i_j_j. + rewrite > transpose_i_j_i. + cut (map_iter_p (m-k) p g a f = + map_iter_p (m-k) p (\lambda x.g (transpose (S(m-k)) (S(S m)) x)) a f) + [rewrite < Hcut. + rewrite < H. + rewrite < H1 in \vdash (? ? (? % ?) ?). + rewrite > H. + reflexivity + |apply eq_map_iter_p. + intros.unfold transpose. + cut (eqb m1 (S (m-k)) =false) + [cut (eqb m1 (S (S m)) =false) + [rewrite > Hcut. + rewrite > Hcut1. + reflexivity + |apply not_eq_to_eqb_false. + apply lt_to_not_eq. + apply (le_to_lt_to_lt ? m) + [apply (trans_le ? (m-k)) + [assumption|auto] + |apply le_S.apply le_n + ] + ] + |apply not_eq_to_eqb_false. + apply lt_to_not_eq. + unfold.auto + ] + ] + |apply le_S_S_to_le.assumption + ] + ] +qed. + +theorem eq_map_iter_p_transpose1: \forall p.\forall f.associative nat f \to +symmetric2 nat nat f \to \forall g. \forall a,k1,k2,n:nat. O < k1 \to k1 < k2 \to k2 \le n \to +(p k1) = true \to (p k2) = true \to (\forall i. k1 < i \to i < k2 \to (p i) = false) +\to map_iter_p n p g a f = map_iter_p n p (\lambda m. g (transpose k1 k2 m)) a f. +intros 10. +elim n 2 + [absurd (k2 \le O) + [assumption|apply lt_to_not_le.apply (trans_lt ? k1 ? H2 H3)] + |apply (eqb_elim (S n1) k2) + [intro. + rewrite < H4. + intros. + cut (k1 = n1 - (n1 -k1)) + [rewrite > Hcut. + apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1)) + [cut (k1 \le n1)[auto|auto] + |assumption + |rewrite < Hcut.assumption + |rewrite < Hcut.intros. + apply (H9 i H10).unfold.auto + ] + |apply sym_eq. + apply plus_to_minus. + auto. + ] + |intros. + cut ((S n1) \neq k1) + [apply (bool_elim ? (p (S n1))) + [intro. + rewrite > map_iter_p_S_true + [rewrite > map_iter_p_S_true + [cut ((transpose k1 k2 (S n1)) = (S n1)) + [rewrite > Hcut1. + apply eq_f. + apply (H3 H5) + [elim (le_to_or_lt_eq ? ? H6) + [auto + |absurd (S n1=k2)[apply sym_eq.assumption|assumption] + ] + |assumption + |assumption + |assumption + ] + |unfold transpose. + rewrite > (not_eq_to_eqb_false ? ? Hcut). + rewrite > (not_eq_to_eqb_false ? ? H4). + reflexivity + ] + |assumption + ] + |assumption + ] + |intro. + rewrite > map_iter_p_S_false + [rewrite > map_iter_p_S_false + [apply (H3 H5) + [elim (le_to_or_lt_eq ? ? H6) + [auto + |absurd (S n1=k2)[apply sym_eq.assumption|assumption] + ] + |assumption + |assumption + |assumption + ] + |assumption + ] + |assumption + ] + ] + |unfold.intro. + absurd (k1 < k2) + [assumption + |apply le_to_not_lt. + rewrite < H10. + assumption + ] + ] + ] + ] +qed. + +lemma decidable_n:\forall p.\forall n. +(\forall m. m \le n \to (p m) = false) \lor +(\exists m. m \le n \land (p m) = true \land +\forall i. m < i \to i \le n \to (p i) = false). +intros. +elim n + [apply (bool_elim ? (p O)) + [intro.right. + apply (ex_intro ? ? O). + split + [split[apply le_n|assumption] + |intros.absurd (O H4.assumption + ] + |right. + elim H1.elim H3.elim H4. + apply (ex_intro ? ? a). + split + [split[apply le_S.assumption|assumption] + |intros.elim (le_to_or_lt_eq i (S n1) H9) + [apply H5[assumption|apply le_S_S_to_le.assumption] + |rewrite > H10.assumption + ] + ] + ] + ] + ] +qed. + +lemma decidable_n1:\forall p.\forall n,j. j \le n \to (p j)=true \to +(\forall m. j < m \to m \le n \to (p m) = false) \lor +(\exists m. j < m \land m \le n \land (p m) = true \land +\forall i. m < i \to i \le n \to (p i) = false). +intros. +elim (decidable_n p n) + [absurd ((p j)=true) + [assumption + |unfold.intro. + apply not_eq_true_false. + rewrite < H3. + apply H2.assumption + ] + |elim H2.clear H2. + apply (nat_compare_elim j a) + [intro. + right. + apply (ex_intro ? ? a). + elim H3.clear H3. + elim H4.clear H4. + split + [split + [split + [assumption|assumption] + |assumption + ] + |assumption + ] + |intro. + rewrite > H2. + left. + elim H3 2.assumption + |intro. + absurd (p j = true) + [assumption + |unfold.intro. + apply not_eq_true_false. + rewrite < H4. + elim H3.clear H3. + apply (H6 j H2).assumption + ] + ] + ] +qed. + +lemma decidable_n2:\forall p.\forall n,j. j \le n \to (p j)=true \to +(\forall m. j < m \to m \le n \to (p m) = false) \lor +(\exists m. j < m \land m \le n \land (p m) = true \land +\forall i. j < i \to i < m \to (p i) = false). +intros 3. +elim n + [left. + apply (le_n_O_elim j H).intros. + absurd (m \le O) + [assumption|apply lt_to_not_le.assumption] + |elim (le_to_or_lt_eq ? ? H1) + [cut (j \le n1) + [elim (H Hcut H2) + [apply (bool_elim ? (p (S n1))) + [intro. + right. + apply (ex_intro ? ? (S n1)). + split + [split + [split + [assumption|apply le_n] + |assumption + ] + |intros. + apply (H4 i H6). + apply le_S_S_to_le. + assumption + ] + |intro. + left. + intros. + elim (le_to_or_lt_eq ? ? H7) + [apply H4 + [assumption|apply le_S_S_to_le.assumption] + |rewrite > H8.assumption + ] + ] + |right. + elim H4.clear H4. + elim H5.clear H5. + elim H4.clear H4. + elim H5.clear H5. + apply (ex_intro ? ? a). + split + [split + [split[assumption|apply le_S.assumption] + |assumption + ] + |assumption + ] + ] + |apply le_S_S_to_le. + assumption + ] + |left. + intros. + absurd (j < m) + [assumption + |apply le_to_not_lt. + rewrite > H3. + assumption + ] + ] + ] +qed. + +(* tutti d spostare *) +theorem lt_minus_to_lt_plus: +\forall n,m,p. n - m < p \to n < m + p. +intros 2. +apply (nat_elim2 ? ? ? ? n m) + [simplify.intros.auto. + |intros 2.rewrite < minus_n_O. + intro.assumption + |intros. + simplify. + cut (n1 < m1+p) + [auto + |apply H. + apply H1 + ] + ] +qed. + +theorem lt_plus_to_lt_minus: +\forall n,m,p. m \le n \to n < m + p \to n - m < p. +intros 2. +apply (nat_elim2 ? ? ? ? n m) + [simplify.intros 3. + apply (le_n_O_elim ? H). + simplify.intros.assumption + |simplify.intros.assumption. + |intros. + simplify. + apply H + [apply le_S_S_to_le.assumption + |apply le_S_S_to_le.apply H2 + ] + ] +qed. + +theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n). +intros. +apply sym_eq. +apply plus_to_minus. +auto. +qed. + +theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to +symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to +(p (S n) = true) \to (p k) = true +\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. +intros 10. +cut (k = (S n)-(S n -k)) + [generalize in match H3.clear H3. + generalize in match g. + generalize in match H2.clear H2. + rewrite > Hcut. + (*generalize in match Hcut.clear Hcut.*) + (* generalize in match H3.clear H3.*) + (* something wrong here + rewrite > Hcut in \vdash (?\rarr ?\rarr %). *) + apply (nat_elim1 (S n - k)). + intros. + elim (decidable_n2 p n (S n -m) H4 H6) + [apply (eq_map_iter_p_transpose1 p f H H1 f1 a) + [assumption. + |unfold.auto. + |apply le_n + |assumption + |assumption + |intros.apply H7 + [assumption|apply le_S_S_to_le.assumption] + ] + |elim H7.clear H7. + elim H8.clear H8. + elim H7.clear H7. + elim H8.clear H8. + apply (trans_eq ? ? + (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f)) + [apply (trans_eq ? ? + (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f)) + [cut (a1 = (S n -(S n -a1))) + [rewrite > Hcut1. + apply H2 + [apply lt_plus_to_lt_minus + [apply le_S.assumption + |rewrite < sym_plus. + apply lt_minus_to_lt_plus. + assumption + ] + |rewrite < Hcut1. + apply (trans_lt ? (S n -m))[assumption|assumption] + |rewrite < Hcut1.assumption + |assumption + |rewrite < Hcut1.assumption + ] + |apply minus_m_minus_mn. + apply le_S.assumption + ] + |apply (eq_map_iter_p_transpose1 p f H H1) + [assumption + |assumption + |apply le_S.assumption + |assumption + |assumption + |assumption + ] + ] + |apply (trans_eq ? ? + (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)) + [cut (a1 = (S n) -(S n -a1)) + [apply H2 + [apply lt_plus_to_lt_minus + [apply le_S.assumption + |rewrite < sym_plus. + apply lt_minus_to_lt_plus. + assumption + ] + |rewrite < Hcut1. + apply (trans_lt ? (S n -m))[assumption|assumption] + |rewrite < Hcut1.assumption + |assumption + |rewrite < Hcut1.assumption + ] + |apply minus_m_minus_mn. + apply le_S.assumption + ] + |apply eq_map_iter_p. + cut (a1 = (S n) -(S n -a1)) + [intros. + apply eq_f. + rewrite < Hcut1. + rewrite < transpose_i_j_j_i. + rewrite > (transpose_i_j_j_i (S n -m)). + rewrite > (transpose_i_j_j_i a1 (S n)). + rewrite > (transpose_i_j_j_i (S n -m)). + apply sym_eq. + apply eq_transpose + [unfold.intro. + apply (not_le_Sn_n n). + rewrite < H12.assumption + |unfold.intro. + apply (not_le_Sn_n n). + rewrite > H12.assumption + |unfold.intro. + apply (not_le_Sn_n a1). + rewrite < H12 in \vdash (? (? %) ?).assumption + ] + |apply minus_m_minus_mn. + apply le_S.assumption + ] + ] + ] + ] + |apply minus_m_minus_mn. + apply le_S.assumption + ] +qed. + +theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to +symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to +(p (S n) = true) \to (p k) = true +\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. +intros. +elim (le_to_or_lt_eq ? ? H3) + [apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2) + [apply le_S_S_to_le.assumption|assumption|assumption] + |rewrite > H6. + apply eq_map_iter_p. + intros. + apply eq_f.apply sym_eq. apply transpose_i_i. + ] +qed. + +lemma permut_p_O: \forall p.\forall h.\forall n. +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). +intros.unfold permut_p in H. +apply not_le_to_lt.unfold.intro. +elim (H (S m) H2 H3). +elim H5. +absurd (p (h (S m)) = true) + [assumption + |apply (le_n_O_elim ? H4). + unfold.intro. + apply not_eq_true_false. + rewrite < H9.rewrite < H1.reflexivity + ] +qed. + +theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to +symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat. +permut_p h p n \to p O = false \to +map_iter_p n p g a f = map_iter_p n p (compose ? ? ? g h) a f . +intros 5. +elim n + [simplify.reflexivity + |apply (bool_elim ? (p (S n1))) + [intro. + apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f)) + [unfold permut_p in H3. + elim (H3 (S n1) (le_n ?) H5). + elim H6. clear H6. + apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1) + [apply (permut_p_O ? ? ? H3 H4) + [apply le_n|assumption] + |assumption + |assumption + |assumption + ] + |apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m. + (g(transpose (h (S n1)) (S n1) + (transpose (h (S n1)) (S n1) (h m)))) ) a f)) + [rewrite > (map_iter_p_S_true ? ? ? ? ? H5). + rewrite > (map_iter_p_S_true ? ? ? ? ? H5). + apply eq_f2 + [rewrite > transpose_i_j_j. + rewrite > transpose_i_j_i. + rewrite > transpose_i_j_j. + reflexivity + |apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?) + [unfold.intros. + split + [split + [simplify. + unfold permut_p in H3. + elim (H3 i (le_S ? ? H6) H7). + elim H8. clear H8. + elim (le_to_or_lt_eq ? ? H10) + [unfold transpose. + rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)). + cut (h i \neq h (S n1)) + [rewrite > (not_eq_to_eqb_false ? ? Hcut). + simplify. + apply le_S_S_to_le. + assumption + |apply H9 + [apply H5 + |apply le_n + |apply lt_to_not_eq. + unfold.apply le_S_S.assumption + ] + ] + |rewrite > H8. + apply (eqb_elim (S n1) (h (S n1))) + [intro. + absurd (h i = h (S n1)) + [rewrite > H8. + assumption + |apply H9 + [assumption + |apply le_n + |apply lt_to_not_eq. + unfold.apply le_S_S.assumption + ] + ] + |intro. + unfold transpose. + rewrite > (not_eq_to_eqb_false ? ? H12). + rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))). + simplify. + elim (H3 (S n1) (le_n ? ) H5). + elim H13.clear H13. + elim (le_to_or_lt_eq ? ? H15) + [apply le_S_S_to_le.assumption + |apply False_ind. + apply H12. + apply sym_eq.assumption + ] + ] + ] + |simplify. + unfold permut_p in H3. + unfold transpose. + apply (eqb_elim (h i) (S n1)) + [intro. + apply (eqb_elim (h i) (h (S n1))) + [intro.simplify.assumption + |intro.simplify. + elim (H3 (S n1) (le_n ? ) H5). + elim H10. assumption + ] + |intro. + apply (eqb_elim (h i) (h (S n1))) + [intro.simplify.assumption + |intro.simplify. + elim (H3 i (le_S ? ? H6) H7). + elim H10. assumption + ] + ] + ] + |simplify.intros.unfold Not.intro. + unfold permut_p in H3. + elim (H3 i (le_S i ? H6) H7). + apply (H13 j H8 (le_S j ? H9) H10). + apply (injective_transpose ? ? ? ? H11) + ] + |assumption + ] + ] + |apply eq_map_iter_p. + intros. + rewrite > transpose_transpose.reflexivity + ] + ] + |intro. + rewrite > (map_iter_p_S_false ? ? ? ? ? H5). + rewrite > (map_iter_p_S_false ? ? ? ? ? H5). + apply H2 + [unfold permut_p. + unfold permut_p in H3. + intros. + elim (H3 i (le_S i ? H6) H7). + elim H8. + split + [split + [elim (le_to_or_lt_eq ? ? H10) + [apply le_S_S_to_le.assumption + |absurd (p (h i) = true) + [assumption + |rewrite > H12. + rewrite > H5. + unfold.intro.apply not_eq_true_false. + apply sym_eq.assumption + ] + ] + |assumption + ] + |intros. + apply H9 + [assumption|apply (le_S ? ? H13)|assumption] + ] + |assumption + ] + ] + ] +qed. + diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma index 587134afc..807906bd2 100644 --- a/matita/library/nat/orders.ma +++ b/matita/library/nat/orders.ma @@ -191,6 +191,18 @@ apply H2.reflexivity. apply H3. apply le_S_S. assumption. qed. +(* le to eq *) +lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m. +apply nat_elim2 + [intros.apply le_n_O_to_eq.assumption + |intros.apply sym_eq.apply le_n_O_to_eq.assumption + |intros.apply eq_f.apply H + [apply le_S_S_to_le.assumption + |apply le_S_S_to_le.assumption + ] + ] +qed. + (* lt and le trans *) theorem lt_O_S : \forall n:nat. O < S n. intro. unfold. apply le_S_S. apply le_O_n. @@ -207,6 +219,12 @@ assumption.apply H2.unfold lt. apply lt_to_le.assumption. qed. +theorem lt_S_to_lt: \forall n,m. S n < m \to n < m. +intros. +apply (trans_lt ? (S n)) + [apply le_n|assumption] +qed. + theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m. intros.apply (le_to_lt_to_lt O n). apply le_O_n.assumption.