From 16a95f57b09ae92ea24ab2addd02c1d0be80f109 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 22 Nov 2010 07:44:58 +0000 Subject: [PATCH] Some arithmetics. --- matita/matita/lib/arithmetics/bigops.ma | 1696 +++++++++++++++++ matita/matita/lib/arithmetics/div_and_mod.ma | 462 +++++ matita/matita/lib/arithmetics/minimization.ma | 304 +++ matita/matita/lib/arithmetics/nat.ma | 1079 +++++++++++ 4 files changed, 3541 insertions(+) create mode 100644 matita/matita/lib/arithmetics/bigops.ma create mode 100644 matita/matita/lib/arithmetics/div_and_mod.ma create mode 100644 matita/matita/lib/arithmetics/minimization.ma create mode 100644 matita/matita/lib/arithmetics/nat.ma diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma new file mode 100644 index 000000000..1bd7c1613 --- /dev/null +++ b/matita/matita/lib/arithmetics/bigops.ma @@ -0,0 +1,1696 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "arithmetics/nat.ma". + +let rec bigop' (n:nat) (filter: nat → bool) (A:Type[0]) (f: nat → A) + (nil: A) (op: A → A → A) ≝ + match n with + [ O ⇒ nil + | S k ⇒ + match filter k with + [true ⇒ op (f k) (bigop' k filter A f nil op) + |false ⇒ bigop' k filter A f nil op] + ]. + +record range (A:Type[0]): Type[0] ≝ + {h:nat→A; upto:nat; filter:nat→bool}. + +definition same_upto: nat → ∀A.relation (range A) ≝ +λk.λA.λI,J. + ∀i. i < k → + ((filter A I i) = (filter A J i) ∧ + ((filter A I i) = true → (h A I i) = (h A J i))). + +definition same: ∀A.relation (range A) ≝ +λA.λI,J. (upto A I = upto A J) ∧ same_upto (upto A I) A I J. + +definition pad: ∀A.nat→range A→range A ≝ + λA.λk.λI.mk_range A (h A I) k + (λi.if_then_else ? (leb (upto A I) i) false (filter A I i)). + +definition same1: ∀A.relation (range A) ≝ +λA.λI,J. + let maxIJ ≝ (max (upto A I) (upto A J)) in + same_upto maxIJ A (pad A maxIJ I) (pad A maxIJ J). + +(* +definition same: ∀A.relation (range A) ≝ +λA.λI,J. + ∀i. i < max (upto A I) (upto A J) → + ((filter A I i) = (filter A J i) ∧ + ((filter A I i) = true → (h A I i) = (h A J i))). *) + +definition bigop: ∀A,B:Type[0].(range A)→B→(B→B→B)→(A→B)→B ≝ + λA,B.λI.λnil.λop.λf. + bigop' (upto A I) (filter A I) B (λx.f(h A I x)) nil op. + +theorem same_bigop: ∀A,B.∀I,J:range A. ∀nil.∀op.∀f. + same A I J → bigop A B I nil op f = bigop A B J nil op f. +#A #B #I #J #nil #op #f * #equp normalize (not_le_to_leb_false …) // @lt_to_not_le // +|#n #leup #Hind normalize (le_to_leb_true … leup) normalize // +] qed. + +theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A. +\forall plusA: A \to A \to A. \forall n. +iter_p_gen n (\lambda x.false) A g baseA plusA = baseA. +intros. +elim n +[ reflexivity +| simplify. + assumption +] +qed. + +theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool. +\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. +(symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA) +\to +iter_p_gen (k + n) p A g baseA plusA += (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA) + (iter_p_gen n p A g baseA plusA)). +intros. + +elim k +[ simplify. + rewrite > H in \vdash (? ? ? %). + rewrite > (H1 ?). + reflexivity +| apply (bool_elim ? (p (n1+n))) + [ intro. + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4). + rewrite > (H2 (g (n1 + n)) ? ?). + rewrite < H3. + reflexivity + | intro. + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4). + assumption + ] +] +qed. + +theorem false_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool. +\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. +n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false) +\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA. +intros 8. +elim H +[ reflexivity +| simplify. + rewrite > H3 + [ simplify. + apply H2. + intros. + apply H3 + [ apply H4 + | apply le_S. + assumption + ] + | assumption + |apply le_n + ] +] +qed. + +(* a therem slightly more general than the previous one *) +theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool. +\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. +(\forall a. plusA baseA a = a) \to +n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA) +\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA. +intros 9. +elim H1 +[reflexivity +|apply (bool_elim ? (p n1));intro + [elim (H4 n1) + [apply False_ind. + apply not_eq_true_false. + rewrite < H5. + rewrite < H6. + reflexivity + |rewrite > true_to_iter_p_gen_Sn + [rewrite > H6. + rewrite > H. + apply H3.intros. + apply H4 + [assumption + |apply le_S.assumption + ] + |assumption + ] + |assumption + |apply le_n + ] + |rewrite > false_to_iter_p_gen_Sn + [apply H3.intros. + apply H4 + [assumption + |apply le_S.assumption + ] + |assumption + ] + ] +] +qed. + +theorem iter_p_gen2 : +\forall n,m:nat. +\forall p1,p2:nat \to bool. +\forall A:Type. +\forall g: nat \to nat \to A. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) +\to +iter_p_gen (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) + A + (\lambda x.g (div x m) (mod x m)) + baseA + plusA = +iter_p_gen n p1 A + (\lambda x.iter_p_gen m p2 A (g x) baseA plusA) + baseA plusA. +intros. +elim n +[ simplify. + reflexivity +| apply (bool_elim ? (p1 n1)) + [ intro. + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + simplify in \vdash (? ? (? % ? ? ? ? ?) ?). + rewrite > iter_p_gen_plusA + [ rewrite < H3. + apply eq_f2 + [ apply eq_iter_p_gen + [ intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify. + reflexivity + | intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + reflexivity. + ] + | reflexivity + ] + | assumption + | assumption + | assumption + ] + | intro. + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + simplify in \vdash (? ? (? % ? ? ? ? ?) ?). + rewrite > iter_p_gen_plusA + [ rewrite > H3. + apply (trans_eq ? ? (plusA baseA + (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA ))) + [ apply eq_f2 + [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m))) + [ apply iter_p_gen_false + | intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify.reflexivity + | intros.reflexivity. + ] + | reflexivity + ] + | rewrite < H. + rewrite > H2. + reflexivity. + ] + | assumption + | assumption + | assumption + ] + ] +] +qed. + +theorem iter_p_gen2': +\forall n,m:nat. +\forall p1: nat \to bool. +\forall p2: nat \to nat \to bool. +\forall A:Type. +\forall g: nat \to nat \to A. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) +\to +iter_p_gen (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m))) + A + (\lambda x.g (div x m) (mod x m)) + baseA + plusA = +iter_p_gen n p1 A + (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA) + baseA plusA. +intros. +elim n +[ simplify. + reflexivity +| apply (bool_elim ? (p1 n1)) + [ intro. + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + simplify in \vdash (? ? (? % ? ? ? ? ?) ?). + rewrite > iter_p_gen_plusA + [ rewrite < H3. + apply eq_f2 + [ apply eq_iter_p_gen + [ intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify. + reflexivity + | intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + reflexivity. + ] + | reflexivity + ] + | assumption + | assumption + | assumption + ] + | intro. + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4). + simplify in \vdash (? ? (? % ? ? ? ? ?) ?). + rewrite > iter_p_gen_plusA + [ rewrite > H3. + apply (trans_eq ? ? (plusA baseA + (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA ))) + [ apply eq_f2 + [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m))) + [ apply iter_p_gen_false + | intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H5). + rewrite > (mod_plus_times ? ? ? H5). + rewrite > H4. + simplify.reflexivity + | intros.reflexivity. + ] + | reflexivity + ] + | rewrite < H. + rewrite > H2. + reflexivity. + ] + | assumption + | assumption + | assumption + ] + ] +] +qed. + +lemma iter_p_gen_gi: +\forall A:Type. +\forall g: nat \to A. +\forall baseA:A. +\forall plusA: A \to A \to A. +\forall n,i:nat. +\forall p:nat \to bool. +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) + \to + +i < n \to p i = true \to +(iter_p_gen n p A g baseA plusA) = +(plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)). +intros 5. +elim n +[ apply False_ind. + apply (not_le_Sn_O i). + assumption +| apply (bool_elim ? (p n1));intro + [ elim (le_to_or_lt_eq i n1) + [ rewrite > true_to_iter_p_gen_Sn + [ rewrite > true_to_iter_p_gen_Sn + [ rewrite < (H2 (g i) ? ?). + rewrite > (H1 (g i) (g n1)). + rewrite > (H2 (g n1) ? ?). + apply eq_f2 + [ reflexivity + | apply H + [ assumption + | assumption + | assumption + | assumption + | assumption + ] + ] + | rewrite > H6.simplify. + change with (notb (eqb n1 i) = notb false). + apply eq_f. + apply not_eq_to_eqb_false. + unfold Not.intro. + apply (lt_to_not_eq ? ? H7). + apply sym_eq.assumption + ] + | assumption + ] + | rewrite > true_to_iter_p_gen_Sn + [ rewrite > H7. + apply eq_f2 + [ reflexivity + | rewrite > false_to_iter_p_gen_Sn + [ apply eq_iter_p_gen + [ intros. + elim (p x) + [ simplify. + change with (notb false = notb (eqb x n1)). + apply eq_f. + apply sym_eq. + apply not_eq_to_eqb_false. + apply (lt_to_not_eq ? ? H8) + | reflexivity + ] + | intros. + reflexivity + ] + | rewrite > H6. + rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)). + reflexivity + ] + ] + | assumption + ] + | apply le_S_S_to_le. + assumption + ] + | rewrite > false_to_iter_p_gen_Sn + [ elim (le_to_or_lt_eq i n1) + [ rewrite > false_to_iter_p_gen_Sn + [ apply H + [ assumption + | assumption + | assumption + | assumption + | assumption + ] + | rewrite > H6.reflexivity + ] + | apply False_ind. + apply not_eq_true_false. + rewrite < H5. + rewrite > H7. + assumption + | apply le_S_S_to_le. + assumption + ] + | assumption + ] + ] +] +qed. + +(* invariance under permutation; single sum *) +theorem eq_iter_p_gen_gh: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to +\forall g: nat \to A. +\forall h,h1: nat \to nat. +\forall n,n1:nat. +\forall p1,p2:nat \to bool. +(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to +(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to +(\forall i. i < n \to p1 i = true \to h i < n1) \to +(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to +(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to +(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to + +iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA = +iter_p_gen n1 p2 A g baseA plusA. +intros 10. +elim n +[ generalize in match H8. + elim n1 + [ reflexivity + | apply (bool_elim ? (p2 n2));intro + [ apply False_ind. + apply (not_le_Sn_O (h1 n2)). + apply H10 + [ apply le_n + | assumption + ] + | rewrite > false_to_iter_p_gen_Sn + [ apply H9. + intros. + apply H10 + [ apply le_S. + apply H12 + | assumption + ] + | assumption + ] + ] + ] +| apply (bool_elim ? (p1 n1));intro + [ rewrite > true_to_iter_p_gen_Sn + [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1)) + [ apply eq_f2 + [ reflexivity + | apply H3 + [ intros. + rewrite > H4 + [ simplify. + change with ((\not eqb (h i) (h n1))= \not false). + apply eq_f. + apply not_eq_to_eqb_false. + unfold Not. + intro. + apply (lt_to_not_eq ? ? H11). + rewrite < H5 + [ rewrite < (H5 n1) + [ apply eq_f. + assumption + | apply le_n + | assumption + ] + | apply le_S. + assumption + | assumption + ] + | apply le_S.assumption + | assumption + ] + | intros. + apply H5 + [ apply le_S. + assumption + | assumption + ] + | intros. + apply H6 + [ apply le_S.assumption + | assumption + ] + | intros. + apply H7 + [ assumption + | generalize in match H12. + elim (p2 j) + [ reflexivity + | assumption + ] + ] + | intros. + apply H8 + [ assumption + | generalize in match H12. + elim (p2 j) + [ reflexivity + | assumption + ] + ] + | intros. + elim (le_to_or_lt_eq (h1 j) n1) + [ assumption + | generalize in match H12. + elim (p2 j) + [ simplify in H13. + absurd (j = (h n1)) + [ rewrite < H13. + rewrite > H8 + [ reflexivity + | assumption + | apply andb_true_true; [2: apply H12] + ] + | apply eqb_false_to_not_eq. + generalize in match H14. + elim (eqb j (h n1)) + [ apply sym_eq.assumption + | reflexivity + ] + ] + | simplify in H14. + apply False_ind. + apply not_eq_true_false. + apply sym_eq.assumption + ] + | apply le_S_S_to_le. + apply H9 + [ assumption + | generalize in match H12. + elim (p2 j) + [ reflexivity + | assumption + ] + ] + ] + ] + ] + | assumption + | assumption + | assumption + | apply H6 + [ apply le_n + | assumption + ] + | apply H4 + [ apply le_n + | assumption + ] + ] + | assumption + ] + | rewrite > false_to_iter_p_gen_Sn + [ apply H3 + [ intros. + apply H4[apply le_S.assumption|assumption] + | intros. + apply H5[apply le_S.assumption|assumption] + | intros. + apply H6[apply le_S.assumption|assumption] + | intros. + apply H7[assumption|assumption] + | intros. + apply H8[assumption|assumption] + | intros. + elim (le_to_or_lt_eq (h1 j) n1) + [ assumption + | absurd (j = (h n1)) + [ rewrite < H13. + rewrite > H8 + [ reflexivity + | assumption + | assumption + ] + | unfold Not.intro. + apply not_eq_true_false. + rewrite < H10. + rewrite < H13. + rewrite > H7 + [ reflexivity + | assumption + | assumption + ] + ] + | apply le_S_S_to_le. + apply H9 + [ assumption + | assumption + ] + ] + ] + | assumption + ] + ] +] +qed. + +theorem eq_iter_p_gen_pred: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +\forall n,p,g. +p O = true \to +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to +iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA = +plusA (iter_p_gen n p A g baseA plusA) (g O). +intros. +elim n + [rewrite > true_to_iter_p_gen_Sn + [simplify.apply H1 + |assumption + ] + |apply (bool_elim ? (p n1));intro + [rewrite > true_to_iter_p_gen_Sn + [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %) + [rewrite > H2 in ⊢ (? ? ? %). + apply eq_f.assumption + |assumption + ] + |assumption + ] + |rewrite > false_to_iter_p_gen_Sn + [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption + |assumption + ] + ] + ] +qed. + +definition p_ord_times \def +\lambda p,m,x. + match p_ord x p with + [pair q r \Rightarrow r*m+q]. + +theorem eq_p_ord_times: \forall p,m,x. +p_ord_times p m x = (ord_rem x p)*m+(ord x p). +intros.unfold p_ord_times. unfold ord_rem. +unfold ord. +elim (p_ord x p). +reflexivity. +qed. + +theorem div_p_ord_times: +\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p. +intros.rewrite > eq_p_ord_times. +apply div_plus_times. +assumption. +qed. + +theorem mod_p_ord_times: +\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p. +intros.rewrite > eq_p_ord_times. +apply mod_plus_times. +assumption. +qed. + +lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m. +intros. +elim (le_to_or_lt_eq O ? (le_O_n m)) + [assumption + |apply False_ind. + rewrite < H1 in H. + rewrite < times_n_O in H. + apply (not_le_Sn_O ? H) + ] +qed. + +theorem iter_p_gen_knm: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to +(associative A plusA) \to +(\forall a:A.(plusA a baseA) = a)\to +\forall g: nat \to A. +\forall h2:nat \to nat \to nat. +\forall h11,h12:nat \to nat. +\forall k,n,m. +\forall p1,p21:nat \to bool. +\forall p22:nat \to nat \to bool. +(\forall x. x < k \to p1 x = true \to +p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true +\land h2 (h11 x) (h12 x) = x +\land (h11 x) < n \land (h12 x) < m) \to +(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to +p1 (h2 i j) = true \land +h11 (h2 i j) = i \land h12 (h2 i j) = j +\land h2 i j < k) \to +iter_p_gen k p1 A g baseA plusA = +iter_p_gen n p21 A (\lambda x:nat.iter_p_gen m (p22 x) A (\lambda y. g (h2 x y)) baseA plusA) baseA plusA. +intros. +rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2). +apply sym_eq. +apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x))) + [intros. + elim (H4 (i/m) (i \mod m));clear H4 + [elim H7.clear H7. + elim H4.clear H4. + assumption + |apply (lt_times_to_lt_div ? ? ? H5) + |apply lt_mod_m_m. + apply (lt_times_to_lt_O ? ? ? H5) + |apply (andb_true_true ? ? H6) + |apply (andb_true_true_r ? ? H6) + ] + |intros. + elim (H4 (i/m) (i \mod m));clear H4 + [elim H7.clear H7. + elim H4.clear H4. + rewrite > H10. + rewrite > H9. + apply sym_eq. + apply div_mod. + apply (lt_times_to_lt_O ? ? ? H5) + |apply (lt_times_to_lt_div ? ? ? H5) + |apply lt_mod_m_m. + apply (lt_times_to_lt_O ? ? ? H5) + |apply (andb_true_true ? ? H6) + |apply (andb_true_true_r ? ? H6) + ] + |intros. + elim (H4 (i/m) (i \mod m));clear H4 + [elim H7.clear H7. + elim H4.clear H4. + assumption + |apply (lt_times_to_lt_div ? ? ? H5) + |apply lt_mod_m_m. + apply (lt_times_to_lt_O ? ? ? H5) + |apply (andb_true_true ? ? H6) + |apply (andb_true_true_r ? ? H6) + ] + |intros. + elim (H3 j H5 H6). + elim H7.clear H7. + elim H9.clear H9. + elim H7.clear H7. + rewrite > div_plus_times + [rewrite > mod_plus_times + [rewrite > H9. + rewrite > H12. + reflexivity. + |assumption + ] + |assumption + ] + |intros. + elim (H3 j H5 H6). + elim H7.clear H7. + elim H9.clear H9. + elim H7.clear H7. + rewrite > div_plus_times + [rewrite > mod_plus_times + [assumption + |assumption + ] + |assumption + ] + |intros. + elim (H3 j H5 H6). + elim H7.clear H7. + elim H9.clear H9. + elim H7.clear H7. + apply (lt_to_le_to_lt ? ((h11 j)*m+m)) + [apply monotonic_lt_plus_r. + assumption + |rewrite > sym_plus. + change with ((S (h11 j)*m) \le n*m). + apply monotonic_le_times_l. + assumption + ] + ] +qed. + +theorem iter_p_gen_divides: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to +\forall g: nat \to A. +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) + +\to + +iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA = +iter_p_gen (S n) (\lambda x.divides_b x n) A + (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA. +intros. +cut (O < p) + [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5). + apply (trans_eq ? ? + (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A + (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m))) baseA plusA) ) + [apply sym_eq. + apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m))) + [ assumption + | assumption + | assumption + |intros. + lapply (divides_b_true_to_lt_O ? ? H H7). + apply divides_to_divides_b_true + [rewrite > (times_n_O O). + apply lt_times + [assumption + |apply lt_O_exp.assumption + ] + |apply divides_times + [apply divides_b_true_to_divides.assumption + |apply (witness ? ? (p \sup (m-i \mod (S m)))). + rewrite < exp_plus_times. + apply eq_f. + rewrite > sym_plus. + apply plus_minus_m_m. + autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S; + ] + ] + |intros. + lapply (divides_b_true_to_lt_O ? ? H H7). + unfold p_ord_times. + rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m)) + [change with ((i/S m)*S m+i \mod S m=i). + apply sym_eq. + apply div_mod. + apply lt_O_S + |assumption + |unfold Not.intro. + apply H2. + apply (trans_divides ? (i/ S m)) + [assumption| + apply divides_b_true_to_divides;assumption] + |apply sym_times. + ] + |intros. + apply le_S_S. + apply le_times + [apply le_S_S_to_le. + change with ((i/S m) < S n). + apply (lt_times_to_lt_l m). + apply (le_to_lt_to_lt ? i);[2:assumption] + autobatch by eq_plus_to_le, div_mod, lt_O_S. + |apply le_exp + [assumption + |apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + ] + ] + |intros. + cut (ord j p < S m) + [rewrite > div_p_ord_times + [apply divides_to_divides_b_true + [apply lt_O_ord_rem + [elim H1.assumption + |apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |cut (n = ord_rem (n*(exp p m)) p) + [rewrite > Hcut2. + apply divides_to_divides_ord_rem + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord_rem. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |assumption + ] + |cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |intros. + cut (ord j p < S m) + [rewrite > div_p_ord_times + [rewrite > mod_p_ord_times + [rewrite > sym_times. + apply sym_eq. + apply exp_ord + [elim H1.assumption + |apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut2. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |assumption + ] + |cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |intros. + rewrite > eq_p_ord_times. + rewrite > sym_plus. + apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m)) + [apply lt_plus_l. + apply le_S_S. + cut (m = ord (n*(p \sup m)) p) + [rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > sym_times. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |reflexivity + ] + ] + |change with (S (ord_rem j p)*S m \le S n*S m). + apply le_times_l. + apply le_S_S. + cut (n = ord_rem (n*(p \sup m)) p) + [rewrite > Hcut1. + apply divides_to_le + [apply lt_O_ord_rem + [elim H1.assumption + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |apply divides_to_divides_ord_rem + [apply (divides_b_true_to_lt_O ? ? ? H7). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + ] + |unfold ord_rem. + rewrite > sym_times. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |reflexivity + ] + ] + ] + ] + |apply eq_iter_p_gen + + [intros. + elim (divides_b (x/S m) n);reflexivity + |intros.reflexivity + ] + ] +|elim H1.apply lt_to_le.assumption +] +qed. + +(*distributive property for iter_p_gen*) +theorem distributive_times_plus_iter_p_gen: \forall A:Type. +\forall plusA: A \to A \to A. \forall basePlusA: A. +\forall timesA: A \to A \to A. +\forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A. +(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a basePlusA) = a) \to +(symmetric A timesA) \to (distributive A timesA plusA) \to +(\forall a:A. (timesA a basePlusA) = basePlusA) + + \to + +((timesA k (iter_p_gen n p A g basePlusA plusA)) = + (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)). +intros. +elim n +[ simplify. + apply H5 +| cut( (p n1) = true \lor (p n1) = false) + [ elim Hcut + [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7). + rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %). + rewrite > (H4). + rewrite > (H3 k (g n1)). + apply eq_f. + assumption + | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7). + rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %). + assumption + ] + | elim ((p n1)) + [ left. + reflexivity + | right. + reflexivity + ] + ] +] +qed. + +(* old version - proved without theorem iter_p_gen_knm +theorem iter_p_gen_2_eq: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to +(associative A plusA) \to +(\forall a:A.(plusA a baseA) = a)\to +\forall g: nat \to nat \to A. +\forall h11,h12,h21,h22: nat \to nat \to nat. +\forall n1,m1,n2,m2. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to +p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true +\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j +\land h11 i j < n1 \land h12 i j < m1) \to +(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to +p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true +\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j +\land (h21 i j) < n2 \land (h22 i j) < m2) \to +iter_p_gen n1 p11 A + (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA) + baseA plusA = +iter_p_gen n2 p21 A + (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA ) + baseA plusA. +intros. +rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2). +rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2). +apply sym_eq. +letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))). +letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))). +apply (trans_eq ? ? + (iter_p_gen (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2)) A + (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1)) baseA plusA )) + [clear h.clear h1. + apply eq_iter_p_gen1 + [intros.reflexivity + |intros. + cut (O < m2) + [cut (x/m2 < n2) + [cut (x \mod m2 < m2) + [elim (and_true ? ? H6). + elim (H3 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + apply eq_f2 + [apply sym_eq. + apply div_plus_times. + assumption + | apply sym_eq. + apply mod_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? x) + [apply (eq_plus_to_le ? ? (x \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + ] + |apply (eq_iter_p_gen_gh ? ? ? H H1 H2 ? h h1);intros + [cut (O < m2) + [cut (i/m2 < n2) + [cut (i \mod m2 < m2) + [elim (and_true ? ? H6). + elim (H3 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = + h11 (i/m2) (i\mod m2)) + [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 = + h12 (i/m2) (i\mod m2)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H9. + rewrite > H15. + reflexivity + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? i) + [apply (eq_plus_to_le ? ? (i \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m2) + [cut (i/m2 < n2) + [cut (i \mod m2 < m2) + [elim (and_true ? ? H6). + elim (H3 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = + h11 (i/m2) (i\mod m2)) + [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 = + h12 (i/m2) (i\mod m2)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H13. + rewrite > H14. + apply sym_eq. + apply div_mod. + assumption + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? i) + [apply (eq_plus_to_le ? ? (i \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m2) + [cut (i/m2 < n2) + [cut (i \mod m2 < m2) + [elim (and_true ? ? H6). + elim (H3 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + apply lt_times_plus_times + [assumption|assumption] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m2) + [assumption + |apply (le_to_lt_to_lt ? i) + [apply (eq_plus_to_le ? ? (i \mod m2)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m1) + [cut (j/m1 < n1) + [cut (j \mod m1 < m1) + [elim (and_true ? ? H6). + elim (H4 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = + h21 (j/m1) (j\mod m1)) + [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 = + h22 (j/m1) (j\mod m1)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H9. + rewrite > H15. + reflexivity + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m1) + [assumption + |apply (le_to_lt_to_lt ? j) + [apply (eq_plus_to_le ? ? (j \mod m1)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m1) + [cut (j/m1 < n1) + [cut (j \mod m1 < m1) + [elim (and_true ? ? H6). + elim (H4 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = + h21 (j/m1) (j\mod m1)) + [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 = + h22 (j/m1) (j\mod m1)) + [rewrite > Hcut3. + rewrite > Hcut4. + rewrite > H13. + rewrite > H14. + apply sym_eq. + apply div_mod. + assumption + |apply mod_plus_times. + assumption + ] + |apply div_plus_times. + assumption + ] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m1) + [assumption + |apply (le_to_lt_to_lt ? j) + [apply (eq_plus_to_le ? ? (j \mod m1)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + |cut (O < m1) + [cut (j/m1 < n1) + [cut (j \mod m1 < m1) + [elim (and_true ? ? H6). + elim (H4 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + apply (lt_times_plus_times ? ? ? m2) + [assumption|assumption] + |apply lt_mod_m_m. + assumption + ] + |apply (lt_times_n_to_lt m1) + [assumption + |apply (le_to_lt_to_lt ? j) + [apply (eq_plus_to_le ? ? (j \mod m1)). + apply div_mod. + assumption + |assumption + ] + ] + ] + |apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H7). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n + ] + ] + ] +qed.*) + + +theorem iter_p_gen_2_eq: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to +(associative A plusA) \to +(\forall a:A.(plusA a baseA) = a)\to +\forall g: nat \to nat \to A. +\forall h11,h12,h21,h22: nat \to nat \to nat. +\forall n1,m1,n2,m2. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to +p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true +\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j +\land h11 i j < n1 \land h12 i j < m1) \to +(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to +p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true +\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j +\land (h21 i j) < n2 \land (h22 i j) < m2) \to +iter_p_gen n1 p11 A + (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA) + baseA plusA = +iter_p_gen n2 p21 A + (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA ) + baseA plusA. + +intros. +rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2). +letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))). +letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))). +letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))). + +apply (trans_eq ? ? +(iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A + (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1))) baseA plusA ) baseA plusA)) +[ + apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros + [ elim (and_true ? ? H6). + cut(O \lt m1) + [ cut(x/m1 < n1) + [ cut((x \mod m1) < m1) + [ elim (H4 ? ? Hcut1 Hcut2 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + split + [ split + [ split + [ split + [ assumption + | assumption + ] + | unfold ha. + unfold ha12. + unfold ha22. + rewrite > H14. + rewrite > H13. + apply sym_eq. + apply div_mod. + assumption + ] + | assumption + ] + | assumption + ] + | apply lt_mod_m_m. + assumption + ] + | apply (lt_times_n_to_lt m1) + [ assumption + | apply (le_to_lt_to_lt ? x) + [ apply (eq_plus_to_le ? ? (x \mod m1)). + apply div_mod. + assumption + | assumption + ] + ] + ] + | apply not_le_to_lt.unfold.intro. + generalize in match H5. + apply (le_n_O_elim ? H9). + rewrite < times_n_O. + apply le_to_not_lt. + apply le_O_n. + ] + | elim (H3 ? ? H5 H6 H7 H8). + elim H9.clear H9. + elim H11.clear H11. + elim H9.clear H9. + elim H11.clear H11. + cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j)) + [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j)) + [ split + [ split + [ split + [ apply true_to_true_to_andb_true + [ rewrite > Hcut. + assumption + | rewrite > Hcut1. + rewrite > Hcut. + assumption + ] + | unfold ha. + unfold ha12. + rewrite > Hcut1. + rewrite > Hcut. + assumption + ] + | unfold ha. + unfold ha22. + rewrite > Hcut1. + rewrite > Hcut. + assumption + ] + | cut(O \lt m1) + [ cut(O \lt n1) + [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) ) + [ unfold ha. + apply (lt_plus_r). + assumption + | rewrite > sym_plus. + rewrite > (sym_times (h11 i j) m1). + rewrite > times_n_Sm. + rewrite > sym_times. + apply (le_times_l). + assumption + ] + | apply not_le_to_lt.unfold.intro. + generalize in match H12. + apply (le_n_O_elim ? H11). + apply le_to_not_lt. + apply le_O_n + ] + | apply not_le_to_lt.unfold.intro. + generalize in match H10. + apply (le_n_O_elim ? H11). + apply le_to_not_lt. + apply le_O_n + ] + ] + | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)). + reflexivity. + assumption + ] + | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)). + reflexivity. + assumption + ] + ] +| apply (eq_iter_p_gen1) + [ intros. reflexivity + | intros. + apply (eq_iter_p_gen1) + [ intros. reflexivity + | intros. + rewrite > (div_plus_times) + [ rewrite > (mod_plus_times) + [ reflexivity + | elim (H3 x x1 H5 H7 H6 H8). + assumption + ] + | elim (H3 x x1 H5 H7 H6 H8). + assumption + ] + ] + ] +] +qed. + +theorem iter_p_gen_iter_p_gen: +\forall A:Type. +\forall baseA: A. +\forall plusA: A \to A \to A. +(symmetric A plusA) \to +(associative A plusA) \to +(\forall a:A.(plusA a baseA) = a)\to +\forall g: nat \to nat \to A. +\forall n,m. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall x,y. x < n \to y < m \to + (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to +iter_p_gen n p11 A + (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA) + baseA plusA = +iter_p_gen m p21 A + (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA ) + baseA plusA. +intros. +apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x) + n m m n p11 p21 p12 p22) + [intros.split + [split + [split + [split + [split + [apply (andb_true_true ? (p12 j i)). + rewrite > H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + |apply (andb_true_true_r (p11 j)). + rewrite > H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + ] + |reflexivity + ] + |reflexivity + ] + |assumption + ] + |assumption + ] + |intros.split + [split + [split + [split + [split + [apply (andb_true_true ? (p22 j i)). + rewrite < H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + |apply (andb_true_true_r (p21 j)). + rewrite < H3 + [rewrite > H6.rewrite > H7.reflexivity + |assumption + |assumption + ] + ] + |reflexivity + ] + |reflexivity + ] + |assumption + ] + |assumption + ] + ] +qed. \ No newline at end of file diff --git a/matita/matita/lib/arithmetics/div_and_mod.ma b/matita/matita/lib/arithmetics/div_and_mod.ma new file mode 100644 index 000000000..b14a44b86 --- /dev/null +++ b/matita/matita/lib/arithmetics/div_and_mod.ma @@ -0,0 +1,462 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "arithmetics/nat.ma". + +let rec mod_aux p m n: nat ≝ +match p with + [ O ⇒ m + | S q ⇒ match (leb m n) with + [ true ⇒ m + | false ⇒ mod_aux q (m-(S n)) n]]. + +definition mod : nat → nat → nat ≝ +λn,m. match m with + [ O ⇒ n + | S p ⇒ mod_aux n n p]. + +interpretation "natural remainder" 'module x y = (mod x y). + +let rec div_aux p m n : nat ≝ +match p with + [ O ⇒ O + | S q ⇒ match (leb m n) with + [ true ⇒ O + | false ⇒ S (div_aux q (m-(S n)) n)]]. + +definition div : nat → nat → nat ≝ +λn,m.match m with + [ O ⇒ S n + | S p ⇒ div_aux n n p]. + +interpretation "natural divide" 'divide x y = (div x y). + +theorem le_mod_aux_m_m: +∀p,n,m. n ≤ p → mod_aux p n m ≤ m. +#p (elim p) +[ normalize #n #m #lenO @(le_n_O_elim …lenO) // +| #q #Hind #n #m #len normalize + @(leb_elim n m) normalize // + #notlenm @Hind @le_plus_to_minus + @(transitive_le … len) /2/ +qed. + +theorem lt_mod_m_m: ∀n,m. O < m → n \mod m < m. +#n #m (cases m) + [#abs @False_ind /2/ + |#p #_ normalize @le_S_S /2/ + ] +qed. + +theorem div_aux_mod_aux: ∀p,n,m:nat. +n=(div_aux p n m)*(S m) + (mod_aux p n m). +#p (elim p) + [#n #m normalize // + |#q #Hind #n #m normalize + @(leb_elim n m) #lenm normalize // + >(associative_plus ???) <(Hind (n-(S m)) m) + applyS plus_minus_m_m (* bello *) /2/ +qed. + +theorem div_mod: ∀n,m:nat. n=(n / m)*m+(n \mod m). +#n #m (cases m) normalize // +qed. + +theorem eq_times_div_minus_mod: +∀a,b:nat. (a / b) * b = a - (a \mod b). +#a #b (applyS minus_plus_m_m) qed. + +inductive div_mod_spec (n,m,q,r:nat) : Prop ≝ +div_mod_spec_intro: r < m → n=q*m+r → div_mod_spec n m q r. + +theorem div_mod_spec_to_not_eq_O: + ∀n,m,q,r.div_mod_spec n m q r → m ≠ O. +#n #m #q #r * /2/ +qed. + +theorem div_mod_spec_div_mod: + ∀n,m. O < m → div_mod_spec n m (n / m) (n \mod m). +#n #m #posm % /2/ qed. + +theorem div_mod_spec_to_eq :∀ a,b,q,r,q1,r1. +div_mod_spec a b q r → div_mod_spec a b q1 r1 → q = q1. +#a #b #q #r #q1 #r1 * #ltrb #spec * #ltr1b #spec1 +@(leb_elim q q1) #leqq1 + [(elim (le_to_or_lt_eq … leqq1)) // + #ltqq1 @False_ind @(absurd ?? (not_le_Sn_n a)) + @(lt_to_le_to_lt ? ((S q)*b) ?) + [>spec (applyS (monotonic_lt_plus_r … ltrb)) + |@(transitive_le ? (q1*b)) /2/ + ] + (* this case is symmetric *) + |@False_ind @(absurd ?? (not_le_Sn_n a)) + @(lt_to_le_to_lt ? ((S q1)*b) ?) + [>spec1 (applyS (monotonic_lt_plus_r … ltr1b)) + |cut (q1 < q) [/2/] #ltq1q @(transitive_le ? (q*b)) /2/ + ] + ] +qed. + +theorem div_mod_spec_to_eq2: ∀a,b,q,r,q1,r1. + div_mod_spec a b q r → div_mod_spec a b q1 r1 → r = r1. +#a #b #q #r #q1 #r1 #spec #spec1 +cut (q=q1) [@(div_mod_spec_to_eq … spec spec1)] +#eqq (elim spec) #_ #eqa (elim spec1) #_ #eqa1 +@(injective_plus_r (q*b)) // +qed. + +(* boh +theorem div_mod_spec_times : ∀ n,m:nat.div_mod_spec ((S n)*m) (S n) m O. +intros.constructor 1. +unfold lt.apply le_S_S.apply le_O_n. demodulate. reflexivity. +(*rewrite < plus_n_O.rewrite < sym_times.reflexivity.*) +qed. *) + +lemma div_plus_times: ∀m,q,r:nat. r < m → (q*m+r)/ m = q. +#m #q #r #ltrm +@(div_mod_spec_to_eq … (div_mod_spec_div_mod ???)) /2/ +qed. + +lemma mod_plus_times: ∀m,q,r:nat. r < m → (q*m+r) \mod m = r. +#m #q #r #ltrm +@(div_mod_spec_to_eq2 … (div_mod_spec_div_mod ???)) /2/ +qed. + +(* some properties of div and mod *) +theorem div_times: ∀a,b:nat. O < b → a*b/b = a. +#a #b #posb +@(div_mod_spec_to_eq (a*b) b … O (div_mod_spec_div_mod …)) +// @div_mod_spec_intro // qed. + +(* +theorem div_n_n: ∀n:nat. O < n → n / n = 1. +/2/ qed. + +theorem eq_div_O: ∀n,m. n < m → n / m = O. +#n #m #ltnm +@(div_mod_spec_to_eq n m (n/m) … n (div_mod_spec_div_mod …)) +/2/ qed. + +theorem mod_n_n: ∀n:nat. O < n → n \mod n = O. +#n #posn +@(div_mod_spec_to_eq2 n n … 1 0 (div_mod_spec_div_mod …)) +/2/ qed. *) + +theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m → +((S n) \mod m) = S (n \mod m). +#n #m #posm #H +@(div_mod_spec_to_eq2 (S n) m … (n / m) ? (div_mod_spec_div_mod …)) +// @div_mod_spec_intro// (applyS eq_f) // +qed. + +theorem mod_O_n: ∀n:nat.O \mod n = O. +/2/ qed. + +theorem lt_to_eq_mod: ∀n,m:nat. n < m → n \mod m = n. +#n #m #ltnm +@(div_mod_spec_to_eq2 n m (n/m) … O n (div_mod_spec_div_mod …)) +/2/ qed. + +(* +theorem mod_1: ∀n:nat. mod n 1 = O. +#n @sym_eq @le_n_O_to_eq +@le_S_S_to_le /2/ qed. + +theorem div_1: ∀n:nat. div n 1 = n. +#n @sym_eq napplyS (div_mod n 1) qed. *) + +theorem or_div_mod: ∀n,q. O < q → + ((S (n \mod q)=q) ∧ S n = (S (div n q)) * q ∨ + ((S (n \mod q) if m divides n q times, with remainder r *) +definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. *) + +(* inequalities *) + +theorem lt_div_S: ∀n,m. O < m → n < S(n / m)*m. +#n #m #posm (change with (n < m +(n/m)*m)) +>(div_mod n m) in ⊢ (? % ?) >(commutative_plus ? ?) +@monotonic_lt_plus_l @lt_mod_m_m // +qed. + +theorem le_div: ∀n,m. O < n → m/n ≤ m. +#n #m #posn +>(div_mod m n) in \vdash (? ? %) @(transitive_le ? (m/n*n)) /2/ +qed. + +theorem le_plus_mod: ∀m,n,q. O < q → +(m+n) \mod q ≤ m \mod q + n \mod q . +#m #n #q #posq +(elim (decidable_le q (m \mod q + n \mod q))) #Hle + [@(transitive_le … Hle) @le_S_S_to_le @le_S /2/ + |cut ((m+n)\mod q = m\mod q+n\mod q) // + @(div_mod_spec_to_eq2 … (m/q + n/q) ? (div_mod_spec_div_mod … posq)). + @div_mod_spec_intro + [@not_le_to_lt // + |>(div_mod n q) in ⊢ (? ? (? ? %) ?) + (applyS (eq_f … (λx.plus x (n \mod q)))) + >(div_mod m q) in ⊢ (? ? (? % ?) ?) + (applyS (eq_f … (λx.plus x (m \mod q)))) // + ] + ] +qed. + +theorem le_plus_div: ∀m,n,q. O < q → + m/q + n/q \le (m+n)/q. +#m #n #q #posq @(le_times_to_le … posq) +@(le_plus_to_le_r ((m+n) \mod q)) +(* bruttino *) +>(commutative_times …) in ⊢ (? ? %) <(div_mod …) +>(div_mod m q) in ⊢ (? ? (? % ?)) >(div_mod n q) in ⊢ (? ? (? ? %)) +>(commutative_plus …) in ⊢ (? ? (? % ?)) >(associative_plus …) in ⊢ (? ? %) +<(associative_plus …) in ⊢ (? ? (? ? %)) (applyS monotonic_le_plus_l) /2/ +qed. + +theorem le_times_to_le_div: ∀a,b,c:nat. + O < b → b*c ≤ a → c ≤ a/b. +#a #b #c #posb #Hle +@le_S_S_to_le @(lt_times_n_to_lt_l b) @(le_to_lt_to_lt ? a)/2/ +qed. + +theorem le_times_to_le_div2: ∀m,n,q. O < q → + n ≤ m*q → n/q ≤ m. +#m #n #q #posq #Hle +@(le_times_to_le q ? ? posq) @(le_plus_to_le (n \mod q)) /2/ +qed. + +(* da spostare +theorem lt_m_nm: ∀n,m. O < m → 1 < n → m < n*m. +/2/ qed. *) + +theorem lt_times_to_lt_div: ∀m,n,q. n < m*q → n/q < m. +#m #n #q #Hlt +@(lt_times_n_to_lt_l q …) @(lt_plus_to_lt_l (n \mod q)) /2/ +qed. + +(* +theorem lt_div: ∀n,m. O < m → 1 < n → m/n < m. +#n #m #posm #lt1n +@lt_times_to_lt_div (applyS lt_m_nm) //. +qed. + +theorem le_div_plus_S: ∀m,n,q. O < q → +(m+n)/q \le S(m/q + n/q). +#m #n #q #posq +@le_S_S_to_le @lt_times_to_lt_div +@(lt_to_le_to_lt … (lt_plus … (lt_div_S m … posq) (lt_div_S n … posq))) +// +qed. *) + +theorem le_div_S_S_div: ∀n,m. O < m → (S n)/m ≤ S (n /m). +#n #m #posm @le_times_to_le_div2 /2/ +qed. + +theorem le_times_div_div_times: ∀a,n,m.O < m → +a*(n/m) ≤ a*n/m. +#a #n #m #posm @le_times_to_le_div /2/ +qed. + +theorem monotonic_div: ∀n.O < n → + monotonic nat le (λm.div m n). +#n #posn #a #b #leab @le_times_to_le_div/2/ +qed. + +theorem pos_div: ∀n,m:nat. O < m → O < n → n \mod m = O → + O < n / m. +#n #m #posm #posn #mod0 +@(lt_times_n_to_lt_l m)// (* MITICO *) +qed. + +(* +theorem lt_div_n_m_n: ∀n,m:nat. 1 < m → O < n → n / m < n. +#n #m #ltm #posn +@(leb_elim 1 (n / m))/2/ (* MITICO *) +qed. *) + +theorem eq_div_div_div_times: ∀n,m,q. O < n → O < m → + q/n/m = q/(n*m). +#n #m #q #posn #posm +@(div_mod_spec_to_eq … (q\mod n+n*(q/n\mod m)) … (div_mod_spec_div_mod …)) /2/ +@div_mod_spec_intro // @(lt_to_le_to_lt ? (n*(S (q/n\mod m)))) + [(applyS monotonic_lt_plus_l) /2/ + |@monotonic_le_times_r/2/ + ] +qed. + +theorem eq_div_div_div_div: ∀n,m,q. O < n → O < m → +q/n/m = q/m/n. +#n #m #q #posn #posm +@(trans_eq ? ? (q/(n*m))) + [/2/ + |@sym_eq (applyS eq_div_div_div_times) // + ] +qed. + +(* +theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)). +intros. +rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?)) + [rewrite > eq_div_div_div_div + [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)). + apply div_mod. + apply lt_O_S + |apply lt_O_S + |assumption + ] + |apply lt_O_S + ] +qed. *) +(* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *) +(* The theorem is shown in two different parts: *) +(* +theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat. +O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)). +intros. +split +[ rewrite < H1. + rewrite > sym_times. + rewrite > eq_times_div_minus_mod + [ apply (le_minus_m a (a \mod b)) + | assumption + ] +| rewrite < (times_n_Sm b c). + rewrite < H1. + rewrite > sym_times. + rewrite > (div_mod a b) in \vdash (? % ?) + [ rewrite > (sym_plus b ((a/b)*b)). + apply lt_plus_r. + apply lt_mod_m_m. + assumption + | assumption + ] +] +qed. *) + +theorem le_plus_to_minus_r: ∀a,b,c. a + b \le c → a \le c -b. +#a #b #c #H @(le_plus_to_le_r … b) /2/ +qed. + +theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b. +#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/ +qed. + +theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b. +#a #b #c #H @not_le_to_lt +@(not_to_not … (lt_to_not_le …H)) /2/ +qed. + +theorem lt_minus_to_plus_r: ∀a,b,c. c ≤ a → + a < b + c → a - c < b. +#a #b #c #lea #H @not_le_to_lt +@(not_to_not … (lt_to_not_le …H)) /2/ +qed. + +theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:nat. +O < b → (b*c) ≤ a → a < (b*(S c)) → a/b = c. +#a #c #b #posb#lea #lta +@(div_mod_spec_to_eq … (a-b*c) (div_mod_spec_div_mod … posb …)) +@div_mod_spec_intro [@lt_minus_to_plus_r // |/2/] +qed. + +theorem div_times_times: ∀a,b,c:nat. O < c → O < b → + (a/b) = (a*c)/(b*c). +#a #b #c #posc #posb +>(commutative_times b c) <(eq_div_div_div_times … )// +>(div_times … posc)// +qed. + +theorem times_mod: ∀a,b,c:nat. +O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b). +#a #b #c #posc #posb +@(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b))) + [>(div_times_times … posc posb …) @div_mod_spec_div_mod /2/ + |@div_mod_spec_intro + [(applyS monotonic_lt_times_l) /2/ + |(applyS (eq_f …(λx.x*c))) // + ] + ] +qed. + +theorem le_div_times_m: ∀a,i,m. O < i → O < m → + (a * (m / i)) / m ≤ a / i. +#a #i #m #posi #posm +@(transitive_le ? ((a*m/i)/m)) + [@monotonic_div /2/ + |>(eq_div_div_div_div … posi posm) >(div_times …) // + ] +qed. + +(* serve ? +theorem le_div_times_Sm: ∀a,i,m. O < i → O < m → +a / i ≤ (a * S (m / i))/m. +intros. +apply (trans_le ? ((a * S (m/i))/((S (m/i))*i))) + [rewrite < (eq_div_div_div_times ? i) + [rewrite > lt_O_to_div_times + [apply le_n + |apply lt_O_S + ] + |apply lt_O_S + |assumption + ] + |apply le_times_to_le_div + [assumption + |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i))) + [apply le_times_div_div_times. + rewrite > (times_n_O O). + apply lt_times + [apply lt_O_S + |assumption + ] + |rewrite > sym_times. + apply le_times_to_le_div2 + [rewrite > (times_n_O O). + apply lt_times + [apply lt_O_S + |assumption + ] + |apply le_times_r. + apply lt_to_le. + apply lt_div_S. + assumption + ] + ] + ] + ] +qed. *) diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma new file mode 100644 index 000000000..19ea14440 --- /dev/null +++ b/matita/matita/lib/arithmetics/minimization.ma @@ -0,0 +1,304 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "arithmetics/nat.ma". + +(* maximization *) + +let rec max' i f d ≝ + match i with + [ O ⇒ d + | S j ⇒ + match (f j) with + [ true ⇒ j + | false ⇒ max' j f d]]. + +definition max ≝ λn.λf.max' n f O. + +theorem max_O: ∀f. max O f = O. +// qed. + +theorem max_cases: ∀f.∀n. + (f n = true ∧ max (S n) f = n) ∨ + (f n = false ∧ max (S n) f = max n f). +#f #n normalize cases (f n) normalize /3/ qed. + +theorem le_max_n: ∀f.∀n. max n f ≤ n. +#f #n (elim n) // #m #Hind +normalize (cases (f m)) normalize @le_S // +(* non trova Hind *) +@Hind +qed. + +theorem lt_max_n : ∀f.∀n. O < n → max n f < n. +#f #n #posn @(lt_O_n_elim ? posn) #m +normalize (cases (f m)) normalize apply le_S_S // +@le_max_n qed. + +theorem le_to_le_max : ∀f.∀n,m. +n ≤ m → max n f ≤ max m f. +#f #n #m #H (elim H) // +#i #leni #Hind @(transitive_le … Hind) +(cases (max_cases f i)) * #_ /2/ +qed. + +theorem true_to_le_max: ∀f.∀n,m. + m < n → f m = true → m ≤ max n f. +#f #n (elim n) + [#m #ltmO @False_ind /2/ + |#i #Hind #m #ltm + (cases (le_to_or_lt_eq … (le_S_S_to_le … ltm))) + [#ltm #fm @(transitive_le ? (max i f)) + [@Hind /2/ | @le_to_le_max //] + |#eqm >eqm #eqf normalize >eqf // + ] +qed. + +theorem lt_max_to_false: ∀f.∀n,m. + m < n → max n f < m → f m = false. +#f #n #m #ltnm #eqf cases(true_or_false (f m)) // +#fm @False_ind @(absurd … eqf) @(le_to_not_lt) @true_to_le_max // +qed. + +lemma max_exists: ∀f.∀n,m.m < n → f m =true → + (∀i. m < i → i < n → f i = false) → max n f = m. +#f #n (elim n) #m + [#ltO @False_ind /2/ + |#Hind #max #ltmax #fmax #ismax + cases (le_to_or_lt_eq …(le_S_S_to_le …(ltmax …))) + #ltm normalize + [>(ismax m …) // normalize @(Hind max ltm fmax) + #i #Hl #Hr @ismax // @le_S // + |fmax // + ] + ] +qed. + +lemma max_not_exists: ∀f.∀n. + (∀i. i < n → f i = false) → max n f = O. +#f #n #ffalse @(le_gen ? n) #i (elim i) // #j #Hind #ltj +normalize >(ffalse j …) // @Hind /2/ +qed. + +lemma fmax_false: ∀f.∀n,m.max n f = m → f m = false → m = O. +#f #n #m (elim n) // +#i #Hind normalize cases(true_or_false … (f i)) #fi >fi +normalize + [#eqm #fm @False_ind @(absurd … fi) // |@Hind] +qed. + +inductive max_spec (n:nat) (f:nat→bool) : nat→Prop ≝ + | found : ∀m:nat.m < n → f m =true → + (∀i. m < i → i < n → f i = false) → max_spec n f m + | not_found: (∀i.i < n → f i = false) → max_spec n f O. + +theorem max_spec_to_max: ∀f.∀n,m. + max_spec n f m → max n f = m. +#f #n #m #spec (cases spec) + [#max #ltmax #fmax #ismax @max_exists // @ismax + |#ffalse @max_not_exists @ffalse + ] +qed. + +theorem max_to_max_spec: ∀f.∀n,m. + max n f = m → max_spec n f m. +#f #n #m (cases n) + [#eqm eqmO + %2 #i (cases i) // #j #ltj @(lt_max_to_false … ltj) // +qed. + +theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) → + max n f = max n g. +#f #g #n (elim n) // +#m #Hind #ext normalize >(ext … (le_n …)) >(Hind …) // +#i #ltim @ext /2/ +qed. + +theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) → +max n f ≤ max n g. +#f #g #n (elim n) // +#m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq + [>(ext m …) // + |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/ +qed. + +theorem f_max_true : ∀ f.∀n. +(∃i:nat. i < n ∧ f i = true) → f (max n f) = true. +#f #n cases(max_to_max_spec f n (max n f) (refl …)) // +#Hall * #x * #ltx #fx @False_ind @(absurd … fx) >(Hall x ?) /2/ +qed. + +(* minimization *) + +(* min k b f is the minimun i, b ≤ i < b + k s.t. f i; + returns b + k otherwise *) + +let rec min k b f ≝ + match k with + [ O ⇒ b + | S p ⇒ + match f b with + [ true ⇒ b + | false ⇒ min p (S b) f]]. + +definition min0 ≝ λn.λf. min n 0 f. + +theorem min_O_f : ∀f.∀b. min O b f = b. +// qed. + +theorem true_min: ∀f.∀b. + f b = true → ∀n.min n b f = b. +#f #b #fb #n (cases n) // #n normalize >fb normalize // +qed. + +theorem false_min: ∀f.∀n,b. + f b = false → min (S n) b f = min n (S b) f. +#f #n #b #fb normalize >fb normalize // +qed. + +(* +theorem leb_to_le_min : ∀f.∀n,b1,b2. +b1 ≤ b2 → min n b1 f ≤ min n b2 f. +#f #n #b1 #b2 #leb (elim n) // +#m #Hind normalize (cases (f m)) normalize *) + +theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b. +#f #n normalize (elim n) // #m #Hind #b +normalize (cases (f b)) normalize // +qed. + +theorem le_min_l: ∀f.∀n,b. b ≤ min n b f. +#f #n normalize (elim n) // #m #Hind #b +normalize (cases (f b)) normalize /2/ +qed. + +theorem le_to_le_min : ∀f.∀n,m. +n ≤ m → ∀b.min n b f ≤ min m b f. +#f @nat_elim2 // + [#n #leSO @False_ind /2/ + |#n #m #Hind #leSS #b + (cases (true_or_false (f b))) #fb + [lapply (true_min …fb) // + |>(false_min f n b fb) >(false_min f m b fb) @Hind /2/ + ] + ] +qed. + +theorem true_to_le_min: ∀f.∀n,m,b. + b ≤ m → f m = true → min n b f ≤ m. +#f #n (elim n) // +#i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb)) + [#ltm #fm normalize (cases (f b)) normalize // @Hind // + |#eqm eqb normalize // + ] +qed. + +theorem lt_min_to_false: ∀f.∀n,m,b. + b ≤ m → m < min n b f → f m = false. +#f #n #m #b #lebm #ltm cases(true_or_false (f m)) // +#fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min // +qed. + +theorem fmin_true: ∀f.∀n,m,b. + m = min n b f → m < n + b → f m = true. +#f #n (elim n) + [#m #b normalize #eqmb >eqmb #leSb @(False_ind) + @(absurd … leSb) // + |#n #Hind #m #b (cases (true_or_false (f b))) #caseb + [>(true_min f b caseb (S n)) // + |>(false_min … caseb) #eqm #ltm @(Hind m (S b)) /2/ + ] + ] +qed. + +lemma min_exists: ∀f.∀t,m. m < t → f m = true → +∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b → + min k b f = m. +#f #t #m #ltmt #fm #k (elim k) + [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) (false_min …) /2/ @Hind // + [#i #H #H1 @ismin /2/ | >eqt normalize //] + |#eqbm >(true_min …) // + ] + ] +qed. + +lemma min_not_exists: ∀f.∀n,b. + (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b. +#f #n (elim n) // +#p #Hind #b #ffalse >(false_min …) + [>(Hind …) // #i #H #H1 @ffalse /2/ + |@ffalse // + ] +qed. + +lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in + f m = false → m = n+b. +#f #n (elim n) // +#i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb +normalize + [#eqm @False_ind @(absurd … fb) // + |>(plus_n_Sm …) @Hind] +qed. + +inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝ + | found : ∀m:nat. b ≤ m → m < n + b → f m =true → + (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m + | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b). + +theorem min_spec_to_min: ∀f.∀n,b,m. + min_spec n b f m → min n b f = m. +#f #n #b #m #spec (cases spec) + [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin + |#ffalse @min_not_exists @ffalse + ] +qed. + +theorem min_to_min_spec: ∀f.∀n,b,m. + min n b f = m → min_spec n b f m. +#f #n #b #m (cases n) + [#eqm eqm #lem + (cases (le_to_or_lt_eq … lem)) #mcase + [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) // + |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) // + ] + ] +qed. + +theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) → + min n b f = min n b g. +#f #g #n (elim n) // +#m #Hind #b #ext normalize >(ext b (le_n b) ?) // >(Hind …) // +#i #ltib #ltim @ext /2/ +qed. + +theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) → +min n b g ≤ min n b f. +#f #g #n (elim n) // +#m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq + [>(ext b …) // + |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi + @ext /2/ +qed. + +theorem f_min_true : ∀ f.∀n,b. +(∃i:nat. b ≤ i ∧ i < n ∧ f i = true) → f (min n b f) = true. +#f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) // +#Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >(Hall x ??) /2/ +qed. diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma new file mode 100644 index 000000000..dc0af3a6b --- /dev/null +++ b/matita/matita/lib/arithmetics/nat.ma @@ -0,0 +1,1079 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "basics/relations.ma". + +inductive nat : Type[0] ≝ + | O : nat + | S : nat → nat. + +interpretation "Natural numbers" 'N = nat. + +alias num (instance 0) = "natural number". + +definition pred ≝ + λn. match n with [ O ⇒ O | S p ⇒ p]. + +theorem pred_Sn : ∀n. n = pred (S n). +// qed. + +theorem injective_S : injective nat nat S. +// qed. + +(* +theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m. +//. qed. *) + +theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m. +/2/ qed. + +definition not_zero: nat → Prop ≝ + λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ]. + +theorem not_eq_O_S : ∀n:nat. O ≠ S n. +#n @nmk #eqOS (change with (not_zero O)) >eqOS // qed. + +theorem not_eq_n_Sn: ∀n:nat. n ≠ S n. +#n (elim n) /2/ qed. + +theorem nat_case: + ∀n:nat.∀P:nat → Prop. + (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n. +#n #P (elim n) /2/ qed. + +theorem nat_elim2 : + ∀R:nat → nat → Prop. + (∀n:nat. R O n) + → (∀n:nat. R (S n) O) + → (∀n,m:nat. R n m → R (S n) (S m)) + → ∀n,m:nat. R n m. +#R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed. + +theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m). +@nat_elim2 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/] +qed. + +(*************************** plus ******************************) + +let rec plus n m ≝ + match n with [ O ⇒ m | S p ⇒ S (plus p m) ]. + +interpretation "natural plus" 'plus x y = (plus x y). + +theorem plus_O_n: ∀n:nat. n = O+n. +// qed. + +(* +theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m. +// qed. +*) + +theorem plus_n_O: ∀n:nat. n = n+O. +#n (elim n) normalize // qed. + +theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m. +#n (elim n) normalize // qed. + +(* +theorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m. +#n (elim n) normalize // qed. +*) + +(* deleterio? +theorem plus_n_1 : ∀n:nat. S n = n+1. +// qed. +*) + +theorem commutative_plus: commutative ? plus. +#n (elim n) normalize // qed. + +theorem associative_plus : associative nat plus. +#n (elim n) normalize // qed. + +theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a. +// qed. + +theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m). +#n (elim n) normalize /3/ qed. + +(* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m +\def injective_plus_r. + +theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m). +/2/ qed. *) + +(* theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m +\def injective_plus_l. *) + +(*************************** times *****************************) + +let rec times n m ≝ + match n with [ O ⇒ O | S p ⇒ m+(times p m) ]. + +interpretation "natural times" 'times x y = (times x y). + +theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m. +// qed. + +theorem times_O_n: ∀n:nat. O = O*n. +// qed. + +theorem times_n_O: ∀n:nat. O = n*O. +#n (elim n) // qed. + +theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m). +#n (elim n) normalize // qed. + +theorem commutative_times : commutative nat times. +#n (elim n) normalize // qed. + +(* variant sym_times : \forall n,m:nat. n*m = m*n \def +symmetric_times. *) + +theorem distributive_times_plus : distributive nat times plus. +#n (elim n) normalize // qed. + +theorem distributive_times_plus_r : + ∀a,b,c:nat. (b+c)*a = b*a + c*a. +// qed. + +theorem associative_times: associative nat times. +#n (elim n) normalize // qed. + +lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z). +// qed. + +(* ci servono questi risultati? +theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O. +napply nat_elim2 /2/ +#n #m #H normalize #H1 napply False_ind napply not_eq_O_S +// qed. + +theorem times_n_SO : ∀n:nat. n = n * S O. +#n // qed. + +theorem times_SSO_n : ∀n:nat. n + n = (S(S O)) * n. +normalize // qed. + +nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)). +// qed. + +theorem or_eq_eq_S: \forall n.\exists m. +n = (S(S O))*m \lor n = S ((S(S O))*m). +#n (elim n) + ##[@ /2/ + ##|#a #H nelim H #b#ornelim or#aeq + ##[@ b @ 2 // + ##|@ (S b) @ 1 /2/ + ##] +qed. +*) + +(******************** ordering relations ************************) + +inductive le (n:nat) : nat → Prop ≝ + | le_n : le n n + | le_S : ∀ m:nat. le n m → le n (S m). + +interpretation "natural 'less or equal to'" 'leq x y = (le x y). + +interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)). + +definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m. + +interpretation "natural 'less than'" 'lt x y = (lt x y). +interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)). + +(* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m). +// qed. *) + +definition ge: nat → nat → Prop ≝ λn,m.m ≤ n. + +interpretation "natural 'greater or equal to'" 'geq x y = (ge x y). + +definition gt: nat → nat → Prop ≝ λn,m.m (S_pred m) + [ apply le_S_S + assumption + | assumption + ] +]. +qed. + +*) + +(* le to lt or eq *) +theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m. +#n #m #lenm (elim lenm) /3/ qed. + +(* not eq *) +theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m. +#n #m #H @not_to_not /2/ qed. + +(*not lt +theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b. +intros. +unfold Not. +intros. +rewrite > H in H1. +apply (lt_to_not_eq b b) +[ assumption +| reflexivity +] +qed. + +theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n. +intros +unfold Not +intro +unfold lt in H +unfold lt in H1 +generalize in match (le_S_S ? ? H) +intro +generalize in match (transitive_le ? ? ? H2 H1) +intro +apply (not_le_Sn_n ? H3). +qed. *) + +theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n H7. +apply H. +apply le_to_or_lt_eq.apply H6. +qed. +*) + +(*********************** monotonicity ***************************) +theorem monotonic_le_plus_r: +∀n:nat.monotonic nat le (λm.n + m). +#n #a #b (elim n) normalize // +#m #H #leab @le_S_S /2/ qed. + +(* +theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m +≝ monotonic_le_plus_r. *) + +theorem monotonic_le_plus_l: +∀m:nat.monotonic nat le (λn.n + m). +/2/ qed. + +(* +theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p +\def monotonic_le_plus_l. *) + +theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2 +→ n1 + m1 ≤ n2 + m2. +#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2)) +/2/ qed. + +theorem le_plus_n :∀n,m:nat. m ≤ n + m. +/2/ qed. + +lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m. +/2/ qed. + +lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m. +/2/ qed. + +theorem le_plus_n_r :∀n,m:nat. m ≤ m + n. +/2/ qed. + +theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n. +// qed. + +theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m. +#a (elim a) normalize /3/ qed. + +theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m. +/2/ qed. + +(* plus & lt *) + +theorem monotonic_lt_plus_r: +∀n:nat.monotonic nat lt (λm.n+m). +/2/ qed. + +(* +variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def +monotonic_lt_plus_r. *) + +theorem monotonic_lt_plus_l: +∀n:nat.monotonic nat lt (λm.m+n). +/2/ qed. + +(* +variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def +monotonic_lt_plus_l. *) + +theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q. +#n #m #p #q #ltnm #ltpq +@(transitive_lt ? (n+q))/2/ qed. + +theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p H2 in H1. + rewrite > (S_pred a) in H1 + [ apply False_ind. + apply (eq_to_not_lt O ((S (pred a))*(S m))) + [ apply sym_eq. + assumption + | apply lt_O_times_S_S + ] + | assumption + ] +] +qed. + +theorem O_lt_times_to_O_lt: \forall a,c:nat. +O \lt (a * c) \to O \lt a. +intros. +apply (nat_case1 a) +[ intros. + rewrite > H1 in H. + simplify in H. + assumption +| intros. + apply lt_O_S +] +qed. + +lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m. +intros. +elim (le_to_or_lt_eq O ? (le_O_n m)) + [assumption + |apply False_ind. + rewrite < H1 in H. + rewrite < times_n_O in H. + apply (not_le_Sn_O ? H) + ] +qed. *) + +(* +theorem monotonic_lt_times_r: +∀n:nat.monotonic nat lt (λm.(S n)*m). +/2/ +simplify. +intros.elim n. +simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption. +apply lt_plus.assumption.assumption. +qed. *) + +theorem monotonic_lt_times_l: + ∀c:nat. O < c → monotonic nat lt (λt.(t*c)). +#c #posc #n #m #ltnm +(elim ltnm) normalize + [/2/ + |#a #_ #lt1 @(transitive_le … lt1) // + ] +qed. + +theorem monotonic_lt_times_r: + ∀c:nat. O < c → monotonic nat lt (λt.(c*t)). +/2/ qed. + +theorem lt_to_le_to_lt_times: +∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q. +#n #m #p #q #ltnm #lepq #posq +@(le_to_lt_to_lt ? (n*q)) + [@monotonic_le_times_r // + |@monotonic_lt_times_l // + ] +qed. + +theorem lt_times:∀n,m,p,q:nat. n nat_compare_n_n.reflexivity. +intro.apply nat_compare_elim.intro. +absurd (p minus_Sn_m. +apply le_S.assumption. +apply lt_to_le.assumption. +qed. + +theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)). +intros. +apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))). +intro.elim n1.simplify.apply le_n_Sn. +simplify.rewrite < minus_n_O.apply le_n. +intros.simplify.apply le_n_Sn. +intros.simplify.apply H. +qed. + +theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. +intros 3.intro. +(* autobatch *) +(* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *) +apply (trans_le (m-n) (S (m-(S n))) p). +apply minus_le_S_minus_S. +assumption. +qed. + +theorem le_minus_m: \forall n,m:nat. n-m \leq n. +intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)). +intros.rewrite < minus_n_O.apply le_n. +intros.simplify.apply le_n. +intros.simplify.apply le_S.assumption. +qed. + +theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n. +intros.apply (lt_O_n_elim n H).intro. +apply (lt_O_n_elim m H1).intro. +simplify.unfold lt.apply le_S_S.apply le_minus_m. +qed. + +theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m. +intros 2. +apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)). +intros.apply le_O_n. +simplify.intros. assumption. +simplify.intros.apply le_S_S.apply H.assumption. +qed. +*) + +(* monotonicity and galois *) + +theorem monotonic_le_minus_l: +∀p,q,n:nat. q ≤ p → q-n ≤ p-n. +@nat_elim2 #p #q + [#lePO @(le_n_O_elim ? lePO) // + |// + |#Hind #n (cases n) // #a #leSS @Hind /2/ + ] +qed. + +theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m. +#n #m #p #lep @transitive_le + [|@le_plus_minus_m_m | @monotonic_le_plus_l // ] +qed. + +theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p. +#n #m #p #lep /2/ qed. + +theorem monotonic_le_minus_r: +∀p,q,n:nat. q ≤ p → n-p ≤ n-q. +#p #q #n #lepq @le_plus_to_minus +@(transitive_le … (le_plus_minus_m_m ? q)) /2/ +qed. + +theorem eq_minus_O: ∀n,m:nat. + n ≤ m → n-m = O. +#n #m #lenm @(le_n_O_elim (n-m)) /2/ +qed. + +theorem distributive_times_minus: distributive ? times minus. +#a #b #c +(cases (decidable_lt b c)) #Hbc + [>(eq_minus_O …) /2/ >(eq_minus_O …) // + @monotonic_le_times_r /2/ + |@sym_eq (applyS plus_to_minus) <(distributive_times_plus …) + (* STRANO *) + @(eq_f …b) (applyS plus_minus_m_m) /2/ +qed. + +(*********************** boolean arithmetics ********************) +include "basics/bool.ma". + +let rec eqb n m ≝ +match n with + [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] + | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q] + ]. + +theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop. +(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). +@nat_elim2 + [#n (cases n) normalize /3/ + |normalize /3/ + |normalize /4/ + ] +qed. + +theorem eqb_n_n: ∀n. eqb n n = true. +#n (elim n) normalize // qed. + +theorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m. +#n #m @(eqb_elim n m) // #_ #abs @False_ind /2/ qed. + +theorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m. +#n #m @(eqb_elim n m) /2/ qed. + +theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true. +// qed. + +theorem not_eq_to_eqb_false: ∀n,m:nat. + n ≠ m → eqb n m = false. +#n #m #noteq @eqb_elim// #Heq @False_ind /2/ qed. + +let rec leb n m ≝ +match n with + [ O ⇒ true + | (S p) ⇒ + match m with + [ O ⇒ false + | (S q) ⇒ leb p q]]. + +theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop. +(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m). +@nat_elim2 normalize + [/2/ + |/3/ + |#n #m #Hind #P #Pt #Pf @Hind + [#lenm @Pt @le_S_S // |#nlenm @Pf /2/ ] + ] +qed. + +theorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m. +#n #m @leb_elim // #_ #abs @False_ind /2/ qed. + +theorem leb_false_to_not_le:∀n,m. + leb n m = false → n ≰ m. +#n #m @leb_elim // #_ #abs @False_ind /2/ qed. + +theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true. +#n #m @leb_elim // #H #H1 @False_ind /2/ qed. + +theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false. +#n #m @leb_elim // #H #H1 @False_ind /2/ qed. + +theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false. +/3/ qed. + +(* serve anche ltb? +ndefinition ltb ≝λn,m. leb (S n) m. + +theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop. +(n < m → P true) → (n ≮ m → P false) → P (ltb n m). +#n #m #P #Hlt #Hnlt +napply leb_elim /3/ qed. + +theorem ltb_true_to_lt:∀n,m.ltb n m = true → n < m. +#n #m #Hltb napply leb_true_to_le nassumption +qed. + +theorem ltb_false_to_not_lt:∀n,m. + ltb n m = false → n ≮ m. +#n #m #Hltb napply leb_false_to_not_le nassumption +qed. + +theorem lt_to_ltb_true: ∀n,m. n < m → ltb n m = true. +#n #m #Hltb napply le_to_leb_true nassumption +qed. + +theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false. +#n #m #Hltb napply lt_to_leb_false /2/ +qed. *) + +(* min e max *) +definition min: nat →nat →nat ≝ +λn.λm. if_then_else ? (leb n m) n m. + +definition max: nat →nat →nat ≝ +λn.λm. if_then_else ? (leb n m) m n. + +lemma commutative_min: commutative ? min. +#n #m normalize @leb_elim + [@leb_elim normalize /2/ + |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/ + ] qed. + +lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m. +#i #n #m normalize @leb_elim normalize /2/ qed. + +lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n. +/2/ qed. + +lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m. +#i #n #m #lein #leim normalize (cases (leb n m)) +normalize // qed. + +lemma commutative_max: commutative ? max. +#n #m normalize @leb_elim + [@leb_elim normalize /2/ + |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/ + ] qed. + +lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i. +#i #n #m normalize @leb_elim normalize /2/ qed. + +lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i. +/2/ qed. + +lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i. +#i #n #m #leni #lemi normalize (cases (leb n m)) +normalize // qed. + -- 2.39.2