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 (* minimization *)
 188
 189 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;
 190    returns  b + k otherwise *)
 191
 192 let rec min k b f ≝
 193   match k with
 194   [ O ⇒ b
 195   | S p ⇒
 196     match f b with
 197    [ true ⇒ b
 198    | false ⇒ min p (S b) f]].
 199
 200 definition min0 ≝ λn.λf. min n 0 f.
 201
 202 theorem min_O_f : ∀f.∀b. min O b f = b.
 203 // qed.
 204
 205 theorem true_min: ∀f.∀b.
 206   f b = true → ∀n.min n b f = b.
 207 #f #b #fb #n (cases n) // #n normalize >fb normalize //
 208 qed.
 209
 210 theorem false_min: ∀f.∀n,b.
 211   f b = false → min (S n) b f = min n (S b) f.
 212 #f #n #b #fb normalize >fb normalize //
 213 qed.
 214
 215 (*
 216 theorem leb_to_le_min : ∀f.∀n,b1,b2.
 217 b1 ≤ b2  → min n b1 f ≤ min n b2 f.
 218 #f #n #b1 #b2 #leb (elim n) //
 219 #m #Hind normalize (cases (f m)) normalize *)
 220
 221 theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b.
 222 #f #n normalize (elim n) // #m #Hind #b
 223 normalize (cases (f b)) normalize //
 224 qed.
 225
 226 theorem le_min_l: ∀f.∀n,b. b ≤ min n b f.
 227 #f #n normalize (elim n) // #m #Hind #b
 228 normalize (cases (f b)) normalize /2/
 229 qed.
 230
 231 theorem le_to_le_min : ∀f.∀n,m.
 232 n ≤ m  → ∀b.min n b f ≤ min m b f.
 233 #f @nat_elim2 //
 234   [#n #leSO @False_ind /2/
 235   |#n #m #Hind #leSS #b
 236    (cases (true_or_false (f b))) #fb
 237     [lapply (true_min …fb) #H >H >H //
 238     |>false_min // >false_min // @Hind /2/
 239     ]
 240   ]
 241 qed.
 242
 243 theorem true_to_le_min: ∀f.∀n,m,b.
 244  b ≤ m → f m = true → min n b f ≤ m.
 245 #f #n (elim n) //
 246 #i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb))
 247   [#ltm #fm normalize (cases (f b)) normalize // @Hind //
 248   |#eqm <eqm #eqb normalize >eqb normalize //
 249   ]
 250 qed.
 251
 252 theorem lt_min_to_false: ∀f.∀n,m,b.
 253  b ≤ m → m < min n b f → f m = false.
 254 #f #n #m #b #lebm #ltm cases(true_or_false (f m)) //
 255 #fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min //
 256 qed.
 257
 258 theorem fmin_true: ∀f.∀n,m,b.
 259  m = min n b f → m < n + b → f m = true.
 260 #f #n (elim n)
 261   [#m #b normalize #eqmb >eqmb #leSb @(False_ind)
 262    @(absurd … leSb) //
 263   |#n #Hind #m #b (cases (true_or_false (f b))) #caseb
 264     [>true_min //
 265     |>false_min // #eqm #ltm @(Hind m (S b)) /2/
 266     ]
 267   ]
 268 qed.
 269
 270 lemma min_exists: ∀f.∀t,m. m < t → f m = true →
 271 ∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b →
 272   min k b f = m.
 273 #f #t #m #ltmt #fm #k (elim k)
 274   [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
 275    @lt_to_not_le //
 276   |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
 277     [#ltbm >false_min /2 by le_n/ @Hind //
 278       [#i #H #H1 @ismin /2/ | >eqt normalize //]
 279     |#eqbm >true_min //
 280     ]
 281   ]
 282 qed.
 283
 284 lemma min_not_exists: ∀f.∀n,b.
 285  (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
 286 #f #n (elim n) //
 287 #p #Hind #b #ffalse >false_min
 288   [>Hind // #i #H #H1 @ffalse /2/
 289   |@ffalse //
 290   ]
 291 qed.
 292
 293 lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in
 294  f m = false → m = n+b.
 295 #f #n (elim n) //
 296 #i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb
 297 normalize
 298   [#eqm @False_ind @(absurd … fb) //
 299   |>plus_n_Sm @Hind]
 300 qed.
 301
 302 inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
 303  | found : ∀m:nat. b ≤ m → m < n + b → f m =true →
 304  (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m
 305  | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b).
 306
 307 theorem min_spec_to_min: ∀f.∀n,b,m.
 308   min_spec n b f m → min n b f = m.
 309 #f #n #b #m #spec (cases spec)
 310   [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin
 311   |#ffalse @min_not_exists @ffalse
 312   ]
 313 qed.
 314
 315 theorem min_to_min_spec: ∀f.∀n,b,m.
 316   min n b f = m → min_spec n b f m.
 317 #f #n #b #m (cases n)
 318   [#eqm <eqm %2 #i #lei #lti @False_ind @(absurd … lti) /2/
 319   |#n #eqm (* (cases (le_to_or_lt_eq … (le_min_r …))) Stack overflow! *)
 320    lapply (le_min_r f (S n) b) >eqm #lem
 321    (cases (le_to_or_lt_eq … lem)) #mcase
 322     [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) //
 323     |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) //
 324     ]
 325   ]
 326 qed.
 327
 328 theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
 329   min n b f = min n b g.
 330 #f #g #n (elim n) //
 331 #m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind //
 332 #i #ltib #ltim @ext // @lt_to_le //
 333 qed.
 334
 335 theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
 336 min n b g ≤ min n b f.
 337 #f #g #n (elim n) //
 338 #m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq
 339   [>ext //
 340   |(cases (g b)) normalize /2 by lt_to_le/ @Hind #i #ltb #ltim #fi
 341     @ext /2/
 342   ]
 343 qed.
 344
 345 theorem f_min_true : ∀ f.∀n,b.
 346 (∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true.
 347 #f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
 348 #Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
 349 qed.