From 8f08fac33a366b2267b35af1a50ad3a9df8dbb88 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 16 Jun 2011 13:53:23 +0000 Subject: [PATCH] Added repository for the shared library to be used by matitaweb. --- weblib/arithmetics/bigops.ma | 1023 ++++++++++++++++++++++ weblib/arithmetics/binomial.ma | 133 +++ weblib/arithmetics/chinese_reminder.ma | 132 +++ weblib/arithmetics/congruence.ma | 118 +++ weblib/arithmetics/div_and_mod.ma | 442 ++++++++++ weblib/arithmetics/exp.ma | 139 +++ weblib/arithmetics/factorial.ma | 196 +++++ weblib/arithmetics/gcd.ma | 406 +++++++++ weblib/arithmetics/log.ma | 474 ++++++++++ weblib/arithmetics/minimization.ma | 304 +++++++ weblib/arithmetics/nat.ma | 1119 ++++++++++++++++++++++++ weblib/arithmetics/nth_prime.ma | 201 +++++ weblib/arithmetics/primes.ma | 530 +++++++++++ weblib/arithmetics/sigma_pi.ma | 747 ++++++++++++++++ weblib/basics/bool.ma | 76 ++ weblib/basics/core_notation.ma | 287 ++++++ weblib/basics/jmeq.ma | 92 ++ weblib/basics/list.ma | 185 ++++ weblib/basics/list2.ma | 30 + weblib/basics/logic.ma | 226 +++++ weblib/basics/pts.ma | 41 + weblib/basics/relations.ma | 106 +++ weblib/basics/types.ma | 59 ++ weblib/hints_declaration.ma | 107 +++ weblib/lambda/subst.ma | 230 +++++ weblib/lambda/types.ma | 214 +++++ weblib/root | 1 + 27 files changed, 7618 insertions(+) create mode 100644 weblib/arithmetics/bigops.ma create mode 100644 weblib/arithmetics/binomial.ma create mode 100644 weblib/arithmetics/chinese_reminder.ma create mode 100644 weblib/arithmetics/congruence.ma create mode 100644 weblib/arithmetics/div_and_mod.ma create mode 100644 weblib/arithmetics/exp.ma create mode 100644 weblib/arithmetics/factorial.ma create mode 100644 weblib/arithmetics/gcd.ma create mode 100644 weblib/arithmetics/log.ma create mode 100644 weblib/arithmetics/minimization.ma create mode 100644 weblib/arithmetics/nat.ma create mode 100644 weblib/arithmetics/nth_prime.ma create mode 100644 weblib/arithmetics/primes.ma create mode 100644 weblib/arithmetics/sigma_pi.ma create mode 100644 weblib/basics/bool.ma create mode 100644 weblib/basics/core_notation.ma create mode 100644 weblib/basics/jmeq.ma create mode 100644 weblib/basics/list.ma create mode 100644 weblib/basics/list2.ma create mode 100644 weblib/basics/logic.ma create mode 100644 weblib/basics/pts.ma create mode 100644 weblib/basics/relations.ma create mode 100644 weblib/basics/types.ma create mode 100644 weblib/hints_declaration.ma create mode 100644 weblib/lambda/subst.ma create mode 100644 weblib/lambda/types.ma create mode 100644 weblib/root diff --git a/weblib/arithmetics/bigops.ma b/weblib/arithmetics/bigops.ma new file mode 100644 index 000000000..03db53f7d --- /dev/null +++ b/weblib/arithmetics/bigops.ma @@ -0,0 +1,1023 @@ +(* + ||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/types.ma". +include "arithmetics/div_and_mod.ma". + +definition sameF_upto: nat → ∀A.relation(nat→A) ≝ +λk.λA.λf,g.∀i. i < k → f i = g i. + +definition sameF_p: nat → (nat → bool) →∀A.relation(nat→A) ≝ +λk,p,A,f,g.∀i. i < k → p i = true → f i = g i. + +lemma sameF_upto_le: ∀A,f,g,n,m. + n ≤m → sameF_upto m A f g → sameF_upto n A f g. +#A #f #g #n #m #lenm #samef #i #ltin @samef /2/ +qed. + +lemma sameF_p_le: ∀A,p,f,g,n,m. + n ≤m → sameF_p m p A f g → sameF_p n p A f g. +#A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /2/ +qed. + +(* +definition sumF ≝ λA.λf,g:nat → A.λn,i. +if_then_else ? (leb n i) (g (i-n)) (f i). + +lemma sumF_unfold: ∀A,f,g,n,i. +sumF A f g n i = if_then_else ? (leb n i) (g (i-n)) (f i). +// qed. *) + +definition prodF ≝ + λA,B.λf:nat→A.λg:nat→B.λm,x.〈 f(div x m), g(mod x m) 〉. + +(* bigop *) +let rec bigop (n:nat) (p:nat → bool) (B:Type[0]) + (nil: B) (op: B → B → B) (f: nat → B) ≝ + match n with + [ O ⇒ nil + | S k ⇒ + match p k with + [true ⇒ op (f k) (bigop k p B nil op f) + |false ⇒ bigop k p B nil op f] + ]. + +notation "\big [ op , nil ]_{ ident i < n | p } f" + with precedence 80 +for @{'bigop $n $op $nil (λ${ident i}. $p) (λ${ident i}. $f)}. + +notation "\big [ op , nil ]_{ ident i < n } f" + with precedence 80 +for @{'bigop $n $op $nil (λ${ident i}.true) (λ${ident i}. $f)}. + +interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f). + +notation "\big [ op , nil ]_{ ident j ∈ [a,b[ | p } f" + with precedence 80 +for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +notation "\big [ op , nil ]_{ ident j ∈ [a,b[ } f" + with precedence 80 +for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +(* notation "\big [ op , nil ]_{( term 50) a ≤ ident j < b | p } f" + with precedence 80 +for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}. +*) + +interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f). + +lemma bigop_Strue: ∀k,p,B,nil,op.∀f:nat→B. p k = true → + \big[op,nil]_{i < S k | p i}(f i) = + op (f k) (\big[op,nil]_{i < k | p i}(f i)). +#k #p #B #nil #op #f #H normalize >H // qed. + +lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:nat→B. p k = false → + \big[op,nil]_{ i < S k | p i}(f i) = + \big[op,nil]_{i < k | p i}(f i). +#k #p #B #nil #op #f #H normalize >H // qed. + +lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:nat→B. + sameF_upto k bool p1 p2 → sameF_p k p1 B f g → + \big[op,nil]_{i < k | p1 i}(f i) = + \big[op,nil]_{i < k | p2 i}(g i). +#k #p1 #p2 #B #nil #op #f #g (elim k) // +#n #Hind #samep #samef normalize >Hind /2/ +<(samep … (le_n …)) cases(true_or_false (p1 n)) #H1 >H1 +normalize // <(samef … (le_n …) H1) // +qed. + +theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k → +\big[op,nil]_{i < n | p i}(f i) + = \big[op,nil]_{i < k | if_then_else ? (leb n i) false (p i)}(f i). +#k #n #p #B #nil #op #f #lenk (elim lenk) + [@same_bigop #i #lti // >(not_le_to_leb_false …) /2/ + |#j #leup #Hind >bigop_Sfalse >(le_to_leb_true … leup) // + ] qed. + +record Aop (A:Type[0]) (nil:A) : Type[0] ≝ + {op :2> A → A → A; + nill:∀a. op nil a = a; + nilr:∀a. op a nil = a; + assoc: ∀a,b,c.op a (op b c) = op (op a b) c + }. + +theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f,g:nat→B. +op (\big[op,nil]_{inill @same_bigop #i #lti + >(lt_to_leb_false … lti) normalize /2/ + |#i #Hind normalize (le_to_leb_true … (le_plus_n …)) normalize (commutative_plus c) +>associative_plus (plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?) /2/ +>minus_plus >(commutative_plus a) bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b)) + [#i #lei >plus_minus // (bigop_sumI a (S a) (S b)) [|@le_S_S //|//] @eq_f2 + [@same_bigop // |bigop_a [|//] @eq_f2 [|//] bigop_Strue // >Hind >bigop_sum @same_bigop + #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/ + #eqi [|#H] (>eqi in ⊢ (???%)) + >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ + |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop + #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/ + #eqi >eqi in ⊢ (???%) >div_plus_times /2/ + ] +qed. + +record ACop (A:Type[0]) (nil:A) : Type[0] ≝ + {aop :> Aop A nil; + comm: ∀a,b.aop a b = aop b a + }. + +lemma bigop_op: ∀k,p,B.∀nil.∀op:ACop B nil.∀f,g: nat → B. +op (\big[op,nil]_{ibigop_Strue // >bigop_Strue // >bigop_Strue // + assoc >comm in ⊢ (??(????%?)?) + bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse // + ] +qed. + +lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n. + i < n → p i = true → + \big[op,nil]_{x(not_eq_to_eqb_false … (lt_to_not_eq … Hi)) //] #Hcut + cases (true_or_false (p n)) #pn + [>bigop_Strue // >bigop_Strue // + >assoc >(comm ?? op (f i) (f n)) Hind // + |>bigop_Sfalse // >bigop_Sfalse // >Hind // + ] + |bigop_Strue // @eq_f >bigop_Sfalse + [@same_bigop // #k #ltki >not_eq_to_eqb_false /2/ + |>eq_to_eqb_true // + ] + ] + ] +qed. + +(* range *) +record range (A:Type[0]): Type[0] ≝ + {enum:nat→A; upto:nat; filter:nat→bool}. + +definition sub_hk: (nat→nat)→(nat→nat)→∀A:Type[0].relation (range A) ≝ +λh,k,A,I,J.∀i.i<(upto A I) → (filter A I i)=true → + (h i < upto A J + ∧ filter A J (h i) = true + ∧ k (h i) = i). + +definition iso: ∀A:Type[0].relation (range A) ≝ + λA,I,J.∃h,k. + (∀i. i < (upto A I) → (filter A I i) = true → + enum A I i = enum A J (h i)) ∧ + sub_hk h k A I J ∧ sub_hk k h A J I. + +lemma sub_hkO: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A I J. +#h #k #A #I #J #up0 #i #lti >up0 @False_ind /2/ +qed. + +lemma sub0_to_false: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A J I → + ∀i. i < upto A J → filter A J i = false. +#h #k #A #I #J #up0 #sub #i #lti cases(true_or_false (filter A J i)) // +#ptrue (cases (sub i lti ptrue)) * #hi @False_ind /2/ +qed. + +lemma sub_lt: ∀A,e,p,n,m. n ≤ m → + sub_hk (λx.x) (λx.x) A (mk_range A e n p) (mk_range A e m p). +#A #e #f #n #m #lenm #i #lti #fi % // % /2/ +qed. + +theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K. + sub_hk h1 k1 A I J → sub_hk h2 k2 A J K → + sub_hk (λx.h2(h1 x)) (λx.k1(k2 x)) A I K. +#h1 #k1 #h2 #k2 #A #I #J #K #sub1 #sub2 #i #lti #fi +cases(sub1 i lti fi) * #lth1i #fh1i #ei +cases(sub2 (h1 i) lth1i fh1i) * #H1 #H2 #H3 % // % // +qed. + +theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2. + iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) → + \big[op,nil]_{ibigop_Sfalse + [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //] + |@(sub0_to_false … sub2) // + ] + |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n ≤n1)) [/2/] #len + cases(true_or_false (p1 n)) #p1n + [>bigop_Strue // (cases (sub1 n (le_n …) p1n)) * #hn #p2hn #eqn + >(bigop_diff … (h n) n2) // >same // + @eq_f @(Hind ? len) + [#i #ltin #p1i (cases (sub1 i (le_S … ltin) p1i)) * + #h1i #p2h1i #eqi % // % // >not_eq_to_eqb_false normalize // + @(not_to_not ??? (lt_to_not_eq ? ? ltin)) // + |#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) * + #ltkj #p1kj #eqj % // % // + (cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) // + #eqkj @False_ind generalize in match p2j @eqb_elim + normalize /2/ + ] + |>bigop_Sfalse // @(Hind ? len) + [@(transitive_sub … (sub_lt …) sub1) // + |#i #lti #p2i cases(sub2 i lti p2i) * #ltki #p1ki #eqi + % // % // cases(le_to_or_lt_eq …(le_S_S_to_le …ltki)) // + #eqki @False_ind /2/ + ] + ] + ] +qed. + +(* distributivity *) + +record Dop (A:Type[0]) (nil:A): Type[0] ≝ + {sum : ACop A nil; + prod: A → A →A; + null: \forall a. prod a nil = nil; + distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c) + }. + +theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.\forall f,a. + let aop \def sum B nil R in + let mop \def prod B nil R in + mop a \big[aop,nil]_{ibigop_Strue // >bigop_Strue // >(distr B nil R) >Hind // + |>bigop_Sfalse // >bigop_Sfalse // + ] +qed. + +(* Sigma e Pi + + +notation "Σ_{ ident i < n | p } f" + with precedence 80 +for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}. + +notation "Σ_{ ident i < n } f" + with precedence 80 +for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}. + +notation "Σ_{ ident j ∈ [a,b[ } f" + with precedence 80 +for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +notation "Σ_{ ident j ∈ [a,b[ | p } f" + with precedence 80 +for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +notation "Π_{ ident i < n | p} f" + with precedence 80 +for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}. + +notation "Π_{ ident i < n } f" + with precedence 80 +for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}. + +notation "Π_{ ident j ∈ [a,b[ } f" + with precedence 80 +for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +notation "Π_{ ident j ∈ [a,b[ | p } f" + with precedence 80 +for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +*) +(* + +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. + + + +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/weblib/arithmetics/binomial.ma b/weblib/arithmetics/binomial.ma new file mode 100644 index 000000000..9397f7b4d --- /dev/null +++ b/weblib/arithmetics/binomial.ma @@ -0,0 +1,133 @@ +(* + ||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/sigma_pi.ma". +include "arithmetics/primes.ma". + +(* binomial coefficient *) +definition bc ≝ λn,k. n!/(k!*(n-k)!). + +lemma bceq :∀n,k. bc n k = n!/(k!*(n-k)!). +// qed. + +theorem bc_n_n: ∀n. bc n n = 1. +#n >bceq bceq (minus_Sn_m k) [// |@le_S_S_to_le //] + ] +qed. + +theorem bc2 : ∀n. +∀k. k ≤n → k!*(n-k)! ∣ n!. +#n (elim n) + [#k #lek0 <(le_n_O_to_eq ? lek0) // + |#m #Hind #k (cases k) normalize // + #c #lec cases (le_to_or_lt_eq … (le_S_S_to_le …lec)) + [#ltcm + cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc + lapply (Hind c (le_S_S_to_le … lec)) #Hc + lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc + >(plus_minus_m_m m c) in ⊢ (??(??(?%))) [|@le_S_S_to_le //] + >commutative_plus >(distributive_times_plus ? (S c)) + @divides_plus + [>associative_times >(commutative_times (S c)) + commutative_times @Hmc + ] + |#eqcm >eqcm bceq >(bceq n) >(bceq n (S k)) +>(div_times_times ?? (S k)) in ⊢ (???(?%?)) + [|>(times_n_O 0) @lt_times // | //] +>associative_times in ⊢ (???(?(??%)?)) +>commutative_times in ⊢ (???(?(??(??%))?)) +(div_times_times ?? (n - k)) in ⊢ (???(??%)) + [|>(times_n_O 0) @lt_times // + |@(le_plus_to_le_r k ??) associative_times in ⊢ (???(??(??%))) +>fact_minus // commutative_plus in ⊢ (???%) associative_times >(commutative_times (S k)) + (times_n_O 0) @lt_times [@(le_1_fact (S k)) | //] + ] +qed. + +theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m. +#n (elim n) + [#m #lemO @(le_n_O_elim ? lemO) // + |-n #n #Hind #m (cases m) // + #m #lemn cases(le_to_or_lt_eq … (le_S_S_to_le …lemn)) // + #ltmn >bc1 // >(plus_O_n 0) @lt_plus @Hind /2/ + ] +qed. + +theorem binomial_law:∀a,b,n. + (a+b)^n = Σ_{k < S n}((bc n k)*(a^(n-k))*(b^k)). +#a #b #n (elim n) // +-n #n #Hind normalize in ⊢ (? ? % ?). +>bigop_Strue // >Hind >distributive_times_plus +<(minus_n_n (S n)) (bigop_distr ???? natDop ? a) >(bigop_distr ???? natDop ? b) +>bigop_Strue in ⊢ (??(??%)?) // associative_plus @eq_f2 + [bc_n_n >bc_n_n normalize // + |>bigop_0 >associative_plus >commutative_plus in ⊢ (??(??%)?) + bigop_0 // @eq_f2 + [>(bigop_op n ??? natACop) @same_bigop // + #i #ltin #_ (commutative_times b) + >(associative_times ?? b) <(distributive_times_plus_r (b^(S i))) + @eq_f2 // (commutative_times a) + >associative_times cut(∀n.a*a^n = a^(S n)) [#n @commutative_times] #H + >H commutative_plus @bc1 // + |>bc_n_O >bc_n_O normalize // + ] + ] +qed. + +theorem exp_S_sigma_p:∀a,n. +(S a)^n = Σ_{k < S n}((bc n k)*a^(n-k)). +#a #n cut (S a = a + 1) // #H >H +>binomial_law @same_bigop // +qed. + +(* +theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n). +intros.simplify. +rewrite < times_n_SO. +rewrite < plus_n_O. +rewrite < sym_times.simplify. +rewrite < assoc_plus. +rewrite < sym_plus. +reflexivity. +qed. *) + diff --git a/weblib/arithmetics/chinese_reminder.ma b/weblib/arithmetics/chinese_reminder.ma new file mode 100644 index 000000000..0837e429e --- /dev/null +++ b/weblib/arithmetics/chinese_reminder.ma @@ -0,0 +1,132 @@ +(* + ||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/exp.ma". +include "arithmetics/gcd.ma". +include "arithmetics/congruence.ma". + +theorem congruent_ab: ∀m,n,a,b:nat. O < n → O < m → + gcd n m = 1 → ∃x.x ≅_{m} a ∧ x ≅_{n} b. +#m #n #a #b #posn #posm #pnm +cut (∃c,d.c*n - d*m = 1 ∨ d*m - c*n = 1) [associative_times >H <(commutative_plus ? (d*m)) + >distributive_times_plus associative_plus + commutative_plus + @minus_to_plus // @(transitive_le … (le_n_Sn …)) + @(lt_minus_to_plus_r 0) //] #H1 + >(associative_times b d) >H1 >distributive_times_minus + commutative_times + @monotonic_le_times_r @(transitive_le ? (m*b)) /2/ + |applyS monotonic_le_times_r @le_plus_to_minus // + ] + ] + |(* and now the symmetric case; the price to pay for working + in nat instead than Z *) + @(ex_intro nat ? ((b+a*n)*d*m-a*c*n)) % + [(* congruent to a *) + cut (c*n = d*m - 1) + [@sym_eq @plus_to_minus >commutative_plus @minus_to_plus // @(transitive_le … (le_n_Sn …)) + @(lt_minus_to_plus_r 0) //] #H1 + >(associative_times a c) >H1 + >distributive_times_minus + commutative_times @monotonic_le_times_r + @(transitive_le ? (n*a)) /2/ + |@monotonic_le_times_r associative_times >H + >(commutative_plus (c*n)) + >distributive_times_plus associative_plus + commutative_times @congruent_n_mod_times // + |@(transitive_congruent n ? x) // + @sym_eq @congruent_n_mod_times // + ] + |@lt_mod_m_m >(times_n_O 0) @lt_times // + ] +qed. + +definition cr_pair ≝ λn,m,a,b. +min (n*m) 0 (λx. andb (eqb (x \mod n) a) (eqb (x \mod m) b)). + +example cr_pair1: cr_pair 2 3 O O = O. +// qed. + +example cr_pair2: cr_pair 2 3 1 0 = 3. +// qed. + +example cr_pair3: cr_pair 2 3 1 2 = 5. +// qed. + +example cr_pair4: cr_pair 5 7 3 2 = 23. +// qed. + +example cr_pair5: cr_pair 3 7 0 4 = ?. +normalize +// qed. + +theorem mod_cr_pair : ∀m,n,a,b. a < m → b < n → gcd n m = 1 → +(cr_pair m n a b) \mod m = a ∧ (cr_pair m n a b) \mod n = b. +#m #n #a #b #ltam #ltbn #pnm +cut (andb (eqb ((cr_pair m n a b) \mod m) a) + (eqb ((cr_pair m n a b) \mod n) b) = true) + [@f_min_true cases(congruent_ab_lt m n a b ?? pnm) + [#x * * #cxa #cxb #ltx @(ex_intro ?? x) % /2/ + >eq_to_eqb_true + [>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) // + |<(lt_to_eq_mod …ltam) // + ] + |@(le_to_lt_to_lt … ltbn) // + |@(le_to_lt_to_lt … ltam) // + ] + |#H >(eqb_true_to_eq … (andb_true_l … H)) >(eqb_true_to_eq … (andb_true_r … H)) /2/ + ] +qed. diff --git a/weblib/arithmetics/congruence.ma b/weblib/arithmetics/congruence.ma new file mode 100644 index 000000000..d1afc19ee --- /dev/null +++ b/weblib/arithmetics/congruence.ma @@ -0,0 +1,118 @@ +(* + ||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/primes.ma". + +(* successor mod n *) +definition S_mod: nat → nat → nat ≝ +λn,m:nat. (S m) \mod n. + +definition congruent: nat → nat → nat → Prop ≝ +λn,m,p:nat. mod n p = mod m p. + +interpretation "congruent" 'congruent n m p = (congruent n m p). + +notation "hvbox(n break ≅_{p} m)" + non associative with precedence 45 + for @{ 'congruent $n $m $p }. + +theorem congruent_n_n: ∀n,p:nat.n ≅_{p} n . +// qed. + +theorem transitive_congruent: + ∀p.transitive nat (λn,m.congruent n m p). +/2/ qed. + +theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m. +#n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m)) +% // @lt_mod_m_m @(ltn_to_ltO … ltnm) +qed. + +theorem mod_mod : ∀n,p:nat. O

(div_mod (n \mod p) p) in ⊢ (? ? % ?) +>(eq_div_O ? p) // @lt_mod_m_m // +qed. + +theorem mod_times_mod : ∀n,m,p:nat. O

distributive_times_plus_r + >associative_plus associative_times distributive_times_plus_r + >associative_plus commutative_times >(div_mod n p) in ⊢ (??%?) +>(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p)) +distributive_times_plus >distributive_times_plus_r + >distributive_times_plus_r congn >congm @sym_eq @mod_times // +qed. + +(* +theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to +congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p. +intros. +elim n. simplify. +apply congruent_n_mod_n.assumption. +simplify. +apply congruent_times. +assumption. +apply congruent_n_mod_n.assumption. +assumption. +qed. *) diff --git a/weblib/arithmetics/div_and_mod.ma b/weblib/arithmetics/div_and_mod.ma new file mode 100644 index 000000000..4044695d2 --- /dev/null +++ b/weblib/arithmetics/div_and_mod.ma @@ -0,0 +1,442 @@ +(* + ||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 ⊢ (? ? %) @(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 m q) in ⊢ (? ? (? % ?)) >(div_mod n q) in ⊢ (? ? (? ? %)) +>commutative_plus in ⊢ (? ? (? % ?)) >associative_plus in ⊢ (? ? %) + 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 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_plus_to_minus // |/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) div_times // +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) // @div_mod_spec_div_mod /2/ + |@div_mod_spec_intro + [applyS (monotonic_lt_times_r … c posc) /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 // >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/weblib/arithmetics/exp.ma b/weblib/arithmetics/exp.ma new file mode 100644 index 000000000..1205044be --- /dev/null +++ b/weblib/arithmetics/exp.ma @@ -0,0 +1,139 @@ +(* + ||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/div_and_mod.ma". + +let rec exp n m on m ≝ + match m with + [ O ⇒ 1 + | S p ⇒ (exp n p) * n]. + +interpretation "natural exponent" 'exp a b = (exp a b). + +theorem exp_plus_times : ∀n,p,q:nat. + n^(p + q) = n^p * n^q. +#n #p #q elim p normalize // +qed. + +theorem exp_n_O : ∀n:nat. 1 = n^O. +// +qed. + +theorem exp_n_1 : ∀n:nat. n = n^1. +#n normalize // +qed. + +theorem exp_1_n : ∀n:nat. 1 = 1^n. +#n (elim n) normalize // +qed. + +theorem exp_2: ∀n. n^2 = n*n. +#n normalize // +qed. + +theorem exp_exp_times : ∀n,p,q:nat. + (n^p)^q = n^(p * q). +#n #p #q (elim q) normalize +(* [applyS exp_n_O funziona ma non lo trova *) +// H normalize @le_times // + |cut (pred (2*(S n)) = S(S(pred(2*n)))) + [>S_pred // @(le_times 1 ? 1) //] #H1 + cut (2^(pred (2*(S n))) = 2^(pred(2*n))*2*2) + [>H1 >H1 //] #H2 >H2 + @(transitive_le ? ((2^(pred (2*n))) * n! * n! *(2*(S n))*(2*(S n)))) + [@le_times[@le_times //]// + (* we generalize to hide the computational content *) + |normalize in match ((S n)!) generalize in match (S n) + #Sn generalize in match 2 #two // + ] + ] +qed. + +theorem fact_to_exp: ∀n. + (2*n)! ≤ (2^(pred (2*n))) * n! * n!. +#n (cases n) [normalize // |#n @fact_to_exp1 //] +qed. + +theorem exp_to_fact1: ∀n.O < n → + 2^(2*n)*n!*n! < (S(2*n))!. +#n #posn (elim posn) [normalize //] +#n #posn #Hind (cut (∀i.2*(S i) = S(S(2*i)))) [//] #H +cut (2^(2*(S n)) = 2^(2*n)*2*2) [>H //] #H1 >H1 +@(le_to_lt_to_lt ? (2^(2*n)*n!*n!*(2*(S n))*(2*(S n)))) + [normalize in match ((S n)!) generalize in match (S n) #Sn + generalize in match 2 #two // + |cut ((S(2*(S n)))! = (S(2*n))!*(S(S(2*n)))*(S(S(S(2*n))))) + [>H //] #H2 >H2 @lt_to_le_to_lt_times + [@lt_to_le_to_lt_times //|>H // | //] + ] +qed. + +(* a slightly better result +theorem fact3: \forall n.O < n \to +(exp 2 (2*n))*(exp (fact n) 2) \le 2*n*fact (2*n). +intros. +elim H + [simplify.apply le_n + |rewrite > times_SSO. + rewrite > factS. + rewrite < times_exp. + change in ⊢ (? (? % ?) ?) with ((S(S O))*((S(S O))*(exp (S(S O)) ((S(S O))*n1)))). + rewrite > assoc_times. + rewrite > assoc_times in ⊢ (? (? ? %) ?). + rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?). + rewrite < sym_times in ⊢ (? (? ? (? ? (? % ?))) ?). + rewrite > assoc_times in ⊢ (? (? ? (? ? %)) ?). + apply (trans_le ? (((S(S O))*((S(S O))*((S n1)\sup((S(S O)))*((S(S O))*n1*((S(S O))*n1)!)))))) + [apply le_times_r. + apply le_times_r. + apply le_times_r. + assumption + |rewrite > factS. + rewrite > factS. + rewrite < times_SSO. + rewrite > assoc_times in ⊢ (? ? %). + apply le_times_r. + rewrite < assoc_times. + change in ⊢ (? (? (? ? %) ?) ?) with ((S n1)*((S n1)*(S O))). + rewrite < assoc_times in ⊢ (? (? % ?) ?). + rewrite < times_n_SO. + rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?). + rewrite < assoc_times in ⊢ (? ? %). + rewrite < assoc_times in ⊢ (? ? (? % ?)). + apply le_times_r. + apply le_times_l. + apply le_S.apply le_n + ] + ] +qed. + +theorem le_fact_10: fact (2*5) \le (exp 2 ((2*5)-2))*(fact 5)*(fact 5). +simplify in \vdash (? (? %) ?). +rewrite > factS in \vdash (? % ?). +rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash(? % ?). +rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?). +rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?). +rewrite > factS in \vdash (? % ?).rewrite < assoc_times in \vdash (? % ?). +apply le_times_l. +apply leb_true_to_le.reflexivity. +qed. + +theorem ab_times_cd: \forall a,b,c,d.(a*b)*(c*d)=(a*c)*(b*d). +intros. +rewrite > assoc_times. +rewrite > assoc_times. +apply eq_f. +rewrite < assoc_times. +rewrite < assoc_times. +rewrite > sym_times in \vdash (? ? (? % ?) ?). +reflexivity. +qed. + +(* an even better result *) +theorem lt_SSSSO_to_fact: \forall n.4 times_SSO. + change in \vdash (? ? (? (? (? ? %) ?) ?)) with (2*n1 - O); + rewrite < minus_n_O. + rewrite > factS. + rewrite > factS. + rewrite < assoc_times. + rewrite > factS. + apply (trans_le ? ((2*(S n1))*(2*(S n1))*(fact (2*n1)))) + [apply le_times_l. + rewrite > times_SSO. + apply le_times_r. + apply le_n_Sn + |apply (trans_le ? (2*S n1*(2*S n1)*(2\sup(2*n1-2)*n1!*n1!))) + [apply le_times_r.assumption + |rewrite > assoc_times. + rewrite > ab_times_cd in \vdash (? (? ? %) ?). + rewrite < assoc_times. + apply le_times_l. + rewrite < assoc_times in \vdash (? (? ? %) ?). + rewrite > ab_times_cd. + apply le_times_l. + rewrite < exp_S. + rewrite < exp_S. + apply le_exp + [apply lt_O_S + |rewrite > eq_minus_S_pred. + rewrite < S_pred + [rewrite > eq_minus_S_pred. + rewrite < S_pred + [rewrite < minus_n_O. + apply le_n + |elim H1;simplify + [apply lt_O_S + |apply lt_O_S + ] + ] + |elim H1;simplify + [apply lt_O_S + |rewrite < plus_n_Sm. + rewrite < minus_n_O. + apply lt_O_S + ] + ] + ] + ] + ] + ] +qed. *) diff --git a/weblib/arithmetics/gcd.ma b/weblib/arithmetics/gcd.ma new file mode 100644 index 000000000..104b59862 --- /dev/null +++ b/weblib/arithmetics/gcd.ma @@ -0,0 +1,406 @@ +(* + ||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/primes.ma". + +let rec gcd_aux p m n: nat ≝ +match p with + [O ⇒ m + |S q ⇒ + match dividesb n m with + [ true ⇒ n + | false ⇒ gcd_aux q n (m \mod n)]]. + +definition gcd : nat → nat → nat ≝ λn,m:nat. + match leb n m with + [ true ⇒ gcd_aux n m n + | false ⇒ gcd_aux m n m ]. + +theorem commutative_gcd: ∀n,m. gcd n m = gcd m n. +#n #m normalize @leb_elim + [#lenm cases(le_to_or_lt_eq … lenm) + [#ltnm >not_le_to_leb_false // @lt_to_not_le // + |#eqnm >eqnm (cases (leb m m)) // + ] + |#notlenm >le_to_leb_true // @(transitive_le ? (S m)) // + @not_le_to_lt // + ] +qed. + +theorem gcd_O_l: ∀m. gcd O m = m. +// qed. + +theorem divides_mod: ∀p,m,n:nat. O < n → + p ∣ m → p ∣ n → p ∣ (m \mod n). +#p #m #n #posn * #qm #eqm * #qn #eqn +@(quotient ?? (qm - qn*(m / n))) >distributive_times_minus +distributive_times_plus +divides_to_dividesb_true normalize // +qed. + +theorem divides_to_gcd: ∀m,n. O < n → n ∣ m → + gcd n m = n. +#m #n #posn (cases m) + [>commutative_gcd // + |#l #divn (cut (n ≤ (S l))) [@divides_to_le //] #len normalize + >le_to_leb_true // normalize @divides_to_gcd_aux // + ] +qed. + +lemma not_divides_to_gcd_aux: ∀p,m,n. 0 < n → n ∤ m → + gcd_aux (S p) m n = gcd_aux p n (m \mod n). +#p #m #n #lenm #divnm normalize >not_divides_to_dividesb_false +normalize // qed. + +theorem divides_gcd_aux_mn: ∀p,m,n. O < n → n ≤ m → n ≤ p → + gcd_aux p m n ∣ m ∧ gcd_aux p m n ∣ n. +#p (elim p) + [#m #n #posn #lenm #lenO @False_ind @(absurd … posn) /2/ + |#q #Hind #m #n #posn #lenm #lenS cases(decidable_divides n m) + [#divnm >(divides_to_gcd_aux … posn divnm) // % // + |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm) + cut (gcd_aux q n (m \mod n) ∣ n ∧ + gcd_aux q n (m \mod n) ∣ mod m n) + [cut (m \mod n < n) [@lt_mod_m_m //] #ltmod + @Hind + [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO + @False_ind @(absurd ?? ndivnm) @mod_O_to_divides // + |/2/ + |@le_S_S_to_le @(transitive_le … ltmod lenS) + ] + |* #H #H1 % [@(divides_mod_to_divides … posn H1) // |//] + ] + ] + ] +qed. + +theorem divides_gcd_nm: ∀n,m. + gcd n m ∣ m ∧ gcd n m ∣ n. +#n #m cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO (divides_to_gcd_aux … posn divnm) // + |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm) + cut (m \mod n < n) [@lt_mod_m_m //] #ltmod + @Hind // + [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO + @False_ind @(absurd ?? ndivnm) @mod_O_to_divides // + |/2/ + |@le_S_S_to_le @(transitive_le … ltmod lenS) + |(times_n_O 0) @lt_times // + ] + ] + ] +qed. + +(*a particular case of the previous theorem, with c=1 *) +theorem divides_gcd_aux: ∀p,m,n,d. O < n → n ≤ m → n ≤ p → + d ∣ m \to d ∣ n \to d ∣ gcd_aux p m n. + (* bell'esempio di smart application *) +/2/ qed. + +theorem divides_d_times_gcd: ∀m,n,d,c. O < c → + d ∣ (c*m) → d ∣ (c*n) → d ∣ c*gcd n m. +#m #n #d #c #posc #dcm #dcn +cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO (divides_to_gcd_aux … posn divnm) // + @(ex_intro ?? 1) @(ex_intro ?? 0) %1 // + |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm) + cut (m \mod n < n) [@lt_mod_m_m //] #ltmod + lapply (Hind n (m \mod n) ???) + [@le_S_S_to_le @(transitive_le … ltmod lenS) + |/2/ + |cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO + @False_ind @(absurd ?? ndivnm) @mod_O_to_divides // + ] + * #a * #b * #H + [(* first case *) + distributive_times_plus_r + >(div_mod m n) in ⊢(? ? (? % ?) ?) + >associative_times distributive_times_plus + distributive_times_plus_r + >(div_mod m n) in ⊢ (? ? (? ? %) ?) + >distributive_times_plus >associative_times + eqn0 @(ex_intro ?? O) @(ex_intro ? ? 1) %2 applyS minus_n_O] +#posn cases(le_to_or_lt_eq …(le_O_n m)) + [|#eqm0 >eqm0 @(ex_intro ?? 1) @(ex_intro ? ? 0) %1 applyS minus_n_O] +#posm normalize @leb_elim normalize + [#lenm @eq_minus_gcd_aux // + |#nlenm lapply(eq_minus_gcd_aux m n m posm ? (le_n m)) + [@(transitive_le … (not_le_to_lt … nlenm)) //] + * #a * #b * #H @(ex_intro ?? b) @(ex_intro ?? a) [%2 // |%1 //] + ] +qed. + +(* some properties of gcd *) + +theorem gcd_O_to_eq_O:∀m,n:nat. + gcd m n = O → m = O ∧ n = O. +#m #n #H cut (O ∣ n ∧ O ∣ m) + [(times_n_O O) @lt_times // |@divides_d_gcd /2/] + ] +qed. + +theorem le_gcd_times: ∀m,n,p. O< p → gcd m n ≤ gcd m (n*p). +#m #n #p #posp @(nat_case n) // +#l #eqn @divides_to_le [@lt_O_gcd >(times_n_O O) @lt_times //] +@divides_d_gcd [@(transitive_divides ? (S l)) /2/ |//] +qed. + +theorem gcd_times_SO_to_gcd_SO: ∀m,n,p:nat. O < n → O < p → + gcd m (n*p) = 1 → gcd m n = 1. +#m #n #p #posn #posp #gcd1 @le_to_le_to_eq + [commutative_gcd @lt_O_gcd //] +qed. + +theorem divides_gcd_mod: ∀m,n:nat. O < n → + gcd m n ∣ gcd n (m \mod n). +#m #n #posn @divides_d_gcd [@divides_mod // | //] +qed. + +theorem divides_mod_gcd: ∀m,n:nat. O < n → + gcd n (m \mod n) ∣ gcd m n. +#m #n #posn @divides_d_gcd + [@divides_gcd_l |@(divides_mod_to_divides ?? n) //] +qed. + +theorem gcd_mod: ∀m,n:nat. O < n → + gcd n (m \mod n) = gcd m n. +#m #n #posn @antisymmetric_divides + [@divides_mod_gcd // | @divides_gcd_mod //] +qed. + +(* gcd and primes *) + +theorem prime_to_gcd_1: ∀n,m:nat. prime n → n ∤ m → + gcd n m = 1. +(* bella dimostrazione *) +#n #m * #lt1n #primen #ndivnm @le_to_le_to_eq + [@not_lt_to_le @(not_to_not … (primen (gcd n m) (divides_gcd_l …))) + @(not_to_not ? (n ∣m)) // + |@lt_O_gcd @not_eq_to_le_to_lt // @(not_to_not ? (n ∣ m)) // + ] +qed. + +(* primes and divides *) +theorem divides_times_to_divides: ∀p,n,m:nat.prime p → + p ∣ n*m → p ∣ n ∨ p ∣ m. +#p #n #m #primp * #c #nm +cases (decidable_divides p n) /2/ #ndivpn %2 +cut (∃a,b. a*n - b*p = 1 ∨ b*p - a*n = 1) + [<(prime_to_gcd_1 … primp ndivpn) >commutative_gcd @eq_minus_gcd] +* #a * #b * #H + [@(quotient ?? (a*c-b*m)) >distributive_times_minus (commutative_times p) >associative_times (commutative_times (p*b)) + distributive_times_minus <(associative_times p) + <(associative_times p) <(commutative_times a) >(associative_times a) + (commutative_times (a*n)) + (times_n_O 0) @lt_times //] +@not_lt_to_le % #lt1gcd +cut (smallest_factor (gcd p (n*m)) ∣ n ∨ + smallest_factor (gcd p (n*m)) ∣ m) + [@divides_times_to_divides + [@prime_smallest_factor_n // + |@(transitive_divides ? (gcd p (n*m))) // + @divides_smallest_factor_n /2/ + ] + |* #H + [@(absurd ?? (lt_to_not_le …(lt_SO_smallest_factor … lt1gcd))) + (times_n_O 0) @lt_times // | //] + |@(absurd ?? (lt_to_not_le … (lt_SO_smallest_factor …lt1gcd))) + (times_n_O 0) @lt_times // | //] + ] +qed. + + +theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p → +gcd p n = 1 → p ∣ (n*m) → p ∣ m. +#p #m #n #posn #gcd1 * #c #nm +cases(eq_minus_gcd m p) #a * #b * #H >gcd1 in H #H + [@(quotient ?? (a*n-c*b)) >distributive_times_minus (commutative_times m) >commutative_times + >associative_times distributive_times_minus (commutative_times m) <(commutative_times n) + >associative_times H5 in H4. +elim (divides_times_to_divides ? ? ? H1 H4) + [elim H.apply False_ind. + apply H2.apply sym_eq.apply H8 + [assumption + |apply prime_to_lt_SO.assumption + ] + |elim H6. + apply (witness ? ? n1). + rewrite > assoc_times. + rewrite < H7.assumption + ] +qed. +*) + +theorem divides_to_divides_times: ∀p,q,n. prime p → p ∤ q → + p ∣ n → q ∣ n → p*q ∣ n. +#p #q #n #primep #notdivpq #divpn * #b #eqn (>eqn in divpn) +#divpn cases(divides_times_to_divides ??? primep divpn) #H + [@False_ind /2/ + |cases H #c #eqb @(quotient ?? c) >eqb (exp_n_SO p). +apply (lt_max_to_false ? ? ? H2). +assumption. +qed. + +theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n. +intros. +cases n + [apply le_n + |apply lt_to_le. + apply lt_log_n_n + [assumption|apply lt_O_S] + ] +qed. + +theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)). +intros.cases n + [simplify.rewrite < times_n_SO.apply lt_to_le.assumption + |apply not_le_to_lt. + apply leb_false_to_not_le. + apply (lt_max_to_false ? (S n1) (S (log p (S n1)))) + [apply le_S_S.apply le_n + |apply lt_log_n_n + [assumption|apply lt_O_S] + ] + ] +qed. + +theorem log_times1: \forall p,n,m. S O < p \to O < n \to O < m \to +log p (n*m) \le S(log p n+log p m). +intros. +unfold in ⊢ (? (% ? ?) ?). +apply f_false_to_le_max + [apply (ex_intro ? ? O). + split + [apply le_O_n + |apply le_to_leb_true. + simplify. + rewrite > times_n_SO. + apply le_times;assumption + ] + |intros. + apply lt_to_leb_false. + apply (lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m))))) + [apply lt_times;apply lt_exp_log;assumption + |rewrite < exp_plus_times. + apply le_exp + [apply lt_to_le.assumption + |simplify. + rewrite < plus_n_Sm. + assumption + ] + ] + ] +qed. + +theorem log_times: \forall p,n,m.S O < p \to log p (n*m) \le S(log p n+log p m). +intros. +cases n + [apply le_O_n + |cases m + [rewrite < times_n_O. + apply le_O_n + |apply log_times1 + [assumption + |apply lt_O_S + |apply lt_O_S + ] + ] + ] +qed. + +theorem log_times_l: \forall p,n,m.O < n \to O < m \to S O < p \to +log p n+log p m \le log p (n*m) . +intros. +unfold log in ⊢ (? ? (% ? ?)). +apply f_m_to_le_max + [elim H + [rewrite > log_SO + [simplify. + rewrite < plus_n_O. + apply le_log_n_n. + assumption + |assumption + ] + |elim H1 + [rewrite > log_SO + [rewrite < plus_n_O. + rewrite < times_n_SO. + apply le_log_n_n. + assumption + |assumption + ] + |apply (trans_le ? (S n1 + S n2)) + [apply le_plus;apply le_log_n_n;assumption + |simplify. + apply le_S_S. + rewrite < plus_n_Sm. + change in ⊢ (? % ?) with ((S n1)+n2). + rewrite > sym_plus. + apply le_plus_r. + change with (n1 < n1*S n2). + rewrite > times_n_SO in ⊢ (? % ?). + apply lt_times_r1 + [assumption + |apply le_S_S.assumption + ] + ] + ] + ] + |apply le_to_leb_true. + rewrite > exp_plus_times. + apply le_times;apply le_exp_log;assumption + ] +qed. + +theorem log_exp: \forall p,n,m.S O < p \to O < m \to +log p ((exp p n)*m)=n+log p m. +intros. +unfold log in ⊢ (? ? (% ? ?) ?). +apply max_spec_to_max. +unfold max_spec. +split + [split + [elim n + [simplify. + rewrite < plus_n_O. + apply le_log_n_n. + assumption + |simplify. + rewrite > assoc_times. + apply (trans_le ? ((S(S O))*(p\sup n1*m))) + [apply le_S_times_SSO + [rewrite > (times_n_O O) in ⊢ (? % ?). + apply lt_times + [apply lt_O_exp. + apply lt_to_le. + assumption + |assumption + ] + |assumption + ] + |apply le_times + [assumption + |apply le_n + ] + ] + ] + |simplify. + apply le_to_leb_true. + rewrite > exp_plus_times. + apply le_times_r. + apply le_exp_log. + assumption + ] + |intros. + simplify. + apply lt_to_leb_false. + apply (lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m))))) + [apply lt_times_r1 + [apply lt_O_exp.apply lt_to_le.assumption + |apply lt_exp_log.assumption + ] + |rewrite < exp_plus_times. + apply le_exp + [apply lt_to_le.assumption + |rewrite < plus_n_Sm. + assumption + ] + ] + ] +qed. + +theorem eq_log_exp: \forall p,n.S O < p \to +log p (exp p n)=n. +intros. +rewrite > times_n_SO in ⊢ (? ? (? ? %) ?). +rewrite > log_exp + [rewrite > log_SO + [rewrite < plus_n_O.reflexivity + |assumption + ] + |assumption + |apply le_n + ] +qed. + +theorem log_exp1: \forall p,n,m.S O < p \to +log p (exp n m) \le m*S(log p n). +intros.elim m + [simplify in ⊢ (? (? ? %) ?). + rewrite > log_SO + [apply le_O_n + |assumption + ] + |simplify. + apply (trans_le ? (S (log p n+log p (n\sup n1)))) + [apply log_times.assumption + |apply le_S_S. + apply le_plus_r. + assumption + ] + ] +qed. + +theorem log_exp2: \forall p,n,m.S O < p \to O < n \to +m*(log p n) \le log p (exp n m). +intros. +apply le_S_S_to_le. +apply (lt_exp_to_lt p) + [assumption + |rewrite > sym_times. + rewrite < exp_exp_times. + apply (le_to_lt_to_lt ? (exp n m)) + [elim m + [simplify.apply le_n + |simplify.apply le_times + [apply le_exp_log. + assumption + |assumption + ] + ] + |apply lt_exp_log. + assumption + ] + ] +qed. + +lemma le_log_plus: \forall p,n.S O < p \to log p n \leq log p (S n). +intros;apply (bool_elim ? (leb (p*(exp p n)) (S n))) + [simplify;intro;rewrite > H1;simplify;apply (trans_le ? n) + [apply le_log_n_n;assumption + |apply le_n_Sn] + |intro;unfold log;simplify;rewrite > H1;simplify;apply le_max_f_max_g; + intros;apply le_to_leb_true;constructor 2;apply leb_true_to_le;assumption] +qed. + +theorem le_log: \forall p,n,m. S O < p \to n \le m \to +log p n \le log p m. +intros.elim H1 + [constructor 1 + |apply (trans_le ? ? ? H3);apply le_log_plus;assumption] +qed. + +theorem log_div: \forall p,n,m. S O < p \to O < m \to m \le n \to +log p (n/m) \le log p n -log p m. +intros. +apply le_plus_to_minus_r. +apply (trans_le ? (log p ((n/m)*m))) + [apply log_times_l + [apply le_times_to_le_div + [assumption + |rewrite < times_n_SO. + assumption + ] + |assumption + |assumption + ] + |apply le_log + [assumption + |rewrite > (div_mod n m) in ⊢ (? ? %) + [apply le_plus_n_r + |assumption + ] + ] + ] +qed. + +theorem log_n_n: \forall n. S O < n \to log n n = S O. +intros. +rewrite > exp_n_SO in ⊢ (? ? (? ? %) ?). +rewrite > times_n_SO in ⊢ (? ? (? ? %) ?). +rewrite > log_exp + [rewrite > log_SO + [reflexivity + |assumption + ] + |assumption + |apply le_n + ] +qed. + +theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to +log i ((S(S O))*n) = S O. +intros. +apply antisymmetric_le + [apply not_lt_to_le.intro. + apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O)))) + [rewrite > exp_SSO. + apply lt_times + [apply (le_to_lt_to_lt ? n);assumption + |assumption + ] + |apply (trans_le ? (exp i (log i ((S(S O))*n)))) + [apply le_exp + [apply (ltn_to_ltO ? ? H1) + |assumption + ] + |apply le_exp_log. + rewrite > (times_n_O O) in ⊢ (? % ?). + apply lt_times + [apply lt_O_S + |apply lt_to_le.assumption + ] + ] + ] + |apply (trans_le ? (log i i)) + [rewrite < (log_n_n i) in ⊢ (? % ?) + [apply le_log + [apply (trans_lt ? n);assumption + |apply le_n + ] + |apply (trans_lt ? n);assumption + ] + |apply le_log + [apply (trans_lt ? n);assumption + |assumption + ] + ] + ] +qed. + +theorem exp_n_O: \forall n. O < n \to exp O n = O. +intros.apply (lt_O_n_elim ? H).intros. +simplify.reflexivity. +qed. + +(* +theorem tech1: \forall n,i.O < n \to +(exp (S n) (S(S i)))/(exp n (S i)) \le ((exp n i) + (exp (S n) (S i)))/(exp n i). +intros. +simplify in ⊢ (? (? ? %) ?). +rewrite < eq_div_div_div_times + [apply monotonic_div + [apply lt_O_exp.assumption + |apply le_S_S_to_le. + apply lt_times_to_lt_div. + change in ⊢ (? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))). + + + |apply (trans_le ? ((n)\sup(i)*(S n)\sup(S i)/(n)\sup(S i))) + [apply le_times_div_div_times. + apply lt_O_exp.assumption + |apply le_times_to_le_div2 + [apply lt_O_exp.assumption + |simplify. + +theorem tech1: \forall a,b,n,m.O < m \to +n/m \le b \to (a*n)/m \le a*b. +intros. +apply le_times_to_le_div2 + [assumption + | + +theorem tech2: \forall n,m. O < n \to +(exp (S n) m) / (exp n m) \le (n + m)/n. +intros. +elim m + [rewrite < plus_n_O.simplify. + rewrite > div_n_n.apply le_n + |apply le_times_to_le_div + [assumption + |apply (trans_le ? (n*(S n)\sup(S n1)/(n)\sup(S n1))) + [apply le_times_div_div_times. + apply lt_O_exp + |simplify in ⊢ (? (? ? %) ?). + rewrite > sym_times in ⊢ (? (? ? %) ?). + rewrite < eq_div_div_div_times + [apply le_times_to_le_div2 + [assumption + | + + +theorem le_log_sigma_p:\forall n,m,p. O < m \to S O < p \to +log p (exp n m) \le sigma_p n (\lambda i.true) (\lambda i. (m / i)). +intros. +elim n + [rewrite > exp_n_O + [simplify.apply le_n + |assumption + ] + |rewrite > true_to_sigma_p_Sn + [apply (trans_le ? (m/n1+(log p (exp n1 m)))) + [ +*) +*) diff --git a/weblib/arithmetics/minimization.ma b/weblib/arithmetics/minimization.ma new file mode 100644 index 000000000..eda9d0166 --- /dev/null +++ b/weblib/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 // @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 >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 // + |(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 /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) #H >H >H // + |>false_min // >false_min // @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 // + |>false_min // #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 // + |(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 + b ∧ 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 /2/ +qed. diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma new file mode 100644 index 000000000..6fa6d57a8 --- /dev/null +++ b/weblib/arithmetics/nat.ma @@ -0,0 +1,1119 @@ +(* + ||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+0. +#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. + +theorem times_n_1 : ∀n:nat. n = n * 1. +#n // 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 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_r: + ∀c:nat. O < c → monotonic nat lt (λt.(c*t)). +#c #posc #n #m #ltnm +(elim ltnm) normalize + [/2/ + |#a #_ #lt1 @(transitive_le … lt1) // + ] +qed. + +theorem monotonic_lt_times_l: + ∀c:nat. O < c → monotonic nat lt (λt.(t*c)). +/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_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 le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p. +#n #m #p #lep /2/ qed. + +theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b. +#a #b #c #H @(le_plus_to_le_r … b) /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. a < b - c → a + c < b. +#a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …)) +@lt_to_not_le // +qed. + +theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p. +#n #m #p #lenm #H normalize eq_minus_O /2/ >eq_minus_O // + @monotonic_le_times_r /2/ + |@sym_eq (applyS plus_to_minus) eq_minus_O /2/ >eq_minus_O // + ] +qed. + +(* +theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p). +#n #m #p #lepm @plus_to_minus >(commutative_plus p) +>associative_plus (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. + diff --git a/weblib/arithmetics/nth_prime.ma b/weblib/arithmetics/nth_prime.ma new file mode 100644 index 000000000..7b7c70bfe --- /dev/null +++ b/weblib/arithmetics/nth_prime.ma @@ -0,0 +1,201 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "nat/primes.ma". +include "nat/lt_arith.ma". + +(* upper bound by Bertrand's conjecture. *) +(* Too difficult to prove. +let rec nth_prime n \def +match n with + [ O \Rightarrow (S(S O)) + | (S p) \Rightarrow + let previous_prime \def S (nth_prime p) in + min_aux previous_prime ((S(S O))*previous_prime) primeb]. + +theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))). +normalize.reflexivity. +qed. + +theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))). +normalize.reflexivity. +qed. + +theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))). +normalize.reflexivity. +qed. *) + +theorem smallest_factor_fact: \forall n:nat. +n < smallest_factor (S n!). +intros. +apply not_le_to_lt.unfold Not. +intro. +apply (not_divides_S_fact n (smallest_factor(S n!))). +apply lt_SO_smallest_factor. +unfold lt.apply le_S_S.apply le_SO_fact. +assumption. +apply divides_smallest_factor_n. +unfold lt.apply le_S_S.apply le_O_n. +qed. + +theorem ex_prime: \forall n. (S O) \le n \to \exists m. +n < m \land m \le S n! \land (prime m). +intros. +elim H. +apply (ex_intro nat ? (S(S O))). +split.split.apply (le_n (S(S O))). +apply (le_n (S(S O))).apply (primeb_to_Prop (S(S O))). +apply (ex_intro nat ? (smallest_factor (S (S n1)!))). +split.split. +apply smallest_factor_fact. +apply le_smallest_factor_n. +(* Andrea: ancora hint non lo trova *) +apply prime_smallest_factor_n.unfold lt. +apply le_S.apply le_SSO_fact. +unfold lt.apply le_S_S.assumption. +qed. + +let rec nth_prime n \def +match n with + [ O \Rightarrow (S(S O)) + | (S p) \Rightarrow + let previous_prime \def (nth_prime p) in + let upper_bound \def S previous_prime! in + min_aux upper_bound (S previous_prime) primeb]. + +(* it works +theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))). +normalize.reflexivity. +qed. + +theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))). +normalize.reflexivity. +qed. + +theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))). +normalize.reflexivity. +qed. + +alias num (instance 0) = "natural number". +theorem example14 : nth_prime 18 = 67. +normalize.reflexivity. +qed. +*) + +theorem prime_nth_prime : \forall n:nat.prime (nth_prime n). +intro. +apply (nat_case n).simplify. +apply (primeb_to_Prop (S(S O))). +intro. +change with +(let previous_prime \def (nth_prime m) in +let upper_bound \def S previous_prime! in +prime (min_aux upper_bound (S previous_prime) primeb)). +apply primeb_true_to_prime. +apply f_min_aux_true. +apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))). +split.split. +apply smallest_factor_fact. +apply transitive_le; + [2: apply le_smallest_factor_n + | skip + | apply (le_plus_n_r (S (nth_prime m)) (S (fact (nth_prime m)))) + ]. +apply prime_to_primeb_true. +apply prime_smallest_factor_n.unfold lt. +apply le_S_S.apply le_SO_fact. +qed. + +(* properties of nth_prime *) +theorem increasing_nth_prime: increasing nth_prime. +unfold increasing. +intros. +change with +(let previous_prime \def (nth_prime n) in +let upper_bound \def S previous_prime! in +(S previous_prime) \le min_aux upper_bound (S previous_prime) primeb). +intros. +apply le_min_aux. +qed. + +variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat. +(nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime. + +theorem injective_nth_prime: injective nat nat nth_prime. +apply increasing_to_injective. +apply increasing_nth_prime. +qed. + +theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n. +intros. elim n.unfold lt.apply le_n. +apply (trans_lt ? (nth_prime n1)). +assumption.apply lt_nth_prime_n_nth_prime_Sn. +qed. + +theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n. +intros.apply (trans_lt O (S O)). +unfold lt. apply le_n.apply lt_SO_nth_prime_n. +qed. + +theorem lt_n_nth_prime_n : \forall n:nat. n \lt nth_prime n. +intro. +elim n + [apply lt_O_nth_prime_n + |apply (lt_to_le_to_lt ? (S (nth_prime n1))) + [unfold.apply le_S_S.assumption + |apply lt_nth_prime_n_nth_prime_Sn + ] + ] +qed. + +theorem ex_m_le_n_nth_prime_m: +\forall n: nat. nth_prime O \le n \to +\exists m. nth_prime m \le n \land n < nth_prime (S m). +intros. +apply increasing_to_le2. +exact lt_nth_prime_n_nth_prime_Sn.assumption. +qed. + +theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n) +\to \lnot (prime m). +intros. +apply primeb_false_to_not_prime. +letin previous_prime \def (nth_prime n). +letin upper_bound \def (S previous_prime!). +apply (lt_min_aux_to_false primeb (S previous_prime) upper_bound m). +assumption. +unfold lt. +apply (transitive_le (S m) (nth_prime (S n)) (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb) ? ?); + [apply (H1). + |apply (le_n (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb)). + ] +qed. + +(* nth_prime enumerates all primes *) +theorem prime_to_nth_prime : \forall p:nat. prime p \to +\exists i. nth_prime i = p. +intros. +cut (\exists m. nth_prime m \le p \land p < nth_prime (S m)). +elim Hcut.elim H1. +cut (nth_prime a < p \lor nth_prime a = p). +elim Hcut1. +absurd (prime p). +assumption. +apply (lt_nth_prime_to_not_prime a).assumption.assumption. +apply (ex_intro nat ? a).assumption. +apply le_to_or_lt_eq.assumption. +apply ex_m_le_n_nth_prime_m. +simplify.unfold prime in H.elim H.assumption. +qed. + diff --git a/weblib/arithmetics/primes.ma b/weblib/arithmetics/primes.ma new file mode 100644 index 000000000..71e372f96 --- /dev/null +++ b/weblib/arithmetics/primes.ma @@ -0,0 +1,530 @@ +(* + ||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/factorial.ma". +include "arithmetics/minimization.ma". + +inductive divides (n,m:nat) : Prop ≝ +quotient: ∀q:nat.m = times n q → divides n m. + +interpretation "divides" 'divides n m = (divides n m). +interpretation "not divides" 'ndivides n m = (Not (divides n m)). + +theorem reflexive_divides : reflexive nat divides. +/2/ qed. + +theorem divides_to_div_mod_spec : +∀n,m. O < n → n ∣ m → div_mod_spec m n (m / n) O. +#n #m #posn * #q #eqm % // >eqm +>commutative_times >div_times // +qed. + +theorem div_mod_spec_to_divides : +∀n,m,q. div_mod_spec m n q O → n ∣ m. +#n #m #q * #posn #eqm /2/ +qed. + +theorem divides_to_mod_O: +∀n,m. O < n → n ∣ m → (m \mod n) = O. +#n #m #posn #divnm +@(div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O) /2/ +qed. + +theorem mod_O_to_divides: +∀n,m. O < n → (m \mod n) = O → n ∣ m. +/2/ qed. + +theorem divides_n_O: ∀n:nat. n ∣ O. +/2/ qed. + +theorem divides_n_n: ∀n:nat. n ∣ n. +/2/ qed. + +theorem divides_SO_n: ∀n:nat. 1 ∣ n. +/2/ qed. + +theorem divides_plus: ∀n,p,q:nat. +n ∣ p → n ∣ q → n ∣ p+q. +#n #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1+d2)) +>H >H1 // +qed. + +theorem divides_minus: ∀n,p,q:nat. +n ∣ p → n ∣ q → n ∣ (p-q). +#n #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1-d2)) +>H >H1 // +qed. + +theorem divides_times: ∀n,m,p,q:nat. +n ∣ p → m ∣ q → n*m ∣ p*q. +#n #m #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1*d2)) +>H >associative_times >associative_times @eq_f // +qed. + +theorem transitive_divides: transitive ? divides. +#a #b #c * #d1 #H * #d2 #H1 @(quotient ?? (d1*d2)) +>H1 >H // +qed. + +theorem eq_mod_to_divides: ∀n,m,q. O < q → + mod n q = mod m q → q ∣ (n-m). +#n #m #q #posq #eqmod @(leb_elim n m) #nm + [cut (n-m=O) /2/ + |@(quotient ?? ((div n q)-(div m q))) + >distributive_times_minus >commutative_times + >(commutative_times q) cut((n/q)*q = n - (n \mod q)) [//] #H + >H >minus_plus >eqmod >commutative_plus + eqm // ] +qed. + +theorem antisymmetric_divides: ∀n,m. n ∣ m → m ∣ n → n = m. +#n #m #divnm #divmn (cases (le_to_or_lt_eq … (le_O_n n))) #Hn + [(cases (le_to_or_lt_eq … (le_O_n m))) #Hm + [@le_to_le_to_eq @divides_to_le // + | eqm // +qed. + +(*a variant of or_div_mod *) +theorem or_div_mod1: ∀n,q. O < q → + q ∣ S n ∧ S n = S (n/q) * q ∨ + q ∤ S n ∧ S n= (div n q) * q + S (n\mod q). +#n #q #posq cases(or_div_mod n q posq) * #H1 #H2 + [%1 % /2/ + |%2 % // @(not_to_not ? ? (divides_to_mod_O … posq)) + cut (S n \mod q = S(n \mod q)) + [@(div_mod_spec_to_eq2 (S n) q (S n/q) (S n \mod q) (n/q) (S (n \mod q))) /2/] + #Hcut >Hcut % /2/ + ] +qed. + +theorem divides_to_div: ∀n,m.n ∣m → m/n*n = m. +#n #m #divnm (cases (le_to_or_lt_eq O n (le_O_n n))) #H + [>(plus_n_O (m/n*n)) <(divides_to_mod_O ?? H divnm) // + |(cases divnm) #d divides_to_div // + |>divides_to_div + [>commutative_times >divides_to_div // + |@(quotient ? ? d) @sym_eq /2/ + ] + ] +qed. + +theorem times_div: ∀a,b,c:nat. + O < b → c ∣ b → a * (b /c) = (a*b)/c. +#a #b #c #posb #divcb +cut(O < c) [@(divides_to_lt_O … posb divcb)] #posc +(cases divcb) #d #eqb >eqb +>(commutative_times c d) >(div_times d c posc) (div_times (a * d) c posc) // +qed. + +theorem plus_div: ∀n,m,d. O < d → + d ∣ n → d ∣ m → (n + m) / d = n/d + m/d. +#n #m #d #posd #divdn #divdm +(cases divdn) #a #eqn (cases divdm) #b #eqm +>eqn >eqm commutative_times +>div_times // >commutative_times >div_times // +>commutative_times >div_times // +qed. + +(* boolean divides *) +definition dividesb : nat → nat → bool ≝ +λn,m :nat. (eqb (m \mod n) O). + +theorem dividesb_true_to_divides: +∀n,m:nat. dividesb n m = true → n ∣ m. +#n #m (cases (le_to_or_lt_eq … (le_O_n n))) + [#posn #divbnm @mod_O_to_divides // @eqb_true_to_eq @divbnm + |#eqnO (eqb_true_to_eq … eqbmO) // + ] +qed. + +theorem dividesb_false_to_not_divides: +∀n,m:nat. dividesb n m = false → n ∤ m. +#n #m (cases (le_to_or_lt_eq … (le_O_n n))) + [#posn #ndivbnm @(not_to_not ?? (divides_to_mod_O … posn)) + @eqb_false_to_not_eq @ndivbnm + |#eqnO bigop_Strue // + cases(le_to_or_lt_eq …(le_S_S_to_le … lti)) /3/ + ] +*) + +(* prime *) +definition prime : nat → Prop ≝ +λn:nat. 1 < n ∧ (∀m:nat. m ∣ n → 1 < m → m = n). + +theorem not_prime_O: ¬ (prime O). +% * #lt10 /2/ +qed. + +theorem not_prime_SO: ¬ (prime 1). +% * #lt11 /2/ +qed. + +theorem prime_to_lt_O: ∀p. prime p → O < p. +#p * #lt1p /2/ +qed. + +theorem prime_to_lt_SO: ∀p. prime p → 1 < p. +#p * #lt1p /2/ +qed. + +(* smallest factor *) +definition smallest_factor : nat → nat ≝ +λn:nat. if_then_else ? (leb n 1) n + (min n 2 (λm.(eqb (n \mod m) O))). + +theorem smallest_factor_to_min : ∀n. 1 < n → +smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))). +#n #lt1n normalize >lt_to_leb_false // +qed. + +(* it works ! +theorem example1 : smallest_factor 3 = 3. +normalize // +qed. + +theorem example2: smallest_factor 4 = 2. +normalize // +qed. + +theorem example3 : smallest_factor 7 = 7. +normalize // +qed. *) + +theorem le_SO_smallest_factor: ∀n:nat. + n ≤ 1 → smallest_factor n = n. +#n #le1n normalize >le_to_leb_true // +qed. + +theorem lt_SO_smallest_factor: ∀n:nat. + 1 < n → 1 < smallest_factor n. +#n #lt1n >smallest_factor_to_min // +qed. + +theorem lt_O_smallest_factor: ∀n:nat. + O < n → O < (smallest_factor n). +#n #posn (cases posn) + [>le_SO_smallest_factor // + |#m #posm @le_S_S_to_le @le_S @lt_SO_smallest_factor @le_S_S // + ] +qed. + +theorem divides_smallest_factor_n : ∀n:nat. 0 < n → + smallest_factor n ∣ n. +#n #posn (cases (le_to_or_lt_eq … posn)) + [#lt1n @mod_O_to_divides [@lt_O_smallest_factor //] + >smallest_factor_to_min // @eqb_true_to_eq @f_min_true + @(ex_intro … n) % /2/ @eq_to_eqb_true /2/ + |#H smallest_factor_to_min // #ltmin +@(not_to_not ? (n \mod i = 0)) + [#divin @divides_to_mod_O /2/ + |@eqb_false_to_not_eq @(lt_min_to_false … lti ltmin) + ] +qed. + +theorem prime_smallest_factor_n : ∀n. 1 < n → + prime (smallest_factor n). +#n #lt1n (cut (0smallest_factor_to_min // @true_to_le_min // + @eq_to_eqb_true @divides_to_mod_O /2/ + @(transitive_divides … divmmin) @divides_smallest_factor_n // + ] +qed. + +theorem prime_to_smallest_factor: ∀n. prime n → + smallest_factor n = n. +#n * #lt1n #primen @primen + [@divides_smallest_factor_n /2/ + |@lt_SO_smallest_factor // + ] +qed. + +theorem smallest_factor_to_prime: ∀n. 1 < n → + smallest_factor n = n → prime n. +#n #lt1n #H O is prime iff its smallest factor is n *) +definition primeb ≝ λn:nat. + (leb 2 n) ∧ (eqb (smallest_factor n) n). + +(* it works! *) +theorem example4 : primeb 3 = true. +normalize // qed. + +theorem example5 : primeb 6 = false. +normalize // qed. + +theorem example6 : primeb 11 = true. +normalize // qed. + +theorem example7 : primeb 17 = true. +normalize // qed. + +theorem primeb_true_to_prime : ∀n:nat. + primeb n = true → prime n. +#n #primebn @smallest_factor_to_prime + [@leb_true_to_le @(andb_true_l … primebn) + |@eqb_true_to_eq @( andb_true_r … primebn) + ] +qed. + +theorem primeb_false_to_not_prime : ∀n:nat. + primeb n = false → ¬ (prime n). +#n #H cut ((leb 2 n ∧ (eqb (smallest_factor n) n)) = false) [>H //] +@leb_elim + [#_ #H1 @(not_to_not … (prime_to_smallest_factor … )) + @eqb_false_to_not_eq @H1 + |#len1 #_ @(not_to_not … len1) * // + ] +qed. + +theorem decidable_prime : ∀n:nat.decidable (prime n). +#n cases(true_or_false (primeb n)) #H + [%1 /2/ |%2 /2/] +qed. + +theorem prime_to_primeb_true: ∀n:nat. + prime n → primeb n = true. +#n #primen (cases (true_or_false (primeb n))) // +#H @False_ind @(absurd … primen) /2/ +qed. + +theorem not_prime_to_primeb_false: ∀n:nat. + ¬(prime n) → primeb n = false. +#n #np (cases (true_or_false (primeb n))) // +#p @False_ind @(absurd (prime n) (primeb_true_to_prime …) np) // +qed. + +(* enumeration of all primes *) + +theorem divides_fact : ∀n,i:nat. O < i → + i ≤ n → i ∣ n!. +#n #i #ltOi (elim n) + [#leiO @False_ind @(absurd … ltOi) /2/ + |#n #Hind #lei normalize cases(le_to_or_lt_eq … lei) + [#ltiS @(transitive_divides ? n!) [@Hind /2/ | /2/] + |#eqi >eqi /2/ + ] + ] +qed. + +theorem mod_S_fact: ∀n,i:nat. + 1 < i → i ≤ n → (S n!) \mod i = 1. +#n #i #lt1i #lein +cut(Omod_S_fact // @eqb_false_to_not_eq // +qed. + +theorem smallest_factor_fact: ∀n:nat. + n < smallest_factor (S n!). +#n @not_le_to_lt @(not_to_not ? ((smallest_factor (S n!)) ∤ (S n!))) + [@not_divides_S_fact @lt_SO_smallest_factor @le_S_S // + |% * #H @H @divides_smallest_factor_n @le_S_S // + ] +qed. + +theorem ex_prime: ∀n. 1 ≤ n →∃m. + n < m ∧ m ≤ S n! ∧ (prime m). +#n #lein (cases lein) + [@(ex_intro nat ? 2) % [/2/|@primeb_true_to_prime //] + |#m #leim @(ex_intro nat ? (smallest_factor (S (S m)!))) + % [% [@smallest_factor_fact |@le_smallest_factor_n ] + |@prime_smallest_factor_n @le_S_S // + ] + ] +qed. + +let rec nth_prime n ≝ match n with + [ O ⇒ 2 + | S p ⇒ + let previous_prime ≝ nth_prime p in + let upper_bound ≝ S previous_prime! in + min upper_bound (S previous_prime) primeb]. + +lemma nth_primeS: ∀n.nth_prime (S n) = + let previous_prime ≝ nth_prime n in + let upper_bound ≝ S previous_prime! in + min upper_bound (S previous_prime) primeb. +// qed. + +(* it works *) +theorem example11 : nth_prime 2 = 5. +normalize // qed. + +theorem example12: nth_prime 3 = 7. +normalize // +qed. + +theorem example13 : nth_prime 4 = 11. +normalize // qed. + +(* done in 13.1369330883s -- qualcosa non va: // lentissimo +theorem example14 : nth_prime 18 = 67. +normalize // (* @refl *) +qed. +*) + +theorem prime_nth_prime : ∀n:nat.prime (nth_prime n). +#n (cases n) + [@primeb_true_to_prime // + |#m >nth_primeS @primeb_true_to_prime @f_min_true + @(ex_intro nat ? (smallest_factor (S (nth_prime m)!))) + % [% // @le_S_S @(transitive_le … (le_smallest_factor_n …)) + nth_primeS #ltmr @primeb_false_to_not_prime +@(lt_min_to_false ? (S (nth_prime n)!) m (S (nth_prime n))) // +qed. + +(* nth_prime enumerates all primes *) +theorem prime_to_nth_prime : ∀p:nat. + prime p → ∃i.nth_prime i = p. +#p #primep +cut (∃m. nth_prime m ≤ p ∧ p < nth_prime (S m)) + [@(increasing_to_le2 nth_prime ?) // @prime_to_lt_SO // + |* #n * #lepl #ltpr cases(le_to_or_lt_eq … lepl) + [#ltpl @False_ind @(absurd … primep) + @(lt_nth_prime_to_not_prime n p ltpl ltpr) + |#eqp @(ex_intro … n) // + ] + ] +qed. + diff --git a/weblib/arithmetics/sigma_pi.ma b/weblib/arithmetics/sigma_pi.ma new file mode 100644 index 000000000..d92d525b7 --- /dev/null +++ b/weblib/arithmetics/sigma_pi.ma @@ -0,0 +1,747 @@ +(* + ||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/bigops.ma". + +definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) + (λa,b,c.sym_eq ??? (associative_plus a b c)). + +definition natACop ≝ mk_ACop nat 0 natAop commutative_plus. + +definition natDop ≝ mk_Dop nat 0 natACop times (λn.(sym_eq ??? (times_n_O n))) + distributive_times_plus. + +unification hint 0 ≔ ; + S ≟ natAop +(* ---------------------------------------- *) ⊢ + plus ≡ op ? ? S. + +unification hint 0 ≔ ; + S ≟ natACop +(* ---------------------------------------- *) ⊢ + plus ≡ op ? ? S. + +unification hint 0 ≔ ; + S ≟ natDop +(* ---------------------------------------- *) ⊢ + plus ≡ sum ? ? S. + +unification hint 0 ≔ ; + S ≟ natDop +(* ---------------------------------------- *) ⊢ + times ≡ prod ? ? S. + +(* Sigma e Pi *) + +notation "∑_{ ident i < n | p } f" + with precedence 80 +for @{'bigop $n plus 0 (λ${ident i}.$p) (λ${ident i}. $f)}. + +notation "∑_{ ident i < n } f" + with precedence 80 +for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}. + +notation "∑_{ ident j ∈ [a,b[ } f" + with precedence 80 +for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +notation "∑_{ ident j ∈ [a,b[ | p } f" + with precedence 80 +for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +notation "∏_{ ident i < n | p} f" + with precedence 80 +for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}. + +notation "∏_{ ident i < n } f" + with precedence 80 +for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}. + +notation "∏_{ ident j ∈ [a,b[ } f" + with precedence 80 +for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + +notation "∏_{ ident j ∈ [a,b[ | p } f" + with precedence 80 +for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a))) + (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}. + + +(* + +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. + + + +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/weblib/basics/bool.ma b/weblib/basics/bool.ma new file mode 100644 index 000000000..adbfd9cab --- /dev/null +++ b/weblib/basics/bool.ma @@ -0,0 +1,76 @@ +(* + ||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". + +(********** bool **********) +inductive bool: Type[0] ≝ + | true : bool + | false : bool. + +(* destruct does not work *) +theorem not_eq_true_false : true ≠ false. +@nmk #Heq change with match true with [true ⇒ False|false ⇒ True] +>Heq // qed. + +definition notb : bool → bool ≝ +λ b:bool. match b with [true ⇒ false|false ⇒ true ]. + +interpretation "boolean not" 'not x = (notb x). + +theorem notb_elim: ∀ b:bool.∀ P:bool → Prop. +match b with +[ true ⇒ P false +| false ⇒ P true] → P (notb b). +#b #P elim b normalize // qed. + +theorem notb_notb: ∀b:bool. notb (notb b) = b. +#b elim b // qed. + +theorem injective_notb: injective bool bool notb. +#b1 #b2 #H // qed. + +definition andb : bool → bool → bool ≝ +λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ]. + +interpretation "boolean and" 'and x y = (andb x y). + +theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop. +match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2). +#b1 #b2 #P (elim b1) normalize // qed. + +theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true. +#b1 (cases b1) normalize // qed. + +theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true. +#b1 #b2 (cases b1) normalize // (cases b2) // qed. + +definition orb : bool → bool → bool ≝ +λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2]. + +interpretation "boolean or" 'or x y = (orb x y). + +theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop. +match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2). +#b1 #b2 #P (elim b1) normalize // qed. + +definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝ +λA.λb.λ P,Q:A. match b with [ true ⇒ P | false ⇒ Q]. + +theorem bool_to_decidable_eq: + ∀b1,b2:bool. decidable (b1=b2). +#b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed. + +theorem true_or_false: +∀b:bool. b = true ∨ b = false. +#b (cases b) /2/ qed. + + diff --git a/weblib/basics/core_notation.ma b/weblib/basics/core_notation.ma new file mode 100644 index 000000000..098b5d419 --- /dev/null +++ b/weblib/basics/core_notation.ma @@ -0,0 +1,287 @@ +(* exists *******************************************************************) + +notation "hvbox(∃ _ break . p)" + with precedence 20 +for @{'exists $p }. + +notation < "hvbox(\exists ident i : ty break . p)" + right associative with precedence 20 +for @{'exists (\lambda ${ident i} : $ty. $p) }. + +notation < "hvbox(\exists ident i break . p)" + with precedence 20 +for @{'exists (\lambda ${ident i}. $p) }. + +(* +notation < "hvbox(\exists ident i opt (: ty) break . p)" + right associative with precedence 20 +for @{ 'exists ${default + @{\lambda ${ident i} : $ty. $p} + @{\lambda ${ident i} . $p}}}. +*) + +notation > "\exists list1 ident x sep , opt (: T). term 19 Px" + with precedence 20 + for ${ default + @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } } + @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } } + }. + +(* sigma ********************************************************************) + +notation < "hvbox(\Sigma ident i : ty break . p)" + left associative with precedence 20 +for @{'sigma (\lambda ${ident i} : $ty. $p) }. + +notation < "hvbox(\Sigma ident i break . p)" + with precedence 20 +for @{'sigma (\lambda ${ident i}. $p) }. + +(* +notation < "hvbox(\Sigma ident i opt (: ty) break . p)" + right associative with precedence 20 +for @{ 'sigma ${default + @{\lambda ${ident i} : $ty. $p} + @{\lambda ${ident i} . $p}}}. +*) + +notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px" + with precedence 20 + for ${ default + @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } } + @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } } + }. + +(* equality, conguence ******************************************************) + +notation > "hvbox(a break = b)" + non associative with precedence 45 +for @{ 'eq ? $a $b }. + +notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)" + non associative with precedence 45 +for @{ 'eq $t $a $b }. + +notation > "hvbox(n break (≅ \sub term 90 p) m)" + non associative with precedence 45 +for @{ 'congruent $n $m $p }. + +notation < "hvbox(term 46 n break ≅ \sub p term 46 m)" + non associative with precedence 45 +for @{ 'congruent $n $m $p }. + +(* other notations **********************************************************) + +notation "hvbox(\langle term 19 a, break term 19 b\rangle)" +with precedence 90 for @{ 'pair $a $b}. + +notation "hvbox(x break \times y)" with precedence 70 +for @{ 'product $x $y}. + +notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}. +notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}. + +notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}. +notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}. + +notation > "\fst" with precedence 90 for @{'pi1}. +notation > "\snd" with precedence 90 for @{'pi2}. + +notation "hvbox(a break \to b)" + right associative with precedence 20 +for @{ \forall $_:$a.$b }. + +notation < "hvbox(a break \to b)" + right associative with precedence 20 +for @{ \Pi $_:$a.$b }. + +notation "hvbox(a break \leq b)" + non associative with precedence 45 +for @{ 'leq $a $b }. + +notation "hvbox(a break \geq b)" + non associative with precedence 45 +for @{ 'geq $a $b }. + +notation "hvbox(a break \lt b)" + non associative with precedence 45 +for @{ 'lt $a $b }. + +notation "hvbox(a break \gt b)" + non associative with precedence 45 +for @{ 'gt $a $b }. + +notation > "hvbox(a break \neq b)" + non associative with precedence 45 +for @{ 'neq ? $a $b }. + +notation < "hvbox(a break maction (\neq) (\neq\sub t) b)" + non associative with precedence 45 +for @{ 'neq $t $a $b }. + +notation "hvbox(a break \nleq b)" + non associative with precedence 45 +for @{ 'nleq $a $b }. + +notation "hvbox(a break \ngeq b)" + non associative with precedence 45 +for @{ 'ngeq $a $b }. + +notation "hvbox(a break \nless b)" + non associative with precedence 45 +for @{ 'nless $a $b }. + +notation "hvbox(a break \ngtr b)" + non associative with precedence 45 +for @{ 'ngtr $a $b }. + +notation "hvbox(a break \divides b)" + non associative with precedence 45 +for @{ 'divides $a $b }. + +notation "hvbox(a break \ndivides b)" + non associative with precedence 45 +for @{ 'ndivides $a $b }. + +notation "hvbox(a break + b)" + left associative with precedence 50 +for @{ 'plus $a $b }. + +notation "hvbox(a break - b)" + left associative with precedence 50 +for @{ 'minus $a $b }. + +notation "hvbox(a break * b)" + left associative with precedence 55 +for @{ 'times $a $b }. + +notation "hvbox(a break \middot b)" + left associative with precedence 55 + for @{ 'middot $a $b }. + +notation "hvbox(a break \mod b)" + left associative with precedence 55 +for @{ 'module $a $b }. + +notation < "a \frac b" + non associative with precedence 90 +for @{ 'divide $a $b }. + +notation "a \over b" + left associative with precedence 55 +for @{ 'divide $a $b }. + +notation "hvbox(a break / b)" + left associative with precedence 55 +for @{ 'divide $a $b }. + +notation "- term 60 a" with precedence 60 +for @{ 'uminus $a }. + +notation "a !" + non associative with precedence 80 +for @{ 'fact $a }. + +notation "\sqrt a" + non associative with precedence 60 +for @{ 'sqrt $a }. + +notation "hvbox(a break \lor b)" + left associative with precedence 30 +for @{ 'or $a $b }. + +notation "hvbox(a break \land b)" + left associative with precedence 35 +for @{ 'and $a $b }. + +notation "hvbox(\lnot a)" + non associative with precedence 40 +for @{ 'not $a }. + +notation > "hvbox(a break \liff b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + +notation "hvbox(a break \leftrightarrow b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + + +notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90 +for @{ 'powerset $A }. +notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90 +for @{ 'powerset $A }. + +notation < "hvbox({ ident i | term 19 p })" with precedence 90 +for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}. + +notation > "hvbox({ ident i | term 19 p })" with precedence 90 +for @{ 'subset (\lambda ${ident i}. $p)}. + +notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90 +for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}. + +notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90 +for @{ 'comprehension $s (\lambda ${ident i}. $p)}. + +notation "hvbox(a break ∈ b)" non associative with precedence 45 +for @{ 'mem $a $b }. + +notation "hvbox(a break ≬ b)" non associative with precedence 45 +for @{ 'overlaps $a $b }. (* \between *) + +notation "hvbox(a break ⊆ b)" non associative with precedence 45 +for @{ 'subseteq $a $b }. (* \subseteq *) + +notation "hvbox(a break ∩ b)" left associative with precedence 55 +for @{ 'intersects $a $b }. (* \cap *) + +notation "hvbox(a break ∪ b)" left associative with precedence 50 +for @{ 'union $a $b }. (* \cup *) + +notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}. + +notation "hvbox(a break \approx b)" non associative with precedence 45 + for @{ 'napart $a $b}. + +notation "hvbox(a break # b)" non associative with precedence 45 + for @{ 'apart $a $b}. + +notation "hvbox(a break \circ b)" + left associative with precedence 55 +for @{ 'compose $a $b }. + +notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }. +notation > "↓ a" with precedence 55 for @{ 'downarrow $a }. + +notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }. + +notation "↑a" with precedence 55 for @{ 'uparrow $a }. + +notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }. + +notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. +notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. +notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}. +notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }. +notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }. +notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}. + +notation "| term 19 C |" with precedence 70 for @{ 'card $C }. + +notation "\naturals" non associative with precedence 90 for @{'N}. +notation "\rationals" non associative with precedence 90 for @{'Q}. +notation "\reals" non associative with precedence 90 for @{'R}. +notation "\integers" non associative with precedence 90 for @{'Z}. +notation "\complexes" non associative with precedence 90 for @{'C}. + +notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *) + +notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}. +notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}. +notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}. +notation > "⊩ " with precedence 60 for @{'Vdash ?}. +notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}. + +notation < "maction (mstyle color #ff0000 (­…­)) (t)" +non associative with precedence 90 for @{'hide $t}. \ No newline at end of file diff --git a/weblib/basics/jmeq.ma b/weblib/basics/jmeq.ma new file mode 100644 index 000000000..ad3aa9371 --- /dev/null +++ b/weblib/basics/jmeq.ma @@ -0,0 +1,92 @@ +(* + ||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/logic.ma". + +inductive Sigma: Type[1] ≝ + mk_Sigma: ∀p1: Type[0]. p1 → Sigma. + +definition p1: Sigma → Type[0]. + #S cases S #Y #_ @Y +qed. + +definition p2: ∀S:Sigma. p1 S. + #S cases S #Y #x @x +qed. + +inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝ +jmrefl : jmeq A x A x. + +definition eqProp ≝ λA:Prop.eq A. + +lemma K : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x). +#A #x #h @(refl ? h: eqProp ? ? ?). +qed. + +definition cast: + ∀A,B:Type[0].∀E:A=B. A → B. + #A #B #E cases E #X @X +qed. + +lemma tech1: + ∀Aa,Bb:Sigma.∀E:Aa=Bb. + cast (p1 Aa) (p1 Bb) ? (p2 Aa) = p2 Bb. + [2: >E % + | #Aa #Bb #E >E cases Bb #B #b normalize % ] +qed. + +lemma gral: ∀A.∀x,y:A. + mk_Sigma A x = mk_Sigma A y → x=y. + #A #x #y #E lapply (tech1 ?? E) + generalize in ⊢ (??(???%?)? → ?) #E1 + normalize in E1; >(K ?? E1) normalize + #H @H +qed. + +axiom daemon: False. + +lemma jm_to_eq_sigma: + ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y. + #A #x #y #E cases E in ⊢ (???%); % +qed. + +definition curry: + ∀A,x. + (∀y. jmeq A x A y → Type[0]) → + (∀y. mk_Sigma A x = mk_Sigma A y → Type[0]). + #A #x #f #y #E @(f y) >(gral ??? E) % +qed. + +lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0]. + P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y. + P y h. + #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E; + @(match G + return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e + with + [refl ⇒ ?]) + #E <(sym_eq ??? (K ?? E)) @H +qed. + +definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0]. + #A #P #a @(P a) +qed. + +lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0]. + PP ? (P x) (jmrefl A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h. + #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E) + lapply (G ?? (curry ?? P) ?? F) + [ normalize // + | #H whd in H; @(H : PP ? (P b) ?) ] +qed. + +lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0]. + P x (jmrefl A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E. diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma new file mode 100644 index 000000000..798f57629 --- /dev/null +++ b/weblib/basics/list.ma @@ -0,0 +1,185 @@ +(* + ||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/types.ma". +include "arithmetics/nat.ma". + +inductive list (A:Type[0]) : Type[0] := + | nil: list A + | cons: A -> list A -> list A. + +notation "hvbox(hd break :: tl)" + right associative with precedence 47 + for @{'cons $hd $tl}. + +notation "[ list0 x sep ; ]" + non associative with precedence 90 + for ${fold right @'nil rec acc @{'cons $x $acc}}. + +notation "hvbox(l1 break @ l2)" + right associative with precedence 47 + for @{'append $l1 $l2 }. + +interpretation "nil" 'nil = (nil ?). +interpretation "cons" 'cons hd tl = (cons ? hd tl). + +definition not_nil: ∀A:Type[0].list A → Prop ≝ + λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ]. + +theorem nil_cons: + ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ []. + #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq // +qed. + +(* +let rec id_list A (l: list A) on l := + match l with + [ nil => [] + | (cons hd tl) => hd :: id_list A tl ]. *) + +let rec append A (l1: list A) l2 on l1 ≝ + match l1 with + [ nil ⇒ l2 + | cons hd tl ⇒ hd :: append A tl l2 ]. + +definition hd ≝ λA.λl: list A.λd:A. + match l with [ nil ⇒ d | cons a _ ⇒ a]. + +definition tail ≝ λA.λl: list A. + match l with [ nil ⇒ [] | cons hd tl ⇒ tl]. + +interpretation "append" 'append l1 l2 = (append ? l1 l2). + +theorem append_nil: ∀A.∀l:list A.l @ [] = l. +#A #l (elim l) normalize // qed. + +theorem associative_append: + ∀A.associative (list A) (append A). +#A #l1 #l2 #l3 (elim l1) normalize // qed. + +(* deleterio per auto +ntheorem cons_append_commute: + ∀A:Type.∀l1,l2:list A.∀a:A. + a :: (l1 @ l2) = (a :: l1) @ l2. +//; nqed. *) + +theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1. +/2/ qed. + +theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. + l1@l2=[] → P (nil A) (nil A) → P l1 l2. +#A #l1 #l2 #P (cases l1) normalize // +#a #l3 #heq destruct +qed. + +theorem nil_to_nil: ∀A.∀l1,l2:list A. + l1@l2 = [] → l1 = [] ∧ l2 = []. +#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/ +qed. + +(* iterators *) + +let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝ + match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)]. + +let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝ + match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)]. + +definition filter ≝ + λT.λp:T → bool. + foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T). + +lemma filter_true : ∀A,l,a,p. p a = true → + filter A p (a::l) = a :: filter A p l. +#A #l #a #p #pa (elim l) normalize >pa normalize // qed. + +lemma filter_false : ∀A,l,a,p. p a = false → + filter A p (a::l) = filter A p l. +#A #l #a #p #pa (elim l) normalize >pa normalize // qed. + +theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. +#A #B #f #g #l #eqfg (elim l) normalize // qed. + +let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝ +match l1 with + [ nil ⇒ nil ? + | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g + ]. + +(**************************** length ******************************) + +let rec length (A:Type[0]) (l:list A) on l ≝ + match l with + [ nil ⇒ 0 + | cons a tl ⇒ S (length A tl)]. + +notation "|M|" non associative with precedence 60 for @{'norm $M}. +interpretation "norm" 'norm l = (length ? l). + +let rec nth n (A:Type[0]) (l:list A) (d:A) ≝ + match n with + [O ⇒ hd A l d + |S m ⇒ nth m A (tail A l) d]. + +(**************************** fold *******************************) + +let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝ + match l with + [ nil ⇒ b + | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l)) + (fold A B op b p f l)]. + +notation "\fold [ op , nil ]_{ ident i ∈ l | p} f" + with precedence 80 +for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}. + +notation "\fold [ op , nil ]_{ident i ∈ l } f" + with precedence 80 +for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}. + +interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l). + +theorem fold_true: +∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → + \fold[op,nil]_{i ∈ a::l| p i} (f i) = + op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). +#A #B #a #l #p #op #nil #f #pa normalize >pa // qed. + +theorem fold_false: +∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f. +p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = + \fold[op,nil]_{i ∈ l| p i} (f i). +#A #B #a #l #p #op #nil #f #pa normalize >pa // qed. + +theorem fold_filter: +∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B. + \fold[op,nil]_{i ∈ l| p i} (f i) = + \fold[op,nil]_{i ∈ (filter A p l)} (f i). +#A #B #a #l #p #op #nil #f elim l // +#a #tl #Hind cases(true_or_false (p a)) #pa + [ >filter_true // > fold_true // >fold_true // + | >filter_false // >fold_false // ] +qed. + +record Aop (A:Type[0]) (nil:A) : Type[0] ≝ + {op :2> A → A → A; + nill:∀a. op nil a = a; + nilr:∀a. op a nil = a; + assoc: ∀a,b,c.op a (op b c) = op (op a b) c + }. + +theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f. + op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) = + \fold[op,nil]_{i∈(I@J)} (f i). +#A #B #I #J #nil #op #f (elim I) normalize + [>nill //|#a #tl #Hind eq ? x a.∀P: + ∀x:A. x = a → Type[2]. P a (refl A a) → P x p. + #A #a #x #p (cases p) // qed. + +lemma eq_ind_r : + ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → + ∀x.∀p:eq ? x a.P x p. + #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed. + +lemma eq_rect_Type2_r: + ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → + ∀x.∀p:eq ? x a.P x p. + #A #a #P #H #x #p (generalize in match H) (generalize in match P) + cases p; //; qed. + +theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x = y → P y. +#A #x #P #Hx #y #Heq (cases Heq); //; qed. + +theorem sym_eq: ∀A.∀x,y:A. x = y → y = x. +#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed. + +theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y = x → P y. +#A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed. + +theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B. +#A #B #Ha #Heq (elim Heq); //; qed. + +theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z. +#A #x #y #z #H1 #H2 >H1; //; qed. + +theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y. +#A #B #f #x #y #H >H; //; qed. + +(* deleterio per auto? *) +theorem eq_f2: ∀A,B,C.∀f:A→B→C. +∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2. +#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. + +(* hint to genereric equality +definition eq_equality: equality ≝ + mk_equality eq refl rewrite_l rewrite_r. + + +unification hint 0 ≔ T,a,b; + X ≟ eq_equality +(*------------------------------------*) ⊢ + equal X T a b ≡ eq T a b. +*) + +(********** connectives ********) + +inductive True: Prop ≝ +I : True. + +inductive False: Prop ≝ . + +(* ndefinition Not: Prop → Prop ≝ +λA. A → False. *) + +inductive Not (A:Prop): Prop ≝ +nmk: (A → False) → Not A. + + +interpretation "logical not" 'not x = (Not x). + +theorem absurd : ∀A:Prop. A → ¬A → False. +#A #H #Hn (elim Hn); /2/; qed. + +(* +ntheorem absurd : ∀ A,C:Prop. A → ¬A → C. +#A; #C; #H; #Hn; nelim (Hn H). +nqed. *) + +theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A. +/4/; qed. + +(* inequality *) +interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). + +theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x. +/3/; qed. + +(* and *) +inductive And (A,B:Prop) : Prop ≝ + conj : A → B → And A B. + +interpretation "logical and" 'and x y = (And x y). + +theorem proj1: ∀A,B:Prop. A ∧ B → A. +#A #B #AB (elim AB) //; qed. + +theorem proj2: ∀ A,B:Prop. A ∧ B → B. +#A #B #AB (elim AB) //; qed. + +(* or *) +inductive Or (A,B:Prop) : Prop ≝ + or_introl : A → (Or A B) + | or_intror : B → (Or A B). + +interpretation "logical or" 'or x y = (Or x y). + +definition decidable : Prop → Prop ≝ +λ A:Prop. A ∨ ¬ A. + +(* exists *) +inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝ + ex_intro: ∀ x:A. P x → ex A P. + +interpretation "exists" 'exists x = (ex ? x). + +inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝ + ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q. + +(* iff *) +definition iff := + λ A,B. (A → B) ∧ (B → A). + +interpretation "iff" 'iff a b = (iff a b). + +(* cose per destruct: da rivedere *) + +definition R0 ≝ λT:Type[0].λt:T.t. + +definition R1 ≝ eq_rect_Type0. + +(* useless stuff *) +definition R2 : + ∀T0:Type[0]. + ∀a0:T0. + ∀T1:∀x0:T0. a0=x0 → Type[0]. + ∀a1:T1 a0 (refl ? a0). + ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0]. + ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1). + ∀b0:T0. + ∀e0:a0 = b0. + ∀b1: T1 b0 e0. + ∀e1:R1 ?? T1 a1 ? e0 = b1. + T2 b0 e0 b1 e1. +#T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1 +@(eq_rect_Type0 ????? e1) +@(R1 ?? ? ?? e0) +@a2 +qed. + +definition R3 : + ∀T0:Type[0]. + ∀a0:T0. + ∀T1:∀x0:T0. a0=x0 → Type[0]. + ∀a1:T1 a0 (refl ? a0). + ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0]. + ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1). + ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1. + ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0]. + ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2). + ∀b0:T0. + ∀e0:a0 = b0. + ∀b1: T1 b0 e0. + ∀e1:R1 ?? T1 a1 ? e0 = b1. + ∀b2: T2 b0 e0 b1 e1. + ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2. + T3 b0 e0 b1 e1 b2 e2. +#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2 +@(eq_rect_Type0 ????? e2) +@(R2 ?? ? ???? e0 ? e1) +@a3 +qed. + +definition R4 : + ∀T0:Type[0]. + ∀a0:T0. + ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0]. + ∀a1:T1 a0 (refl T0 a0). + ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0]. + ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1). + ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1. + ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0]. + ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) + a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2). + ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1. + ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2. + ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. + Type[0]. + ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) + a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2) + a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) + a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)) + a3). + ∀b0:T0. + ∀e0:eq (T0 …) a0 b0. + ∀b1: T1 b0 e0. + ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1. + ∀b2: T2 b0 e0 b1 e1. + ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2. + ∀b3: T3 b0 e0 b1 e1 b2 e2. + ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3. + T4 b0 e0 b1 e1 b2 e2 b3 e3. +#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3 +@(eq_rect_Type0 ????? e3) +@(R3 ????????? e0 ? e1 ? e2) +@a4 +qed. + +(* TODO concrete definition by means of proof irrelevance *) +axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. \ No newline at end of file diff --git a/weblib/basics/pts.ma b/weblib/basics/pts.ma new file mode 100644 index 000000000..1b87a2d0b --- /dev/null +++ b/weblib/basics/pts.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basics/core_notation.ma". + +universe constraint Type[0] < Type[1]. +universe constraint Type[1] < Type[2]. +universe constraint Type[2] < Type[3]. +universe constraint Type[3] < Type[4]. + +(*inductive True : Prop ≝ I : True. + +(*lemma fa : ∀X:Prop.X → X. +#X #p // +qed. + +(* check fa*) + +lemma ggr ≝ fa.*) + +inductive False : Prop ≝ . + +inductive bool : Prop ≝ True : bool | false : bool. + +inductive eq (A:Type[1]) (x:A) : A → Prop ≝ + refl: eq A x x. + +lemma provable_True : True → eq Prop True True. +#H % +qed.*) \ No newline at end of file diff --git a/weblib/basics/relations.ma b/weblib/basics/relations.ma new file mode 100644 index 000000000..b31db23d7 --- /dev/null +++ b/weblib/basics/relations.ma @@ -0,0 +1,106 @@ +(* + ||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/logic.ma". + +(********** relations **********) +definition relation : Type[0] → Type[0] +≝ λA.A→A→Prop. + +definition reflexive: ∀A.∀R :relation A.Prop +≝ λA.λR.∀x:A.R x x. + +definition symmetric: ∀A.∀R: relation A.Prop +≝ λA.λR.∀x,y:A.R x y → R y x. + +definition transitive: ∀A.∀R:relation A.Prop +≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z. + +definition irreflexive: ∀A.∀R:relation A.Prop +≝ λA.λR.∀x:A.¬(R x x). + +definition cotransitive: ∀A.∀R:relation A.Prop +≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y. + +definition tight_apart: ∀A.∀eq,ap:relation A.Prop +≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧ +(eq x y → ¬(ap x y)). + +definition antisymmetric: ∀A.∀R:relation A.Prop +≝ λA.λR.∀x,y:A. R x y → ¬(R y x). + +(********** functions **********) + +definition compose ≝ + λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x). + +interpretation "function composition" 'compose f g = (compose ? ? ? f g). + +definition injective: ∀A,B:Type[0].∀ f:A→B.Prop +≝ λA,B.λf.∀x,y:A.f x = f y → x=y. + +definition surjective: ∀A,B:Type[0].∀f:A→B.Prop +≝λA,B.λf.∀z:B.∃x:A.z = f x. + +definition commutative: ∀A:Type[0].∀f:A→A→A.Prop +≝ λA.λf.∀x,y.f x y = f y x. + +definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop +≝ λA,B.λf.∀x,y.f x y = f y x. + +definition associative: ∀A:Type[0].∀f:A→A→A.Prop +≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z). + +(* functions and relations *) +definition monotonic : ∀A:Type[0].∀R:A→A→Prop. +∀f:A→A.Prop ≝ +λA.λR.λf.∀x,y:A.R x y → R (f x) (f y). + +(* functions and functions *) +definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop +≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z). + +definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop +≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z). + +lemma injective_compose : ∀A,B,C,f,g. +injective A B f → injective B C g → injective A C (λx.g (f x)). +/3/; qed. + +(* extensional equality *) + +definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ +λA.λP,Q.∀a.iff (P a) (Q a). + +definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝ +λA,B.λR,S.∀a.∀b.iff (R a b) (S a b). + +definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝ +λA,B.λf,g.∀a.f a = g a. + +notation " x \eqP y " non associative with precedence 45 +for @{'eqP A $x $y}. + +interpretation "functional extentional equality" +'eqP A x y = (exteqP A x y). + +notation "x \eqR y" non associative with precedence 45 +for @{'eqR ? ? x y}. + +interpretation "functional extentional equality" +'eqR A B R S = (exteqR A B R S). + +notation " f \eqF g " non associative with precedence 45 +for @{'eqF ? ? f g}. + +interpretation "functional extentional equality" +'eqF A B f g = (exteqF A B f g). + diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma new file mode 100644 index 000000000..c14cc60b4 --- /dev/null +++ b/weblib/basics/types.ma @@ -0,0 +1,59 @@ +(* + ||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/logic.ma". + +(* void *) +inductive void : Type[0] ≝. + +(* unit *) +inductive unit : Type[0] ≝ it: unit. + +(* Prod *) +inductive Prod (A,B:Type[0]) : Type[0] ≝ +pair : A → B → Prod A B. + +interpretation "Pair construction" 'pair x y = (pair ? ? x y). + +interpretation "Product" 'product x y = (Prod x y). + +definition fst ≝ λA,B.λp:A × B. + match p with [pair a b ⇒ a]. + +definition snd ≝ λA,B.λp:A × B. + match p with [pair a b ⇒ b]. + +interpretation "pair pi1" 'pi1 = (fst ? ?). +interpretation "pair pi2" 'pi2 = (snd ? ?). +interpretation "pair pi1" 'pi1a x = (fst ? ? x). +interpretation "pair pi2" 'pi2a x = (snd ? ? x). +interpretation "pair pi1" 'pi1b x y = (fst ? ? x y). +interpretation "pair pi2" 'pi2b x y = (snd ? ? x y). + +theorem eq_pair_fst_snd: ∀A,B.∀p:A × B. + p = 〈 \fst p, \snd p 〉. +#A #B #p (cases p) // qed. + +(* sum *) +inductive Sum (A,B:Type[0]) : Type[0] ≝ + inl : A → Sum A B +| inr : B → Sum A B. + +interpretation "Disjoint union" 'plus A B = (Sum A B). + +(* option *) +inductive option (A:Type[0]) : Type[0] ≝ + None : option A + | Some : A → option A. + +(* sigma *) +inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ + dp: ∀a:A.(f a)→Sig A f. \ No newline at end of file diff --git a/weblib/hints_declaration.ma b/weblib/hints_declaration.ma new file mode 100644 index 000000000..d04f453f2 --- /dev/null +++ b/weblib/hints_declaration.ma @@ -0,0 +1,107 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* + +Notation for hint declaration +============================== + +The idea is to write a context, with abstraction first, then +recursive calls (let-in) and finally the two equivalent terms. +The context can be empty. Note the ; to begin the second part of +the context (necessary even if the first part is empty). + + unification hint PREC \coloneq + ID : TY, ..., ID : TY + ; ID \equest T, ..., ID \equest T + \vdash T1 \equiv T2 + +With unidoce and some ASCII art it looks like the following: + + unification hint PREC ≔ ID : TY, ..., ID : TY; + ID ≟ T, ..., ID ≟ T + (*---------------------*) ⊢ + T1 ≡ T2 + +The order of premises is relevant, since they are processed in order +(left to right). + +*) + +(* it seems unbelivable, but it works! *) +notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 19 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py" + with precedence 90 + for @{ ${ fold right + @{ ${ default + @{ ${ fold right + @{ 'hint_decl $Px $Py } + rec acc1 @{ let ( ${ident U} : ?) ≝ $V in $acc1} } } + @{ 'hint_decl $Px $Py } + } + } + rec acc @{ + ${ fold right @{ $acc } rec acc2 + @{ ∀${ident x}:${ default @{ $T } @{ ? } }.$acc2 } } + } + }}. + +include "basics/pts.ma". + +definition hint_declaration_Type0 ≝ λA:Type[0] .λa,b:A.Prop. +definition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.Prop. +definition hint_declaration_Type2 ≝ λa,b:Type[2].Prop. +definition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop. +definition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop. +definition hint_declaration_CProp2 ≝ λa,b:CProp[2].Prop. + +interpretation "hint_decl_Type2" 'hint_decl a b = (hint_declaration_Type2 a b). +interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b). +interpretation "hint_decl_Type1" 'hint_decl a b = (hint_declaration_Type1 ? a b). +interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b). +interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b). +interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b). + +(* Non uniform coercions support +record solution2 (S : Type[2]) (s : S) : Type[3] ≝ { + target2 : Type[2]; + result2 : target2 +}. + +record solution1 (S : Type[1]) (s : S) : Type[2] ≝ { + target1 : Type[1]; + result1 : target1 +}. + +coercion nonunifcoerc1 : ∀S:Type[1].∀s:S.∀l:solution1 S s. target1 S s l ≝ result1 + on s : ? to target1 ???. + +coercion nonunifcoerc2 : ∀S:Type[2].∀s:S.∀l:solution2 S s. target2 S s l ≝ result2 + on s : ? to target2 ???. +*) + +(* Example of a non uniform coercion declaration + + Type[0] setoid + >---> + MR R + + provided MR = carr R + +unification hint 0 ≔ R : setoid; + MR ≟ carr R, + sol ≟ mk_solution1 Type[0] MR setoid R +(* ---------------------------------------- *) ⊢ + setoid ≡ target1 ? MR sol. + +*) \ No newline at end of file diff --git a/weblib/lambda/subst.ma b/weblib/lambda/subst.ma new file mode 100644 index 000000000..bd8c5b713 --- /dev/null +++ b/weblib/lambda/subst.ma @@ -0,0 +1,230 @@ +(* + ||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". + +inductive T : Type[0] ≝ + | Sort: nat → T (* starts from 0 *) + | Rel: nat → T (* starts from ... ? *) + | App: T → T → T (* function, argument *) + | Lambda: T → T → T (* type, body *) + | Prod: T → T → T (* type, body *) + | D: T → T (* dummifier *) +. + +(* arguments: k is the depth (starts from 0), p is the height (starts from 0) *) +let rec lift t k p ≝ + match t with + [ Sort n ⇒ Sort n + | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p)) + | App m n ⇒ App (lift m k p) (lift n k p) + | Lambda m n ⇒ Lambda (lift m k p) (lift n (k+1) p) + | Prod m n ⇒ Prod (lift m k p) (lift n (k+1) p) + | D n ⇒ D (lift n k p) + ]. + +(* +ndefinition lift ≝ λt.λp.lift_aux t 0 p. + +notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift O $M}. +notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}. +*) +(* interpretation "Lift" 'Lift n M = (lift M n). *) +interpretation "Lift" 'Lift n k M = (lift M k n). + +let rec subst t k a ≝ + match t with + [ Sort n ⇒ Sort n + | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) + (if_then_else T (eqb n k) (lift a 0 n) (Rel (n-1))) + | App m n ⇒ App (subst m k a) (subst n k a) + | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a) + | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a) + | D n ⇒ D (subst n k a) + ]. + +(* meglio non definire +ndefinition subst ≝ λa.λt.subst_aux t 0 a. +notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}. +*) + +notation "M [ k := N ]" non associative with precedence 90 for @{'Subst $M $k $N}. + +(* interpretation "Subst" 'Subst N M = (subst N M). *) +interpretation "Subst" 'Subst M k N = (subst M k N). + +(*** properties of lift and subst ***) + +lemma lift_0: ∀t:T.∀k. lift t k 0 = t. +#t (elim t) normalize // #n #k cases (leb (S n) k) normalize // +qed. + +(* nlemma lift_0: ∀t:T. lift t 0 = t. +#t; nelim t; nnormalize; //; nqed. *) + +lemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i. +// qed. + +lemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n). +// qed. + +lemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i). +#i (change with (lift (Rel i) 0 1 = Rel (1 + i))) // +qed. + +lemma lift_lift: ∀t.∀i,j.j ≤ i → ∀h,k. + lift (lift t k i) (j+k) h = lift t k (i+h). +#t #i #j #h (elim t) normalize // #n #h #k +@(leb_elim (S n) k) #Hnk normalize + [>(le_to_leb_true (S n) (j+k) ?) normalize /2/ + |>(lt_to_leb_false (S n+i) (j+k) ?) + normalize // @le_S_S >(commutative_plus j k) + @le_plus // @not_lt_to_le /2/ + ] +qed. + +lemma lift_lift1: ∀t.∀i,j,k. + lift(lift t k j) k i = lift t k (j+i). +/2/ qed. + +lemma lift_lift2: ∀t.∀i,j,k. + lift (lift t k j) (j+k) i = lift t k (j+i). +/2/ qed. + +(* +nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i). +nnormalize; //; nqed. *) + +lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B. +#A #B (elim B) normalize /2/ #n #k +@(leb_elim (S n) k) normalize #Hnk + [>(le_to_leb_true ?? Hnk) normalize // + |>(lt_to_leb_false (S (n + 1)) k ?) normalize + [>(not_eq_to_eqb_false (n+1) k ?) normalize /2/ + |@le_S (applyS (not_le_to_lt (S n) k Hnk)) + ] + ] +qed. + +(* +nlemma subst_lift: ∀A,B. subst A (lift B 1) = B. +nnormalize; //; nqed. *) + +lemma subst_sort: ∀A.∀n,k.(Sort n) [k ≝ A] = Sort n. +// qed. + +lemma subst_rel: ∀A.(Rel 0) [0 ≝ A] = A. +normalize // qed. + +lemma subst_rel1: ∀A.∀k,i. i < k → + (Rel i) [k ≝ A] = Rel i. +#A #k #i normalize #ltik >(le_to_leb_true (S i) k) // +qed. + +lemma subst_rel2: ∀A.∀k. + (Rel k) [k ≝ A] = lift A 0 k. +#A #k normalize >(lt_to_leb_false (S k) k) // >(eq_to_eqb_true … (refl …)) // +qed. + +lemma subst_rel3: ∀A.∀k,i. k < i → + (Rel i) [k ≝ A] = Rel (i-1). +#A #k #i normalize #ltik >(lt_to_leb_false (S i) k) /2/ +>(not_eq_to_eqb_false i k) // @sym_not_eq @lt_to_not_eq // +qed. + +lemma lift_subst_ijk: ∀A,B.∀i,j,k. + lift (B [j+k := A]) k i = (lift B k i) [j+k+i ≝ A]. +#A #B #i #j (elim B) normalize /2/ #n #k +@(leb_elim (S n) (j + k)) normalize #Hnjk + [(elim (leb (S n) k)) + [>(subst_rel1 A (j+k+i) n) /2/ + |>(subst_rel1 A (j+k+i) (n+i)) /2/ + ] + |@(eqb_elim n (j+k)) normalize #Heqnjk + [>(lt_to_leb_false (S n) k); + [(cut (j+k+i = n+i)) [//] #Heq + >Heq >(subst_rel2 A ?) normalize (applyS lift_lift) // + |/2/ + ] + |(cut (j + k < n)) + [@not_eq_to_le_to_lt; + [/2/ |@le_S_S_to_le @not_le_to_lt /2/ ] + |#ltjkn + (cut (O < n)) [/2/] #posn (cut (k ≤ n)) [/2/] #lekn + >(lt_to_leb_false (S (n-1)) k) normalize + [>(lt_to_leb_false … (le_S_S … lekn)) + >(subst_rel3 A (j+k+i) (n+i)); [/3/ |/2/] + |@le_S_S; (* /3/; 65 *) (applyS monotonic_pred) @le_plus_b // + ] + ] + ] +qed. + +theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → + (lift B i (S k)) [j ≝ A] = lift B i k. +#A #B (elim B) normalize /2/ + [2,3,4: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk + @eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) // + |5:#T #Hind #i #j #k #leij #lejk @eq_f @Hind // + |#n #i #j #k #leij #ltjk @(leb_elim (S n) i) normalize #len + [>(le_to_leb_true (S n) j) /2/ + |>(lt_to_leb_false (S (n+S k)) j); + [normalize >(not_eq_to_eqb_false (n+S k) j)normalize + /2/ @(not_to_not …len) #H @(le_plus_to_le_r k) normalize // + |@le_S_S @(transitive_le … ltjk) @le_plus // @not_lt_to_le /2/ + ] + ] + ] +qed. + +(********************* substitution lemma ***********************) + +lemma subst_lemma: ∀A,B,C.∀k,i. + (A [i ≝ B]) [k+i ≝ C] = + (A [S (k+i) := C]) [i ≝ B [k ≝ C]]. +#A #B #C #k (elim A) normalize // (* WOW *) +#n #i @(leb_elim (S n) i) #Hle + [(cut (n < k+i)) [/2/] #ltn (* lento *) (cut (n ≤ k+i)) [/2/] #len + >(subst_rel1 C (k+i) n ltn) >(le_to_leb_true n (k+i) len) >(subst_rel1 … Hle) // + |@(eqb_elim n i) #eqni + [>eqni >(le_to_leb_true i (k+i)) // >(subst_rel2 …); + normalize @sym_eq (applyS (lift_subst_ijk C B i k O)) + |@(leb_elim (S (n-1)) (k+i)) #nk + [>(subst_rel1 C (k+i) (n-1) nk) >(le_to_leb_true n (k+i)); + [>(subst_rel3 ? i n) // @not_eq_to_le_to_lt; + [/2/ |@not_lt_to_le /2/] + |@(transitive_le … nk) // + ] + |(cut (i < n)) [@not_eq_to_le_to_lt; [/2/] @(not_lt_to_le … Hle)] + #ltin (cut (O < n)) [/2/] #posn + @(eqb_elim (n-1) (k+i)) #H + [>H >(subst_rel2 C (k+i)) >(lt_to_leb_false n (k+i)); + [>(eq_to_eqb_true n (S(k+i))); + [normalize |delift normalize /2/ + |(lt_to_leb_false n (k+i)); + [>(not_eq_to_eqb_false n (S(k+i))); + [>(subst_rel3 C (k+i) (n-1) Hlt); + >(subst_rel3 ? i (n-1)) // @(le_to_lt_to_lt … Hlt) // + |@(not_to_not … H) #Hn >Hn normalize // + ] + |@(transitive_lt … Hlt) @(lt_O_n_elim … posn) normalize // + ] + ] + ] + ] + ] +qed. diff --git a/weblib/lambda/types.ma b/weblib/lambda/types.ma new file mode 100644 index 000000000..543b3b7b9 --- /dev/null +++ b/weblib/lambda/types.ma @@ -0,0 +1,214 @@ +(* + ||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 "lambda/subst.ma". +include "basics/list.ma". + + +(*************************** substl *****************************) + +let rec substl (G:list T) (N:T) : list T ≝ + match G with + [ nil ⇒ nil T + | cons A D ⇒ ((subst A (length T D) N)::(substl D N)) + ]. + +(* +nlemma substl_cons: ∀A,N.∀G. +substl (A::G) N = (subst_aux A (length T G) N)::(substl G N). +//; nqed. +*) + +(* +nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1. +/2/; nqed.*) + +(****************************************************************) + +axiom A: nat → nat → Prop. +axiom R: nat → nat → nat → Prop. +axiom conv: T → T → Prop. + +inductive TJ: list T → T → T → Prop ≝ + | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j) + | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1) + | weak: ∀G.∀A,B,C.∀i. + TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1) + | prod: ∀G.∀A,B.∀i,j,k. R i j k → + TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k) + | app: ∀G.∀F,A,B,a. + TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 a) + | abs: ∀G.∀A,B,b.∀i. + TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B) + | conv: ∀G.∀A,B,C.∀i. conv B C → + TJ G A B → TJ G B (Sort i) → TJ G A C + | dummy: ∀G.∀A,B.∀i. + TJ G A B → TJ G B (Sort i) → TJ G (D A) B. + +notation "hvbox(G break ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}. +interpretation "type judgement" 'TJ G A B = (TJ G A B). + +(* ninverter TJ_inv2 for TJ (%?%) : Prop. *) + +(**** definitions ****) + +inductive Glegal (G: list T) : Prop ≝ +glegalk : ∀A,B. G ⊢ A : B → Glegal G. + +inductive Gterm (G: list T) (A:T) : Prop ≝ + | is_term: ∀B.G ⊢ A:B → Gterm G A + | is_type: ∀B.G ⊢ B:A → Gterm G A. + +inductive Gtype (G: list T) (A:T) : Prop ≝ +gtypek: ∀i.G ⊢ A : Sort i → Gtype G A. + +inductive Gelement (G:list T) (A:T) : Prop ≝ +gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A. + +inductive Tlegal (A:T) : Prop ≝ +tlegalk: ∀G. Gterm G A → Tlegal A. + +(* +ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B . + +ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A. + +ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i). + +ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B. + +ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A. +*) + +(* +ntheorem free_var1: ∀G.∀A,B,C. TJ G A B → +subst C A +#G; #i; #j; #axij; #Gleg; ncases Gleg; +#A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed. +*) + +theorem start_lemma1: ∀G.∀i,j. +A i j → Glegal G → G ⊢ Sort i: Sort j. +#G #i #j #axij #Gleg (cases Gleg) +#A #B #tjAB (elim tjAB) /2/ +(* bello *) qed. + +theorem start_rel: ∀G.∀A.∀C.∀n,i,q. +G ⊢ C: Sort q → G ⊢ Rel n: lift A 0 i → (C::G) ⊢ Rel (S n): lift A 0 (S i). +#G #A #C #n #i #p #tjC #tjn + (applyS (weak G (Rel n))) //. (* bello *) + (* + nrewrite > (plus_n_O i); + nrewrite > (plus_n_Sm i O); + nrewrite < (lift_lift A 1 i); + nrewrite > (plus_n_O n); nrewrite > (plus_n_Sm n O); + applyS (weak G (Rel n) (lift A i) C p tjn tjC). *) +qed. + +theorem start_lemma2: ∀G. +Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n). +#G #Gleg (cases Gleg) #A #B #tjAB (elim tjAB) /2/ + [#i #j #axij #p normalize #abs @False_ind @(absurd … abs) // + |#G #A #i #tjA #Hind #m (cases m) /2/ + #p #Hle @start_rel // @Hind @le_S_S_to_le @Hle + |#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m) + /2/ #p #Hle @start_rel // @Hind1 @le_S_S_to_le @Hle + ] +qed. + +(* +nlet rec TJm G D on D : Prop ≝ + match D with + [ nil ⇒ True + | cons A D1 ⇒ TJ G (Rel 0) A ∧ TJm G D1 + ]. + +nlemma tjm1: ∀G,D.∀A. TJm G (A::D) → TJ G (Rel 0) A. +#G; #D; #A; *; //; nqed. + +ntheorem transitivity_tj: ∀D.∀A,B. TJ D A B → + ∀G. Glegal G → TJm G D → TJ G A B. +#D; #A; #B; #tjAB; nelim tjAB; + ##[/2/; + ##|/2/; + ##|#E; #T; #T0; #T1; #n; #tjT; #tjT1; #H; #H1; #G; #HlegG; + #tjGcons; + napply weak; +*) +(* +ntheorem substitution_tj: +∀G.∀A,B,N,M.TJ (A::G) M B → TJ G N A → + TJ G (subst N M) (subst N B). +#G;#A;#B;#N;#M;#tjM; + napply (TJ_inv2 (A::G) M B); + ##[nnormalize; /3/; + ##|#G; #A; #N; #tjA; #Hind; #Heq; + ndestruct;//; + ##|#G; #A; #B; #C; #n; #tjA; #tjC; #Hind1; #Hind2; #Heq; + ndestruct;//; + ##|nnormalize; #E; #A; #B; #i; #j; #k; + #Ax; #tjA; #tjB; #Hind1; #_; + #Heq; #HeqB; #tjN; napply (prod ?????? Ax); + ##[/2/; + ##|nnormalize; napplyS weak; + +*) + + +axiom conv_subst: ∀P,Q,N,i.conv P Q → conv P[i := N] Q[i := N]. + +theorem substitution_tj: +∀E.∀A,B,M. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A → + ((substl D N)@G) ⊢ M[|D| := N]: B[|D| := N]. +#E #A #B #M #tjMB (elim tjMB) + [normalize #i #j #k #G #D #N (cases D) + [normalize #isnil destruct + |#P #L normalize #isnil destruct + ] + |#G #A1 #i #tjA #Hind #G1 #D (cases D) + [#N #Heq #tjN >(delift (lift N O O) A1 O O O ??) // + (normalize in Heq) destruct /2/ + |#H #L #N1 #Heq (normalize in Heq) + #tjN1 normalize destruct; (applyS start) /2/ + ] + |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #N + (cases D) normalize + [#Heq destruct #tjN // + |#H #L #Heq #tjN1 destruct; + (* napplyS weak non va *) + (cut (S (length T L) = (length T L)+0+1)) [//] + #Hee (applyS weak) /2/ + ] + |#G #P #Q #i #j #k #Ax #tjP #tjQ #Hind1 #Hind2 + #G1 #D #N #Heq #tjN normalize @(prod … Ax); + [/2/ + |(cut (S (length T D) = (length T D)+1)) [//] + #Heq1 (plus_n_O (length ? D)) in ⊢ (? ? ? (? ? % ?)) + >(subst_lemma R S N ? 0) (applyS app) /2/ + |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2 + #G1 #D #N #Heq #tjN normalize + (applyS abs) + [normalize in Hind2 /2/ + |(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *) + generalize in match (Hind1 G1 (P::D) N ? tjN); + [#H (normalize in H) (applyS H) | normalize // ] + ] + |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2 + #G1 #D #N #Heq #tjN + @(conv …(conv_subst … convQR) ? (Hind2 …)) // @Hind1 // + |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2 + #G1 #D #N #Heq #tjN @dummy /2/ + ] +qed. diff --git a/weblib/root b/weblib/root new file mode 100644 index 000000000..c57405b94 --- /dev/null +++ b/weblib/root @@ -0,0 +1 @@ +baseuri=cic:/matita/ -- 2.39.2