From 7f9fc98eb7dc5467c46ff59cade6d929b3bbf9e0 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 31 May 2013 09:41:17 +0000 Subject: [PATCH] bounded quantifiers and pidgeon_hole --- .../lib/arithmetics/bounded_quantifiers.ma | 62 +++++++++++ matita/matita/lib/arithmetics/log.ma | 2 +- matita/matita/lib/arithmetics/minimization.ma | 7 ++ matita/matita/lib/arithmetics/pidgeon_hole.ma | 100 ++++++++++++++++++ 4 files changed, 170 insertions(+), 1 deletion(-) create mode 100644 matita/matita/lib/arithmetics/bounded_quantifiers.ma create mode 100644 matita/matita/lib/arithmetics/pidgeon_hole.ma diff --git a/matita/matita/lib/arithmetics/bounded_quantifiers.ma b/matita/matita/lib/arithmetics/bounded_quantifiers.ma new file mode 100644 index 000000000..6d715fcec --- /dev/null +++ b/matita/matita/lib/arithmetics/bounded_quantifiers.ma @@ -0,0 +1,62 @@ +(* + ||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". + +lemma decidable_not: ∀P. decidable P → decidable (¬P). +#P * #H [%2 % * /2/ | /2/] +qed. + +lemma decidable_or: ∀P,Q. decidable P → decidable Q → decidable (P∨Q). +#P #Q * #HP [#_ %1 %1 // |* #HQ [ %1 %2 // | %2 % * /2/] +qed. + +lemma decidable_forall: ∀P. (∀i.decidable (P i))→ + ∀n.decidable (∀i. i < n → P i). +#P #Hdec #n elim n + [%1 #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt // + |#m * #H + [cases (Hdec m) #HPm + [%1 #i #lei0 cases (le_to_or_lt_eq … lei0) #H1 + [@H @le_S_S_to_le @H1 |>(injective_S … H1) @HPm] + |%2 @(not_to_not … HPm) #H1 @H1 // + ] + |%2 @(not_to_not … H) #H1 #i #leim @H1 @le_S // + ] + ] +qed. + +lemma not_exists_to_forall: ∀P,n. + ¬(∃i. i < n ∧ P i) → ∀i. i < n → ¬ P i. +#P #n elim n + [#_ #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt // + |#m #Hind #H1 #i #leiS cases (le_to_or_lt_eq … leiS) #H2 + [@(Hind … (le_S_S_to_le … H2)) @(not_to_not … H1) * + #a * #leam #Pa %{a} % // @le_S // + |@(not_to_not … H1) #Pi %{i} % // + ] + ] +qed. + +lemma not_forall_to_exists: ∀P,n. (∀i.decidable (P i)) → + ¬(∀i. i < n → P i) → (∃i. i < n ∧ ¬ (P i)). +#P #n #decP elim n + [* #H @False_ind @H #i #lti0 @False_ind @(absurd … lti0) @le_to_not_lt // + |#m #Hind #H1 cases (decP m) #H2 + [cases (Hind ?) + [#i * #leim #nPi %{i} % // @le_S // + |@(not_to_not … H1) #H3 #i #leiS cases (le_to_or_lt_eq … leiS) + [#ltiS @H3 @le_S_S_to_le // |#eqi //] + ] + |%{m} % // + ] + ] +qed. \ No newline at end of file diff --git a/matita/matita/lib/arithmetics/log.ma b/matita/matita/lib/arithmetics/log.ma index bbd65be96..6c7e159e4 100644 --- a/matita/matita/lib/arithmetics/log.ma +++ b/matita/matita/lib/arithmetics/log.ma @@ -10,8 +10,8 @@ V_______________________________________________________________ *) include "arithmetics/exp.ma". -include "arithmetics/minimization.ma". include "arithmetics/div_and_mod.ma". +include "arithmetics/minimization.ma". definition log ≝ λp,n. max n (λx.leb (exp p x) n). diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma index 526539b24..55a6ddef8 100644 --- a/matita/matita/lib/arithmetics/minimization.ma +++ b/matita/matita/lib/arithmetics/minimization.ma @@ -184,6 +184,7 @@ theorem false_to_lt_max: ∀f,n,m.O < n → ] ] qed. + (* minimization *) (* min k b f is the minimun i, b ≤ i < b + k s.t. f i; @@ -347,3 +348,9 @@ theorem f_min_true : ∀ f.∀n,b. #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. + +theorem lt_min : ∀ f.∀n,b. +(∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → min n b f < n + b. +#f #n #b #H cases H #i * * #lebi #ltin #fi_true +@(le_to_lt_to_lt … ltin) @true_to_le_min // +qed. \ No newline at end of file diff --git a/matita/matita/lib/arithmetics/pidgeon_hole.ma b/matita/matita/lib/arithmetics/pidgeon_hole.ma new file mode 100644 index 000000000..c1bcc72ef --- /dev/null +++ b/matita/matita/lib/arithmetics/pidgeon_hole.ma @@ -0,0 +1,100 @@ +(* + ||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/bounded_quantifiers.ma". +include "basics/lists/list.ma". + +(* A bit of combinatorics *) +interpretation "list membership" 'mem a l = (mem ? a l). + +lemma decidable_mem_nat: ∀n:nat.∀l. decidable (n ∈ l). +#n #l elim l + [%2 % @False_ind |#a #tl #Htl @decidable_or //] +qed. + +lemma length_unique_le: ∀n,l. unique ? l → (∀x. x ∈ l → x < n) → |l| ≤ n. +#n elim n + [* // #a #tl #_ #H @False_ind @(absurd (a < 0)) + [@H %1 % | @le_to_not_lt //] + |#m #Hind #l #Huni #Hmem <(filter_length2 ? (eqb m) l) + lapply (length_filter_eqb … m l Huni) #Hle + @(transitive_le ? (1+|filter ? (λx.¬ eqb m x) l|)) + [@le_plus // + |@le_S_S @Hind + [@unique_filter // + |#x #memx cut (x ≤ m) + [@le_S_S_to_le @Hmem @(mem_filter … memx)] #Hcut + cases(le_to_or_lt_eq … Hcut) // #eqxm @False_ind + @(absurd ? eqxm) @sym_not_eq @eqb_false_to_not_eq + @injective_notb @(mem_filter_true ???? memx) + ] + ] + ] +qed. + +lemma eq_length_to_mem : ∀n,l. |l| = S n → unique ? l → + (∀x. x ∈ l → x ≤ n) → n ∈ l. +#n #l #H1 #H2 #H3 cases (decidable_mem_nat n l) // +#H4 @False_ind @(absurd (|l| > n)) + [>H1 // + |@le_to_not_lt @length_unique_le // + #x #memx cases(le_to_or_lt_eq … (H3 x memx)) // + #Heq @not_le_to_lt @(not_to_not … H4) #_ Hfilter % + |@unique_filter @H1 + |#x #memx cases (le_to_or_lt_eq … (H2 x (mem_filter … memx))) #H3 + [@le_S_S_to_le @H3 + |@False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq + @injective_notb >(mem_filter_true ???? memx) % + ] + |@le_S_S_to_le @leim + ] + |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //] + ] + ] +qed. + +lemma lt_length_to_not_mem: ∀n,l. unique ? l → (∀x. x ∈ l → x < n) → |l| < n → +∃i. i < n ∧ ¬ (i ∈ l). +#n elim n + [#l #_ #_ #H @False_ind /2/ + |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni) + [2: * #H #_ %{m} % // + |* #memm #Hfilter cases (Hind (filter ? (λx. ¬(eqb m x)) l) ? ? ?) + [#i * #ltim #memi %{i} % [@le_S // ] + @(not_to_not … memi) @mem_filter_l @injective_notb >notb_notb + @not_eq_to_eqb_false @sym_not_eq @lt_to_not_eq // + |@unique_filter // + |#x #memx cases (le_to_or_lt_eq … (Hmem x ?)) + [#H @le_S_S_to_le @H + |#H @False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq + @injective_notb >(mem_filter_true ???? memx) % + |@(mem_filter … memx) + ] + |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H + @le_S_S_to_le @H + ] + ] + ] +qed. \ No newline at end of file -- 2.39.2