X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fminimization.ma;h=55a6ddef8fee864fdf0a7c05984ecefd0f10ef52;hb=7c9d99dfb049d726491b71f07ba6a9b088b30166;hp=33a75b67bad55c4ed5fe63693d1dd50c1c44c66a;hpb=1b1224fb776aaccb9935e61db36fed1160317621;p=helm.git

diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index 33a75b67b..55a6ddef8 100644
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -40,7 +40,7 @@ qed.
 
 theorem lt_max_n : ∀f.∀n. O < n → max n f < n.
 #f #n #posn @(lt_O_n_elim ? posn) #m
-normalize (cases (f m)) normalize apply le_S_S //
+normalize (cases (f m)) normalize @le_S_S //
 @le_max_n qed.
 
 theorem le_to_le_max : ∀f.∀n,m.
@@ -122,8 +122,8 @@ qed.
 theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) → 
   max n f = max n g.
 #f #g #n (elim n) //
-#m #Hind #ext normalize >ext >Hind //
-#i #ltim @ext /2/
+#m #Hind #ext normalize >ext normalize in Hind; >Hind //
+#i #ltim @ext @le_S //
 qed.
 
 theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) →
@@ -131,7 +131,7 @@ max n f ≤ max n g.
 #f #g #n (elim n) //
 #m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq 
   [>ext //
-  |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/
+  |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext @le_S //
 qed.
 
 theorem f_max_true : ∀ f.∀n.
@@ -140,6 +140,51 @@ theorem f_max_true : ∀ f.∀n.
 #Hall * #x * #ltx #fx @False_ind @(absurd … fx) >Hall /2/
 qed.
 
+theorem f_false_to_le_max: ∀f,n,p. (∃i:nat.i<n∧f i=true) →
+  (∀m. p < m → f m = false) → max n f ≤ p.
+#f #n #p #H1 #H2 @not_lt_to_le % #H3
+@(absurd ?? not_eq_true_false) <(H2 ? H3) @sym_eq
+@(f_max_true ? n H1)
+qed.
+
+theorem exists_forall_lt:∀f,n. 
+(∃i. i < n ∧ f i = true) ∨ (∀i. i < n → f i = false).
+#f #n elim n
+  [%2 #i #lti0 @False_ind @(absurd ? lti0) @le_to_not_lt // 
+  |#n1 *
+    [* #a * #Ha1 #Ha2 %1 %{a} % // @le_S //
+    |#H cases (true_or_false (f n1)) #HfS >HfS
+      [%1 %{n1} /2/
+      |%2 #i #lei 
+       cases (le_to_or_lt_eq ?? lei) #Hi 
+        [@H @le_S_S_to_le @Hi | destruct (Hi) //] 
+      ]
+    ]
+  ]
+qed.
+     
+theorem exists_max_forall_false:∀f,n. 
+((∃i. i < n ∧ f i = true) ∧ (f (max n f) = true))∨
+((∀i. i < n → f i = false) ∧ (max n f) = O).
+#f #n
+cases (exists_forall_lt f n)
+  [#H %1 % // @(f_max_true f n) @H
+  |#H %2 % [@H | @max_not_exists @H 
+  ]
+qed.
+
+
+theorem false_to_lt_max: ∀f,n,m.O < n →
+  f n = false → max m f ≤ n → max m f < n.
+#f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax 
+  [//
+  |cases (exists_max_forall_false f m)
+    [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) //
+    |* //
+    ]
+  ]
+qed.
+
 (* minimization *)
  
 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;  
@@ -190,7 +235,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/
     ]
   ]
@@ -230,8 +275,8 @@ lemma min_exists: ∀f.∀t,m. m < t → f m = true →
   [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
    @lt_to_not_le //
   |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
-    [#ltbm >false_min /2/ @Hind // 
-      [#i #H #H1 @ismin /2/ | >eqt normalize //]
+    [#ltbm >false_min /2 by le_n/ @Hind //
+      [#i #H #H1 @ismin /2/ | >eqt normalize //] 
     |#eqbm >true_min //
     ]
   ]
@@ -285,7 +330,7 @@ theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
   min n b f = min n b g.
 #f #g #n (elim n) //
 #m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind //
-#i #ltib #ltim @ext /2/
+#i #ltib #ltim @ext // @lt_to_le //
 qed.
 
 theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
@@ -293,12 +338,19 @@ min n b g ≤ min n b f.
 #f #g #n (elim n) //
 #m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq 
   [>ext //
-  |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi
+  |(cases (g b)) normalize /2 by lt_to_le/ @Hind #i #ltb #ltim #fi
     @ext /2/
+  ]
 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.
+
+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