From 53452958508001e7af3090695b619fe92135fb9e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 16 Dec 2010 11:54:35 +0000 Subject: [PATCH] New version of the library. Several files still do not compile. --- matita/matita/lib/arithmetics/bigops.ma | 2 +- matita/matita/lib/arithmetics/binomial.ma | 245 ++++++++ matita/matita/lib/arithmetics/congruence.ma | 118 ++++ matita/matita/lib/arithmetics/div_and_mod.ma | 5 +- matita/matita/lib/arithmetics/exp.ma | 9 +- matita/matita/lib/arithmetics/gcd.ma | 406 ++++++++++++++ matita/matita/lib/arithmetics/log.ma | 474 ++++++++++++++++ matita/matita/lib/arithmetics/minimization.ma | 4 +- matita/matita/lib/arithmetics/nat.ma | 92 ++- matita/matita/lib/arithmetics/nth_prime.ma | 201 +++++++ matita/matita/lib/arithmetics/primes.ma | 530 ++++++++++++++++++ matita/matita/lib/basics/bool.ma | 76 +++ matita/matita/lib/basics/core_notation.ma | 287 ++++++++++ matita/matita/lib/basics/jmeq.ma | 92 +++ matita/matita/lib/basics/list.ma | 170 ++++++ matita/matita/lib/basics/list2.ma | 30 + matita/matita/lib/basics/logic.ma | 221 ++++++++ matita/matita/lib/basics/pts.ma | 20 + matita/matita/lib/basics/relations.ma | 106 ++++ matita/matita/lib/basics/types.ma | 59 ++ matita/matita/lib/hints_declaration.ma | 107 ++++ matita/matita/lib/root | 1 + 22 files changed, 3194 insertions(+), 61 deletions(-) create mode 100644 matita/matita/lib/arithmetics/binomial.ma create mode 100644 matita/matita/lib/arithmetics/congruence.ma create mode 100644 matita/matita/lib/arithmetics/gcd.ma create mode 100644 matita/matita/lib/arithmetics/log.ma create mode 100644 matita/matita/lib/arithmetics/nth_prime.ma create mode 100644 matita/matita/lib/arithmetics/primes.ma create mode 100644 matita/matita/lib/basics/bool.ma create mode 100644 matita/matita/lib/basics/core_notation.ma create mode 100644 matita/matita/lib/basics/jmeq.ma create mode 100644 matita/matita/lib/basics/list.ma create mode 100644 matita/matita/lib/basics/list2.ma create mode 100644 matita/matita/lib/basics/logic.ma create mode 100644 matita/matita/lib/basics/pts.ma create mode 100644 matita/matita/lib/basics/relations.ma create mode 100644 matita/matita/lib/basics/types.ma create mode 100644 matita/matita/lib/hints_declaration.ma create mode 100644 matita/matita/lib/root diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma index 69a9ff20b..3211814db 100644 --- a/matita/matita/lib/arithmetics/bigops.ma +++ b/matita/matita/lib/arithmetics/bigops.ma @@ -265,7 +265,7 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2. ] qed. -(* Sigma e Pi - da generalizzare *) +(* Sigma e Pi *) notation "Σ_{ ident i < n | p } f" with precedence 80 for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}. diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma new file mode 100644 index 000000000..414b71a15 --- /dev/null +++ b/matita/matita/lib/arithmetics/binomial.ma @@ -0,0 +1,245 @@ +(* + ||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". +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 [>commutative_times //|@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 generalize in match H1;cases k + [intro;simplify in ⊢ (? (? ? (? %)) ?);simplify in ⊢ (? (? % ?) ?); + rewrite > sym_times;rewrite < times_n_SO;apply reflexive_divides + |intro;elim (decidable_eq_nat n2 n1) + [rewrite > H3;rewrite < minus_n_n; + rewrite > times_n_SO in ⊢ (? ? %);apply reflexive_divides + |lapply (H n2) + [lapply (H (n1 - (S n2))) + [change in ⊢ (? ? %) with ((S n1)*n1!); + rewrite > (plus_minus_m_m n1 n2) in ⊢ (? ? (? (? %) ?)) + [rewrite > sym_plus; + change in ⊢ (? ? (? % ?)) with ((S n2) + (n1 - n2)); + rewrite > sym_times in \vdash (? ? %); + rewrite > distr_times_plus in ⊢ (? ? %); + simplify in ⊢ (? (? ? (? %)) ?); + apply divides_plus + [rewrite > sym_times; + change in ⊢ (? (? ? %) ?) with ((S n2)*n2!); + rewrite > sym_times in ⊢ (? (? ? %) ?); + rewrite < assoc_times; + apply divides_times + [rewrite > sym_times;assumption + |apply reflexive_divides] + |rewrite < fact_minus in ⊢ (? (? ? %) ?) + [rewrite > sym_times in ⊢ (? (? ? %) ?); + rewrite < assoc_times; + apply divides_times + [rewrite < eq_plus_minus_minus_minus in Hletin1; + [rewrite > sym_times;rewrite < minus_n_n in Hletin1; + rewrite < plus_n_O in Hletin1;assumption + |lapply (le_S_S_to_le ? ? H2); + elim (le_to_or_lt_eq ? ? Hletin2); + [assumption + |elim (H3 H4)] + |constructor 1] + |apply reflexive_divides] + |lapply (le_S_S_to_le ? ? H2); + elim (le_to_or_lt_eq ? ? Hletin2); + [assumption + |elim (H3 H4)]]] + |apply le_S_S_to_le;assumption] + |apply le_minus_m;apply le_S_S_to_le;assumption] + |apply le_S_S_to_le;assumption]]]] +qed. + +theorem bc1: \forall n.\forall k. k < n \to bc (S n) (S k) = (bc n k) + (bc n (S k)). +intros.unfold bc. +rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?)) + [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)). + rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)). + rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %)) + [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))). + rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))). + rewrite > fact_minus + [rewrite < eq_div_plus + [rewrite < distr_times_plus. + simplify in ⊢ (? ? ? (? (? ? %) ?)). + rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)). + rewrite < plus_minus_m_m + [rewrite > sym_times in ⊢ (? ? ? (? % ?)). + reflexivity + |apply lt_to_le. + assumption + ] + |rewrite > (times_n_O O). + apply lt_times;apply lt_O_fact + |change in ⊢ (? (? % ?) ?) with ((S k)*k!); + rewrite < sym_times in ⊢ (? ? %); + rewrite > assoc_times;apply divides_times + [apply reflexive_divides + |apply bc2;apply le_S_S_to_le;constructor 2;assumption] + |rewrite < fact_minus + [rewrite > sym_times in ⊢ (? (? ? %) ?);rewrite < assoc_times; + apply divides_times + [apply bc2;assumption + |apply reflexive_divides] + |assumption]] + |assumption] + |apply lt_to_lt_O_minus;assumption + |rewrite > (times_n_O O). + apply lt_times;apply lt_O_fact] +|apply lt_O_S +|rewrite > (times_n_O O). + apply lt_times;apply lt_O_fact] +qed. + +theorem lt_O_bc: \forall n,m. m \le n \to O < bc n m. +intro.elim n + [apply (le_n_O_elim ? H). + simplify.apply le_n + |elim (le_to_or_lt_eq ? ? H1) + [generalize in match H2.cases m;intro + [rewrite > bc_n_O.apply le_n + |rewrite > bc1 + [apply (trans_le ? (bc n1 n2)) + [apply H.apply le_S_S_to_le.apply lt_to_le.assumption + |apply le_plus_n_r + ] + |apply le_S_S_to_le.assumption + ] + ] + |rewrite > H2. + rewrite > bc_n_n. + apply le_n + ] + ] +qed. + +theorem exp_plus_sigma_p:\forall a,b,n. +exp (a+b) n = sigma_p (S n) (\lambda k.true) + (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)). +intros.elim n + [simplify.reflexivity + |simplify in ⊢ (? ? % ?). + rewrite > true_to_sigma_p_Sn + [rewrite > H;rewrite > sym_times in ⊢ (? ? % ?); + rewrite > distr_times_plus in ⊢ (? ? % ?); + rewrite < minus_n_n in ⊢ (? ? ? (? (? (? ? (? ? %)) ?) ?)); + rewrite > sym_times in ⊢ (? ? (? % ?) ?); + rewrite > sym_times in ⊢ (? ? (? ? %) ?); + rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? % ?) ?); + rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? ? %) ?); + rewrite > true_to_sigma_p_Sn in ⊢ (? ? (? ? %) ?) + [rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?); + rewrite > assoc_plus; + apply eq_f2 + [rewrite > sym_times;rewrite > assoc_times;autobatch paramodulation + |rewrite > (sigma_p_gi ? ? O); + [rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in ⊢ (? ? (? (? ? %) ?) ?) + [rewrite > (sigma_p_gi ? ? O) in ⊢ (? ? ? %); + [rewrite > assoc_plus;apply eq_f2 + [autobatch paramodulation; + |rewrite < sigma_p_plus_1; + rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in \vdash (? ? ? %); + [apply eq_sigma_p + [intros;reflexivity + |intros;rewrite > sym_times;rewrite > assoc_times; + rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?); + rewrite > assoc_times;rewrite < assoc_times in ⊢ (? ? (? (? ? %) ?) ?); + rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?) ?); + change in ⊢ (? ? (? (? ? (? % ?)) ?) ?) with (exp a (S (n1 - S x))); + rewrite < (minus_Sn_m ? ? H1);rewrite > minus_S_S; + rewrite > sym_times in \vdash (? ? (? ? %) ?); + rewrite > assoc_times; + rewrite > sym_times in ⊢ (? ? (? ? (? ? %)) ?); + change in \vdash (? ? (? ? (? ? %)) ?) with (exp b (S x)); + rewrite > assoc_times in \vdash (? ? (? ? %) ?); + rewrite > sym_times in \vdash (? ? (? % ?) ?); + rewrite > sym_times in \vdash (? ? (? ? %) ?); + rewrite > assoc_times in \vdash (? ? ? %); + rewrite > sym_times in \vdash (? ? ? %); + rewrite < distr_times_plus; + rewrite > sym_plus;rewrite < bc1; + [reflexivity|assumption]] + |intros;simplify;reflexivity + |intros;simplify;reflexivity + |intros;apply le_S_S;assumption + |intros;reflexivity + |intros 2;elim j + [simplify in H2;destruct H2 + |simplify;reflexivity] + |intro;elim j + [simplify in H2;destruct H2 + |simplify;apply le_S_S_to_le;assumption]]] + |apply le_S_S;apply le_O_n + |reflexivity] + |intros;simplify;reflexivity + |intros;simplify;reflexivity + |intros;apply le_S_S;assumption + |intros;reflexivity + |intros 2;elim j + [simplify in H2;destruct H2 + |simplify;reflexivity] + |intro;elim j + [simplify in H2;destruct H2 + |simplify;apply le_S_S_to_le;assumption]] + |apply le_S_S;apply le_O_n + |reflexivity]] + |reflexivity] + |reflexivity]] +qed. + +theorem exp_S_sigma_p:\forall a,n. +exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))). +intros. +rewrite > plus_n_SO. +rewrite > exp_plus_sigma_p. +apply eq_sigma_p;intros + [reflexivity + |rewrite < exp_SO_n. + rewrite < times_n_SO. + reflexivity + ] +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/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma new file mode 100644 index 000000000..e8f8a7732 --- /dev/null +++ b/matita/matita/lib/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/matita/matita/lib/arithmetics/div_and_mod.ma b/matita/matita/lib/arithmetics/div_and_mod.ma index f2b0849af..cf19b8203 100644 --- a/matita/matita/lib/arithmetics/div_and_mod.ma +++ b/matita/matita/lib/arithmetics/div_and_mod.ma @@ -136,7 +136,6 @@ theorem div_times: ∀a,b:nat. O < b → a*b/b = a. @(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. @@ -148,7 +147,7 @@ theorem eq_div_O: ∀n,m. n < m → n / m = O. 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. *) +/2/ qed. theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m → ((S n) \mod m) = S (n \mod m). @@ -407,7 +406,7 @@ O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b). @(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_l) /2/ + [applyS (monotonic_lt_times_r … c posc) /2/ |(applyS (eq_f …(λx.x*c))) // ] ] diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma index 1c7adf69b..1205044be 100644 --- a/matita/matita/lib/arithmetics/exp.ma +++ b/matita/matita/lib/arithmetics/exp.ma @@ -75,11 +75,10 @@ qed. theorem le_exp: ∀n,m,p:nat. O < p → n ≤m → p^n ≤ p^m. -@nat_elim2 - [#n #m #ltm #len @lt_O_exp // - |#n #m #_ #len @False_ind /2/ - |#n #m #Hind #p #posp #lenm normalize @le_times // - @Hind /2/ +@nat_elim2 #n #m + [#ltm #len @lt_O_exp // + |#_ #len @False_ind /2/ + |#Hind #p #posp #lenm normalize @le_times // @Hind /2/ ] qed. diff --git a/matita/matita/lib/arithmetics/gcd.ma b/matita/matita/lib/arithmetics/gcd.ma new file mode 100644 index 000000000..86b0600be --- /dev/null +++ b/matita/matita/lib/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/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma index 33a75b67b..eda9d0166 100644 --- a/matita/matita/lib/arithmetics/minimization.ma +++ b/matita/matita/lib/arithmetics/minimization.ma @@ -190,7 +190,7 @@ n ≤ m → ∀b.min n b f ≤ min m b f. [#n #leSO @False_ind /2/ |#n #m #Hind #leSS #b (cases (true_or_false (f b))) #fb - [lapply (true_min …fb) // + [lapply (true_min …fb) #H >H >H // |>false_min // >false_min // @Hind /2/ ] ] @@ -298,7 +298,7 @@ min n b g ≤ min n b f. qed. theorem f_min_true : ∀ f.∀n,b. -(∃i:nat. b ≤ i ∧ i < n ∧ f i = true) → f (min n b f) = true. +(∃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/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index bb77db7c6..7ca90dcb2 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -151,6 +151,9 @@ theorem associative_times: associative nat times. 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/ @@ -452,58 +455,46 @@ cut (∀q:nat. q ≤ n → P q) /2/ qed. (* some properties of functions *) -(* -definition increasing \def \lambda f:nat \to nat. -\forall n:nat. f n < f (S n). - -theorem increasing_to_monotonic: \forall f:nat \to nat. -increasing f \to monotonic nat lt f. -unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H. -apply (trans_le ? (f n1)). -assumption.apply (trans_le ? (S (f n1))). -apply le_n_Sn. -apply H. + +definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n). + +theorem increasing_to_monotonic: ∀f:nat → nat. + increasing f → monotonic nat lt f. +#f #incr #n #m #ltnm (elim ltnm) /2/ qed. -theorem le_n_fn: \forall f:nat \to nat. (increasing f) -\to \forall n:nat. n \le (f n). -intros.elim n. -apply le_O_n. -apply (trans_le ? (S (f n1))). -apply le_S_S.apply H1. -simplify in H. unfold increasing in H.unfold lt in H.apply H. +theorem le_n_fn: ∀f:nat → nat. + increasing f → ∀n:nat. n ≤ f n. +#f #incr #n (elim n) /2/ qed. -theorem increasing_to_le: \forall f:nat \to nat. (increasing f) -\to \forall m:nat. \exists i. m \le (f i). -intros.elim m. -apply (ex_intro ? ? O).apply le_O_n. -elim H1. -apply (ex_intro ? ? (S a)). -apply (trans_le ? (S (f a))). -apply le_S_S.assumption. -simplify in H.unfold increasing in H.unfold lt in H. -apply H. +theorem increasing_to_le: ∀f:nat → nat. + increasing f → ∀m:nat.∃i.m ≤ f i. +#f #incr #m (elim m) /2/#n * #a #lenfa +@(ex_intro ?? (S a)) /2/ qed. -theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) -\to \forall m:nat. (f O) \le m \to -\exists i. (f i) \le m \land m <(f (S i)). -intros.elim H1. -apply (ex_intro ? ? O). -split.apply le_n.apply H. -elim H3.elim H4. -cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a))). -elim Hcut. -apply (ex_intro ? ? a). -split.apply le_S. assumption.assumption. -apply (ex_intro ? ? (S a)). -split.rewrite < H7.apply le_n. -rewrite > H7. -apply H. -apply le_to_or_lt_eq.apply H6. +theorem increasing_to_le2: ∀f:nat → nat. increasing f → + ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i). +#f #incr #m #lem (elim lem) + [@(ex_intro ? ? O) /2/ + |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H + [@(ex_intro ? ? a) % /2/ + |@(ex_intro ? ? (S a)) % // + ] + ] +qed. + +theorem increasing_to_injective: ∀f:nat → nat. + increasing f → injective nat nat f. +#f #incr #n #m cases(decidable_le n m) + [#lenm cases(le_to_or_lt_eq … lenm) // + #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq + @increasing_to_monotonic // + |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq + @lt_to_not_eq @increasing_to_monotonic /2/ + ] qed. -*) (*********************** monotonicity ***************************) theorem monotonic_le_plus_r: @@ -692,8 +683,8 @@ simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption. apply lt_plus.assumption.assumption. qed. *) -theorem monotonic_lt_times_l: - ∀c:nat. O < c → monotonic nat lt (λt.(t*c)). +theorem monotonic_lt_times_r: + ∀c:nat. O < c → monotonic nat lt (λt.(c*t)). #c #posc #n #m #ltnm (elim ltnm) normalize [/2/ @@ -701,9 +692,10 @@ theorem monotonic_lt_times_l: ] qed. -theorem monotonic_lt_times_r: - ∀c:nat. O < c → monotonic nat lt (λt.(c*t)). -/2/ 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. diff --git a/matita/matita/lib/arithmetics/nth_prime.ma b/matita/matita/lib/arithmetics/nth_prime.ma new file mode 100644 index 000000000..7b7c70bfe --- /dev/null +++ b/matita/matita/lib/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/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma new file mode 100644 index 000000000..2c4897d06 --- /dev/null +++ b/matita/matita/lib/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_minus >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/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma new file mode 100644 index 000000000..adbfd9cab --- /dev/null +++ b/matita/matita/lib/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/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma new file mode 100644 index 000000000..cdb497371 --- /dev/null +++ b/matita/matita/lib/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/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma new file mode 100644 index 000000000..ad3aa9371 --- /dev/null +++ b/matita/matita/lib/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/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma new file mode 100644 index 000000000..4d99c59c8 --- /dev/null +++ b/matita/matita/lib/basics/list.ma @@ -0,0 +1,170 @@ +(* + ||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 "basics/bool.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 + ]. + +(**************************** 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 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. + +(* +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; +napply (eq_rect_Type0 ????? e1); +napply (R1 ?? ? ?? e0); +napply a2; +nqed. + +ndefinition 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; +napply (eq_rect_Type0 ????? e2); +napply (R2 ?? ? ???? e0 ? e1); +napply a3; +nqed. + +ndefinition 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; +napply (eq_rect_Type0 ????? e3); +napply (R3 ????????? e0 ? e1 ? e2); +napply a4; +nqed. + +naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. *) diff --git a/matita/matita/lib/basics/pts.ma b/matita/matita/lib/basics/pts.ma new file mode 100644 index 000000000..94f49fc5c --- /dev/null +++ b/matita/matita/lib/basics/pts.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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]. diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma new file mode 100644 index 000000000..b31db23d7 --- /dev/null +++ b/matita/matita/lib/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/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma new file mode 100644 index 000000000..c14cc60b4 --- /dev/null +++ b/matita/matita/lib/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/matita/matita/lib/hints_declaration.ma b/matita/matita/lib/hints_declaration.ma new file mode 100644 index 000000000..bcbfed4f3 --- /dev/null +++ b/matita/matita/lib/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 lock2 (S : Type[2]) (s : S) : Type[3] ≝ { + force2 : Type[2]; + lift2 : force2 +}. + +record lock1 (S : Type[1]) (s : S) : Type[2] ≝ { + force1 : Type[1]; + lift1 : force1 +}. + +coercion zzzlift1 : ∀S:Type[1].∀s:S.∀l:lock1 S s. force1 S s l ≝ lift1 + on s : ? to force1 ???. + +coercion zzzlift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2 + on s : ? to force2 ???. + +(* Example of a non uniform coercion declaration + + Type[0] setoid + >---> + MR R + + provided MR = carr R + +unification hint 0 ≔ R : setoid; + MR ≟ carr R, + lock ≟ mk_lock1 Type[0] MR setoid R +(* ---------------------------------------- *) ⊢ + setoid ≡ force1 ? MR lock. + +*) +*) \ No newline at end of file diff --git a/matita/matita/lib/root b/matita/matita/lib/root new file mode 100644 index 000000000..c57405b94 --- /dev/null +++ b/matita/matita/lib/root @@ -0,0 +1 @@ +baseuri=cic:/matita/ -- 2.39.2