From 96d58f0c965040b5fecbb8c36ceb52277b1c78db Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 18 Dec 2006 11:52:57 +0000 Subject: [PATCH] Renamed iterative into map_iter_p and moved around a few theorems. --- matita/library/nat/euler_theorem.ma | 192 +++--------------- matita/library/nat/gcd.ma | 103 ++++++++++ .../nat/{iteration.ma => map_iter_p.ma} | 156 +++++++------- matita/library/nat/orders.ma | 18 ++ 4 files changed, 228 insertions(+), 241 deletions(-) rename matita/library/nat/{iteration.ma => map_iter_p.ma} (86%) 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/map_iter_p.ma similarity index 86% rename from matita/library/nat/iteration.ma rename to matita/library/nat/map_iter_p.ma index 404cbbded..c263076aa 100644 --- a/matita/library/nat/iteration.ma +++ b/matita/library/nat/map_iter_p.ma @@ -12,36 +12,25 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/iteration.ma". +set "baseuri" "cic:/matita/nat/map_iter_p.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 +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] + [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. +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. +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)) @@ -56,45 +45,45 @@ intros 6.elim n ] qed. -(* useful since simply simpifies too much *) +(* 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. +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. +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). +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. +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. +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. +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) = +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) + [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. +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. + |rewrite > pi_p_S. elim p (S n1) - [change with (O < (S n1)*(Pi_P p n1)). + [change with (O < (S n1)*(pi_p p n1)). rewrite >(times_n_O n1). apply lt_times[apply le_n|assumption] | assumption @@ -107,16 +96,35 @@ let rec card n p \def [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. +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). + (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 @@ -240,20 +248,20 @@ split ] qed. -theorem eq_map_iter_P_k: \forall f,g.\forall p.\forall a,k,n:nat. +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. +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 + 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 > map_iter_p_S_false [rewrite > (H m H1) [reflexivity |intros. @@ -268,11 +276,11 @@ elim k 3 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. +(\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 + |rewrite > map_iter_p_S_false [apply H. intros. apply H1.apply le_S.assumption @@ -284,31 +292,31 @@ 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. +\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). + 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 > (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) + 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. + |apply eq_map_iter_p. intros.unfold transpose. cut (eqb m1 (S (m-k)) =false) [cut (eqb m1 (S (S m)) =false) @@ -336,7 +344,7 @@ 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. +\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) @@ -362,8 +370,8 @@ elim n 2 cut ((S n1) \neq k1) [apply (bool_elim ? (p (S n1))) [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 [cut ((transpose k1 k2 (S n1)) = (S n1)) [rewrite > Hcut1. apply eq_f. @@ -386,8 +394,8 @@ elim n 2 |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 [apply (H3 H5) [elim (le_to_or_lt_eq ? ? H6) [auto @@ -615,7 +623,7 @@ 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. +\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. @@ -643,9 +651,9 @@ cut (k = (S n)-(S n -k)) 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)) + (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)) + (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 @@ -674,7 +682,7 @@ cut (k = (S n)-(S n -k)) ] ] |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)) + (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 @@ -692,7 +700,7 @@ cut (k = (S n)-(S n -k)) |apply minus_m_minus_mn. apply le_S.assumption ] - |apply eq_map_iter_P. + |apply eq_map_iter_p. cut (a1 = (S n) -(S n -a1)) [intros. apply eq_f. @@ -727,13 +735,13 @@ 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. +\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. + apply eq_map_iter_p. intros. apply eq_f.apply sym_eq. apply transpose_i_i. ] @@ -757,13 +765,13 @@ 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 . +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)) + 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. @@ -774,11 +782,11 @@ elim n |assumption |assumption ] - |apply (trans_eq ? ? (map_iter_P (S n1) p (\lambda m. + |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). + [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. @@ -864,14 +872,14 @@ elim n |assumption ] ] - |apply eq_map_iter_P. + |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). + rewrite > (map_iter_p_S_false ? ? ? ? ? H5). + rewrite > (map_iter_p_S_false ? ? ? ? ? H5). apply H2 [unfold permut_p. unfold permut_p in H3. 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. -- 2.39.2