weblib/arithmetics/minimization.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/nat.ma".
  13
  14 (* maximization *)
  15
  16 let rec max' i f d ≝
  17   match i with
  18   [ O ⇒ d
  19   | S j ⇒
  20       match (f j) with
  21       [ true ⇒ j
  22       | false ⇒ max' j f d]].
  23
  24 definition max ≝ λn.λf.max' n f O.
  25
  26 theorem max_O: ∀f. \ 5A href="cic:/matita/arithmetics/minimization/max.def(2)"\ 6max\ 5/A\ 6 O f = O.
  27 // qed.
  28
  29 theorem max_cases: ∀f.∀n.
  30   (f n = true ∧ max (S n) f = n) ∨
  31   (f n  = false ∧ max (S n) f = max n f).
  32 #f #n normalize cases (f n) normalize /3/ qed.
  33
  34 theorem le_max_n: ∀f.∀n. max n f ≤ n.
  35 #f #n (elim n) // #m #Hind
  36 normalize (cases (f m)) normalize @le_S //
  37 (* non trova Hind *)
  38 @Hind
  39 qed.
  40
  41 theorem lt_max_n : ∀f.∀n. O < n → max n f < n.
  42 #f #n #posn @(lt_O_n_elim ? posn) #m
  43 normalize (cases (f m)) normalize apply le_S_S //
  44 @le_max_n qed.
  45
  46 theorem le_to_le_max : ∀f.∀n,m.
  47 n ≤ m  → max n f ≤ max m f.
  48 #f #n #m #H (elim H) //
  49 #i #leni #Hind @(transitive_le … Hind)
  50 (cases (max_cases f i)) * #_ /2/
  51 qed.
  52
  53 theorem true_to_le_max: ∀f.∀n,m.
  54  m < n → f m = true → m ≤ max n f.
  55 #f #n (elim n)
  56   [#m #ltmO @False_ind /2/
  57   |#i #Hind #m #ltm
  58    (cases (le_to_or_lt_eq … (le_S_S_to_le … ltm)))
  59     [#ltm #fm @(transitive_le ? (max i f))
  60       [@Hind /2/ | @le_to_le_max //]
  61     |#eqm >eqm #eqf normalize >eqf //
  62  ]
  63 qed.
  64
  65 theorem lt_max_to_false: ∀f.∀n,m.
  66  m < n → max n f < m → f m = false.
  67 #f #n #m #ltnm #eqf cases(true_or_false (f m)) //
  68 #fm @False_ind @(absurd … eqf) @(le_to_not_lt) @true_to_le_max //
  69 qed.
  70
  71 lemma max_exists: ∀f.∀n,m.m < n → f m =true →
  72  (∀i. m < i → i < n → f i = false) → max n f = m.
  73 #f #n (elim n) #m
  74   [#ltO @False_ind /2/
  75   |#Hind #max #ltmax #fmax #ismax
  76    cases (le_to_or_lt_eq …(le_S_S_to_le …(ltmax …)))
  77    #ltm normalize
  78      [>(ismax m …) // normalize @(Hind max ltm fmax)
  79       #i #Hl #Hr @ismax // @le_S //
  80      |<ltm >fmax //
  81      ]
  82    ]
  83 qed.
  84
  85 lemma max_not_exists: ∀f.∀n.
  86  (∀i. i < n → f i = false) → max n f = O.
  87 #f #n #ffalse @(le_gen ? n) #i (elim i) // #j #Hind #ltj
  88 normalize >ffalse // @Hind /2/
  89 qed.
  90
  91 lemma fmax_false: ∀f.∀n,m.max n f = m → f m = false → m = O.
  92 #f #n #m (elim n) //
  93 #i #Hind normalize cases(true_or_false … (f i)) #fi >fi
  94 normalize
  95   [#eqm #fm @False_ind @(absurd … fi) // |@Hind]
  96 qed.
  97
  98 inductive max_spec (n:nat) (f:nat→bool) : nat→Prop ≝
  99  | found : ∀m:nat.m < n → f m =true →
 100  (∀i. m < i → i < n → f i = false) → max_spec n f m
 101  | not_found: (∀i.i < n → f i = false) → max_spec n f O.
 102
 103 theorem max_spec_to_max: ∀f.∀n,m.
 104   max_spec n f m → max n f = m.
 105 #f #n #m #spec (cases spec)
 106   [#max #ltmax #fmax #ismax @max_exists // @ismax
 107   |#ffalse @max_not_exists @ffalse
 108   ]
 109 qed.
 110
 111 theorem max_to_max_spec: ∀f.∀n,m.
 112   max n f = m → max_spec n f m.
 113 #f #n #m (cases n)
 114   [#eqm <eqm %2 #i #ltiO @False_ind /2/
 115   |#n #eqm cases(true_or_false (f m)) #fm
 116     (* non trova max_to_false *)
 117     [%1 /2/
 118     |lapply (fmax_false ??? eqm fm) #eqmO >eqmO
 119      %2 #i (cases i) // #j #ltj @(lt_max_to_false … ltj) //
 120 qed.
 121
 122 theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) →
 123   max n f = max n g.
 124 #f #g #n (elim n) //
 125 #m #Hind #ext normalize >ext >Hind //
 126 #i #ltim @ext /2/
 127 qed.
 128
 129 theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) →
 130 max n f ≤ max n g.
 131 #f #g #n (elim n) //
 132 #m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq
 133   [>ext //
 134   |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/
 135 qed.
 136
 137 theorem f_max_true : ∀ f.∀n.
 138 (∃i:nat. i < n ∧ f i = true) → f (max n f) = true.
 139 #f #n cases(max_to_max_spec f n (max n f) (refl …)) //
 140 #Hall * #x * #ltx #fx @False_ind @(absurd … fx) >Hall /2/
 141 qed.
 142
 143 (* minimization *)
 144
 145 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;
 146    returns  b + k otherwise *)
 147
 148 let rec min k b f ≝
 149   match k with
 150   [ O ⇒ b
 151   | S p ⇒
 152     match f b with
 153    [ true ⇒ b
 154    | false ⇒ min p (S b) f]].
 155
 156 definition min0 ≝ λn.λf. min n 0 f.
 157
 158 theorem min_O_f : ∀f.∀b. min O b f = b.
 159 // qed.
 160
 161 theorem true_min: ∀f.∀b.
 162   f b = true → ∀n.min n b f = b.
 163 #f #b #fb #n (cases n) // #n normalize >fb normalize //
 164 qed.
 165
 166 theorem false_min: ∀f.∀n,b.
 167   f b = false → min (S n) b f = min n (S b) f.
 168 #f #n #b #fb normalize >fb normalize //
 169 qed.
 170
 171 (*
 172 theorem leb_to_le_min : ∀f.∀n,b1,b2.
 173 b1 ≤ b2  → min n b1 f ≤ min n b2 f.
 174 #f #n #b1 #b2 #leb (elim n) //
 175 #m #Hind normalize (cases (f m)) normalize *)
 176
 177 theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b.
 178 #f #n normalize (elim n) // #m #Hind #b
 179 normalize (cases (f b)) normalize //
 180 qed.
 181
 182 theorem le_min_l: ∀f.∀n,b. b ≤ min n b f.
 183 #f #n normalize (elim n) // #m #Hind #b
 184 normalize (cases (f b)) normalize /2/
 185 qed.
 186
 187 theorem le_to_le_min : ∀f.∀n,m.
 188 n ≤ m  → ∀b.min n b f ≤ min m b f.
 189 #f @nat_elim2 //
 190   [#n #leSO @False_ind /2/
 191   |#n #m #Hind #leSS #b
 192    (cases (true_or_false (f b))) #fb
 193     [lapply (true_min …fb) #H >H >H //
 194     |>false_min // >false_min // @Hind /2/
 195     ]
 196   ]
 197 qed.
 198
 199 theorem true_to_le_min: ∀f.∀n,m,b.
 200  b ≤ m → f m = true → min n b f ≤ m.
 201 #f #n (elim n) //
 202 #i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb))
 203   [#ltm #fm normalize (cases (f b)) normalize // @Hind //
 204   |#eqm <eqm #eqb normalize >eqb normalize //
 205   ]
 206 qed.
 207
 208 theorem lt_min_to_false: ∀f.∀n,m,b.
 209  b ≤ m → m < min n b f → f m = false.
 210 #f #n #m #b #lebm #ltm cases(true_or_false (f m)) //
 211 #fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min //
 212 qed.
 213
 214 theorem fmin_true: ∀f.∀n,m,b.
 215  m = min n b f → m < n + b → f m = true.
 216 #f #n (elim n)
 217   [#m #b normalize #eqmb >eqmb #leSb @(False_ind)
 218    @(absurd … leSb) //
 219   |#n #Hind #m #b (cases (true_or_false (f b))) #caseb
 220     [>true_min //
 221     |>false_min // #eqm #ltm @(Hind m (S b)) /2/
 222     ]
 223   ]
 224 qed.
 225
 226 lemma min_exists: ∀f.∀t,m. m < t → f m = true →
 227 ∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b →
 228   min k b f = m.
 229 #f #t #m #ltmt #fm #k (elim k)
 230   [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
 231    @lt_to_not_le //
 232   |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
 233     [#ltbm >false_min /2/ @Hind //
 234       [#i #H #H1 @ismin /2/ | >eqt normalize //]
 235     |#eqbm >true_min //
 236     ]
 237   ]
 238 qed.
 239
 240 lemma min_not_exists: ∀f.∀n,b.
 241  (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
 242 #f #n (elim n) //
 243 #p #Hind #b #ffalse >false_min
 244   [>Hind // #i #H #H1 @ffalse /2/
 245   |@ffalse //
 246   ]
 247 qed.
 248
 249 lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in
 250  f m = false → m = n+b.
 251 #f #n (elim n) //
 252 #i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb
 253 normalize
 254   [#eqm @False_ind @(absurd … fb) //
 255   |>plus_n_Sm @Hind]
 256 qed.
 257
 258 inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
 259  | found : ∀m:nat. b ≤ m → m < n + b → f m =true →
 260  (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m
 261  | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b).
 262
 263 theorem min_spec_to_min: ∀f.∀n,b,m.
 264   min_spec n b f m → min n b f = m.
 265 #f #n #b #m #spec (cases spec)
 266   [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin
 267   |#ffalse @min_not_exists @ffalse
 268   ]
 269 qed.
 270
 271 theorem min_to_min_spec: ∀f.∀n,b,m.
 272   min n b f = m → min_spec n b f m.
 273 #f #n #b #m (cases n)
 274   [#eqm <eqm %2 #i #lei #lti @False_ind @(absurd … lti) /2/
 275   |#n #eqm (* (cases (le_to_or_lt_eq … (le_min_r …))) Stack overflow! *)
 276    lapply (le_min_r f (S n) b) >eqm #lem
 277    (cases (le_to_or_lt_eq … lem)) #mcase
 278     [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) //
 279     |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) //
 280     ]
 281   ]
 282 qed.
 283
 284 theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
 285   min n b f = min n b g.
 286 #f #g #n (elim n) //
 287 #m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind //
 288 #i #ltib #ltim @ext /2/
 289 qed.
 290
 291 theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
 292 min n b g ≤ min n b f.
 293 #f #g #n (elim n) //
 294 #m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq
 295   [>ext //
 296   |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi
 297     @ext /2/
 298 qed.
 299
 300 theorem f_min_true : ∀ f.∀n,b.
 301 (∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true.
 302 #f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
 303 #Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
 304 qed.