matita/matita/lib/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. max 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 @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 normalize in Hind; >Hind //
 126 #i #ltim @ext @le_S //
 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 @le_S //
 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 theorem f_false_to_le_max: ∀f,n,p. (∃i:nat.i<n∧f i=true) →
 144   (∀m. p < m → f m = false) → max n f ≤ p.
 145 #f #n #p #H1 #H2 @not_lt_to_le % #H3
 146 @(absurd ?? not_eq_true_false) <(H2 ? H3) @sym_eq
 147 @(f_max_true ? n H1)
 148 qed.
 149
 150 theorem exists_forall_lt:∀f,n.
 151 (∃i. i < n ∧ f i = true) ∨ (∀i. i < n → f i = false).
 152 #f #n elim n
 153   [%2 #i #lti0 @False_ind @(absurd ? lti0) @le_to_not_lt //
 154   |#n1 *
 155     [* #a * #Ha1 #Ha2 %1 %{a} % // @le_S //
 156     |#H cases (true_or_false (f n1)) #HfS >HfS
 157       [%1 %{n1} /2/
 158       |%2 #i #lei
 159        cases (le_to_or_lt_eq ?? lei) #Hi
 160         [@H @le_S_S_to_le @Hi | destruct (Hi) //]
 161       ]
 162     ]
 163   ]
 164 qed.
 165
 166 theorem exists_max_forall_false:∀f,n.
 167 ((∃i. i < n ∧ f i = true) ∧ (f (max n f) = true))∨
 168 ((∀i. i < n → f i = false) ∧ (max n f) = O).
 169 #f #n
 170 cases (exists_forall_lt f n)
 171   [#H %1 % // @(f_max_true f n) @H
 172   |#H %2 % [@H | @max_not_exists @H
 173   ]
 174 qed.
 175
 176
 177 theorem false_to_lt_max: ∀f,n,m.O < n →
 178   f n = false → max m f ≤ n → max m f < n.
 179 #f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax
 180   [//
 181   |cases (exists_max_forall_false f m)
 182     [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) //
 183     |* //
 184     ]
 185   ]
 186 qed.
 187
 188 (* minimization *)
 189
 190 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;
 191    returns  b + k otherwise *)
 192
 193 let rec min k b f ≝
 194   match k with
 195   [ O ⇒ b
 196   | S p ⇒
 197     match f b with
 198    [ true ⇒ b
 199    | false ⇒ min p (S b) f]].
 200
 201 definition min0 ≝ λn.λf. min n 0 f.
 202
 203 theorem min_O_f : ∀f.∀b. min O b f = b.
 204 // qed.
 205
 206 theorem true_min: ∀f.∀b.
 207   f b = true → ∀n.min n b f = b.
 208 #f #b #fb #n (cases n) // #n normalize >fb normalize //
 209 qed.
 210
 211 theorem false_min: ∀f.∀n,b.
 212   f b = false → min (S n) b f = min n (S b) f.
 213 #f #n #b #fb normalize >fb normalize //
 214 qed.
 215
 216 (*
 217 theorem leb_to_le_min : ∀f.∀n,b1,b2.
 218 b1 ≤ b2  → min n b1 f ≤ min n b2 f.
 219 #f #n #b1 #b2 #leb (elim n) //
 220 #m #Hind normalize (cases (f m)) normalize *)
 221
 222 theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b.
 223 #f #n normalize (elim n) // #m #Hind #b
 224 normalize (cases (f b)) normalize //
 225 qed.
 226
 227 theorem le_min_l: ∀f.∀n,b. b ≤ min n b f.
 228 #f #n normalize (elim n) // #m #Hind #b
 229 normalize (cases (f b)) normalize /2/
 230 qed.
 231
 232 theorem le_to_le_min : ∀f.∀n,m.
 233 n ≤ m  → ∀b.min n b f ≤ min m b f.
 234 #f @nat_elim2 //
 235   [#n #leSO @False_ind /2/
 236   |#n #m #Hind #leSS #b
 237    (cases (true_or_false (f b))) #fb
 238     [lapply (true_min …fb) #H >H >H //
 239     |>false_min // >false_min // @Hind /2/
 240     ]
 241   ]
 242 qed.
 243
 244 theorem true_to_le_min: ∀f.∀n,m,b.
 245  b ≤ m → f m = true → min n b f ≤ m.
 246 #f #n (elim n) //
 247 #i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb))
 248   [#ltm #fm normalize (cases (f b)) normalize // @Hind //
 249   |#eqm <eqm #eqb normalize >eqb normalize //
 250   ]
 251 qed.
 252
 253 theorem lt_min_to_false: ∀f.∀n,m,b.
 254  b ≤ m → m < min n b f → f m = false.
 255 #f #n #m #b #lebm #ltm cases(true_or_false (f m)) //
 256 #fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min //
 257 qed.
 258
 259 theorem fmin_true: ∀f.∀n,m,b.
 260  m = min n b f → m < n + b → f m = true.
 261 #f #n (elim n)
 262   [#m #b normalize #eqmb >eqmb #leSb @(False_ind)
 263    @(absurd … leSb) //
 264   |#n #Hind #m #b (cases (true_or_false (f b))) #caseb
 265     [>true_min //
 266     |>false_min // #eqm #ltm @(Hind m (S b)) /2/
 267     ]
 268   ]
 269 qed.
 270
 271 lemma min_exists: ∀f.∀t,m. m < t → f m = true →
 272 ∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b →
 273   min k b f = m.
 274 #f #t #m #ltmt #fm #k (elim k)
 275   [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
 276    @lt_to_not_le //
 277   |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
 278     [#ltbm >false_min /2 by le_n/ @Hind //
 279       [#i #H #H1 @ismin /2/ | >eqt normalize //]
 280     |#eqbm >true_min //
 281     ]
 282   ]
 283 qed.
 284
 285 lemma min_not_exists: ∀f.∀n,b.
 286  (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
 287 #f #n (elim n) //
 288 #p #Hind #b #ffalse >false_min
 289   [>Hind // #i #H #H1 @ffalse /2/
 290   |@ffalse //
 291   ]
 292 qed.
 293
 294 lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in
 295  f m = false → m = n+b.
 296 #f #n (elim n) //
 297 #i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb
 298 normalize
 299   [#eqm @False_ind @(absurd … fb) //
 300   |>plus_n_Sm @Hind]
 301 qed.
 302
 303 inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
 304  | found : ∀m:nat. b ≤ m → m < n + b → f m =true →
 305  (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m
 306  | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b).
 307
 308 theorem min_spec_to_min: ∀f.∀n,b,m.
 309   min_spec n b f m → min n b f = m.
 310 #f #n #b #m #spec (cases spec)
 311   [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin
 312   |#ffalse @min_not_exists @ffalse
 313   ]
 314 qed.
 315
 316 theorem min_to_min_spec: ∀f.∀n,b,m.
 317   min n b f = m → min_spec n b f m.
 318 #f #n #b #m (cases n)
 319   [#eqm <eqm %2 #i #lei #lti @False_ind @(absurd … lti) /2/
 320   |#n #eqm (* (cases (le_to_or_lt_eq … (le_min_r …))) Stack overflow! *)
 321    lapply (le_min_r f (S n) b) >eqm #lem
 322    (cases (le_to_or_lt_eq … lem)) #mcase
 323     [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) //
 324     |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) //
 325     ]
 326   ]
 327 qed.
 328
 329 theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
 330   min n b f = min n b g.
 331 #f #g #n (elim n) //
 332 #m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind //
 333 #i #ltib #ltim @ext // @lt_to_le //
 334 qed.
 335
 336 theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
 337 min n b g ≤ min n b f.
 338 #f #g #n (elim n) //
 339 #m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq
 340   [>ext //
 341   |(cases (g b)) normalize /2 by lt_to_le/ @Hind #i #ltb #ltim #fi
 342     @ext /2/
 343   ]
 344 qed.
 345
 346 theorem f_min_true : ∀ f.∀n,b.
 347 (∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true.
 348 #f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
 349 #Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
 350 qed.
 351
 352 theorem lt_min : ∀ f.∀n,b.
 353 (∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → min n b f < n + b.
 354 #f #n #b #H cases H #i * * #lebi #ltin #fi_true
 355 @(le_to_lt_to_lt … ltin) @true_to_le_min //
 356 qed.