From b4681c749d6e8812fe86d5a9adbf4d4acbc3df06 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 28 Oct 2011 09:34:23 +0000 Subject: [PATCH] Some qed- --- matita/matita/lib/arithmetics/div_and_mod.ma | 4 +- matita/matita/lib/arithmetics/exp.ma | 50 ++++++++++++++++++- matita/matita/lib/arithmetics/minimization.ma | 4 +- matita/matita/lib/arithmetics/nat.ma | 26 +++++----- matita/matita/lib/arithmetics/primes.ma | 23 ++++----- 5 files changed, 76 insertions(+), 31 deletions(-) diff --git a/matita/matita/lib/arithmetics/div_and_mod.ma b/matita/matita/lib/arithmetics/div_and_mod.ma index 4044695d2..966ea3c84 100644 --- a/matita/matita/lib/arithmetics/div_and_mod.ma +++ b/matita/matita/lib/arithmetics/div_and_mod.ma @@ -153,7 +153,7 @@ 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) // +// @div_mod_spec_intro// applyS eq_f // qed. theorem mod_O_n: ∀n:nat.O \mod n = O. @@ -177,7 +177,7 @@ theorem or_div_mod: ∀n,q. O < q → ((S (n \mod q) (minus_Sn_n ?) +[cut (∃x.∃y.∃z.(x - y ≤ x - z) = (1 ≤ n ^a)) + [@ex_intro + [|@ex_intro + [|@ex_intro + [| +@(rewrite_r \Nopf (S n \sup a - n \sup a ) + (\lambda x:\Nopf + .(S n \sup a - n \sup a \le S n \sup a -(S ?-?))=(x\le n \sup a )) + (rewrite_r \Nopf ? + (\lambda x:\Nopf + .(S n \sup a - n \sup a \le x)=(S n \sup a - n \sup a \le n \sup a )) + ( refl … Type[0] (S n \sup a - n \sup a \le n \sup a ) ) (S ?-(S ?-?)) + (rewrite_r \Nopf (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x) + (rewrite_l \Nopf 1 (\lambda x:\Nopf .S ?-x=n ^a -O) (minus_S_S ? O) (S ?-?) + (minus_Sn_n ?)) ? + (minus_n_O ?))) 1 + (minus_Sn_n n \sup a )) + +@(rewrite_r \Nopf (S ?-?) + (\lambda x:\Nopf + .(S n \sup a - n \sup a \le S n \sup a -(S ?-?))=(x\le n \sup a )) + (rewrite_r \Nopf ? + (\lambda x:\Nopf + .(S n \sup a - n \sup a \le x)=(S n \sup a - n \sup a \le n \sup a )) + ( refl ??) (S ?-(S ?-?)) + ?) 1 + (minus_Sn_n ?)) + [|| +@(rewrite_r \Nopf (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x) + ???) +[|<(minus_Sn_n ?) +@(rewrite_r \Nopf (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x) + (rewrite_l \Nopf 1 (\lambda x:\Nopf .S ?-x=?-O) + ? (S ?-?) + (minus_Sn_n ?)) ??) + +@(rewrite_r \Nopf (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x) + (rewrite_l \Nopf 1 (\lambda x:\Nopf .S ?-x=?-O) (minus_S_S ? O) (S ?-?) + (minus_Sn_n ?)) ? + (minus_n_O ?))) + +applyS monotonic_le_minus_r /2/ +qed. *) theorem lt_m_exp_nm: ∀n,m:nat. 1 < n → m < n^m. #n #m #lt1n (elim m) normalize // diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma index 4c55ea6be..e558754d0 100644 --- a/matita/matita/lib/arithmetics/minimization.ma +++ b/matita/matita/lib/arithmetics/minimization.ma @@ -230,8 +230,8 @@ lemma min_exists: ∀f.∀t,m. m < t → f m = true → [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) false_min /2/ @Hind // - [#i #H #H1 @ismin /2/ | >eqt normalize //] + [#ltbm >false_min /2/ @Hind // + [#i #H #H1 @ismin /2/ | >eqt normalize //] |#eqbm >true_min // ] ] diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma index 6b3a1a19b..f4d78234f 100644 --- a/matita/matita/lib/arithmetics/nat.ma +++ b/matita/matita/lib/arithmetics/nat.ma @@ -1,4 +1,4 @@ -(* + (* ||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. @@ -239,7 +239,7 @@ theorem monotonic_pred: monotonic ? le pred. theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m. (* demo *) -/2/ qed. +/2/ qed-. (* this are instances of the le versions theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m. @@ -390,7 +390,7 @@ qed. *) theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → neq_minus_O /2/ >eq_minus_O // + #H >eq_minus_O /2/ (* >eq_minus_O // *) ] qed. @@ -1095,7 +1095,7 @@ 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. +/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)) @@ -1111,7 +1111,7 @@ 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. +/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)) diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma index 2e2ef98fb..c44caa7fe 100644 --- a/matita/matita/lib/arithmetics/primes.ma +++ b/matita/matita/lib/arithmetics/primes.ma @@ -255,18 +255,17 @@ 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. +example example1 : smallest_factor 3 = 3. normalize // qed. -theorem example2: smallest_factor 4 = 2. +example example2: smallest_factor 4 = 2. normalize // qed. -theorem example3 : smallest_factor 7 = 7. +example example3 : smallest_factor 7 = 7. normalize // -qed. *) +qed. theorem le_SO_smallest_factor: ∀n:nat. n ≤ 1 → smallest_factor n = n. @@ -339,16 +338,16 @@ definition primeb ≝ λn:nat. (leb 2 n) ∧ (eqb (smallest_factor n) n). (* it works! *) -theorem example4 : primeb 3 = true. +example example4 : primeb 3 = true. normalize // qed. -theorem example5 : primeb 6 = false. +example example5 : primeb 6 = false. normalize // qed. -theorem example6 : primeb 11 = true. +example example6 : primeb 11 = true. normalize // qed. -theorem example7 : primeb 17 = true. +example example7 : primeb 17 = true. normalize // qed. theorem primeb_true_to_prime : ∀n:nat. @@ -446,14 +445,14 @@ lemma nth_primeS: ∀n.nth_prime (S n) = // qed. (* it works *) -theorem example11 : nth_prime 2 = 5. +example example11 : nth_prime 2 = 5. normalize // qed. -theorem example12: nth_prime 3 = 7. +example example12: nth_prime 3 = 7. normalize // qed. -theorem example13 : nth_prime 4 = 11. +example example13 : nth_prime 4 = 11. normalize // qed. (* done in 13.1369330883s -- qualcosa non va: // lentissimo -- 2.39.2