bounded quantifiers and pidgeon_hole

diff --git a/matita/matita/lib/arithmetics/bounded_quantifiers.ma b/matita/matita/lib/arithmetics/bounded_quantifiers.ma
new file mode 100644 (file)
index 0000000..6d715fc
--- /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 bbd65be967edac94f57b849d89632f1dca0a6895..6c7e159e416c0f4f1bc58bf9b5a3d501f479e7ac 100644 (file)
--- 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 526539b2440d99a5703dd2d7926b8bd238447aca..55a6ddef8fee864fdf0a7c05984ecefd0f10ef52 100644 (file)
--- 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 (file)
index 0000000..c1bcc72
--- /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) #_ <Heq //
+  ]
+qed.
+
+lemma eq_length_to_mem_all: ∀n,l. |l| = n → unique ? l  → 
+  (∀x. x ∈ l → x < n) → ∀i. i < n → i ∈ l.
+#n elim n
+  [#l #_ #_ #_ #i #lti0 @False_ind @(absurd ? lti0 (not_le_Sn_O ?))
+  |#m #Hind #l #H #H1 #H2 #i #lei cases (le_to_or_lt_eq … lei)
+    [#leim @(mem_filter… (λi.¬(eqb m i))) 
+     cases (filter_eqb m … H1)
+      [2: * #H @False_ind @(absurd ?? H) @eq_length_to_mem //
+       #x #memx @le_S_S_to_le @H2 //]
+      * #memm #Hfilter @Hind
+        [@injective_S <H <(filter_length2 ? (eqb m) l) >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