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 /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 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 (* minimization *)
 151
 152 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;
 153    returns  b + k otherwise *)
 154
 155 let rec min k b f ≝
 156   match k with
 157   [ O ⇒ b
 158   | S p ⇒
 159     match f b with
 160    [ true ⇒ b
 161    | false ⇒ min p (S b) f]].
 162
 163 definition min0 ≝ λn.λf. min n 0 f.
 164
 165 theorem min_O_f : ∀f.∀b. min O b f = b.
 166 // qed.
 167
 168 theorem true_min: ∀f.∀b.
 169   f b = true → ∀n.min n b f = b.
 170 #f #b #fb #n (cases n) // #n normalize >fb normalize //
 171 qed.
 172
 173 theorem false_min: ∀f.∀n,b.
 174   f b = false → min (S n) b f = min n (S b) f.
 175 #f #n #b #fb normalize >fb normalize //
 176 qed.
 177
 178 (*
 179 theorem leb_to_le_min : ∀f.∀n,b1,b2.
 180 b1 ≤ b2  → min n b1 f ≤ min n b2 f.
 181 #f #n #b1 #b2 #leb (elim n) //
 182 #m #Hind normalize (cases (f m)) normalize *)
 183
 184 theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b.
 185 #f #n normalize (elim n) // #m #Hind #b
 186 normalize (cases (f b)) normalize //
 187 qed.
 188
 189 theorem le_min_l: ∀f.∀n,b. b ≤ min n b f.
 190 #f #n normalize (elim n) // #m #Hind #b
 191 normalize (cases (f b)) normalize /2/
 192 qed.
 193
 194 theorem le_to_le_min : ∀f.∀n,m.
 195 n ≤ m  → ∀b.min n b f ≤ min m b f.
 196 #f @nat_elim2 //
 197   [#n #leSO @False_ind /2/
 198   |#n #m #Hind #leSS #b
 199    (cases (true_or_false (f b))) #fb
 200     [lapply (true_min …fb) #H >H >H //
 201     |>false_min // >false_min // @Hind /2/
 202     ]
 203   ]
 204 qed.
 205
 206 theorem true_to_le_min: ∀f.∀n,m,b.
 207  b ≤ m → f m = true → min n b f ≤ m.
 208 #f #n (elim n) //
 209 #i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb))
 210   [#ltm #fm normalize (cases (f b)) normalize // @Hind //
 211   |#eqm <eqm #eqb normalize >eqb normalize //
 212   ]
 213 qed.
 214
 215 theorem lt_min_to_false: ∀f.∀n,m,b.
 216  b ≤ m → m < min n b f → f m = false.
 217 #f #n #m #b #lebm #ltm cases(true_or_false (f m)) //
 218 #fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min //
 219 qed.
 220
 221 theorem fmin_true: ∀f.∀n,m,b.
 222  m = min n b f → m < n + b → f m = true.
 223 #f #n (elim n)
 224   [#m #b normalize #eqmb >eqmb #leSb @(False_ind)
 225    @(absurd … leSb) //
 226   |#n #Hind #m #b (cases (true_or_false (f b))) #caseb
 227     [>true_min //
 228     |>false_min // #eqm #ltm @(Hind m (S b)) /2/
 229     ]
 230   ]
 231 qed.
 232
 233 lemma min_exists: ∀f.∀t,m. m < t → f m = true →
 234 ∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b →
 235   min k b f = m.
 236 #f #t #m #ltmt #fm #k (elim k)
 237   [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
 238    @lt_to_not_le //
 239   |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
 240     [#ltbm >false_min /2/ @Hind //
 241       [#i #H #H1 @ismin /2/ | >eqt normalize //]
 242     |#eqbm >true_min //
 243     ]
 244   ]
 245 qed.
 246
 247 lemma min_not_exists: ∀f.∀n,b.
 248  (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
 249 #f #n (elim n) //
 250 #p #Hind #b #ffalse >false_min
 251   [>Hind // #i #H #H1 @ffalse /2/
 252   |@ffalse //
 253   ]
 254 qed.
 255
 256 lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in
 257  f m = false → m = n+b.
 258 #f #n (elim n) //
 259 #i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb
 260 normalize
 261   [#eqm @False_ind @(absurd … fb) //
 262   |>plus_n_Sm @Hind]
 263 qed.
 264
 265 inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
 266  | found : ∀m:nat. b ≤ m → m < n + b → f m =true →
 267  (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m
 268  | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b).
 269
 270 theorem min_spec_to_min: ∀f.∀n,b,m.
 271   min_spec n b f m → min n b f = m.
 272 #f #n #b #m #spec (cases spec)
 273   [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin
 274   |#ffalse @min_not_exists @ffalse
 275   ]
 276 qed.
 277
 278 theorem min_to_min_spec: ∀f.∀n,b,m.
 279   min n b f = m → min_spec n b f m.
 280 #f #n #b #m (cases n)
 281   [#eqm <eqm %2 #i #lei #lti @False_ind @(absurd … lti) /2/
 282   |#n #eqm (* (cases (le_to_or_lt_eq … (le_min_r …))) Stack overflow! *)
 283    lapply (le_min_r f (S n) b) >eqm #lem
 284    (cases (le_to_or_lt_eq … lem)) #mcase
 285     [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) //
 286     |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) //
 287     ]
 288   ]
 289 qed.
 290
 291 theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
 292   min n b f = min n b g.
 293 #f #g #n (elim n) //
 294 #m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind //
 295 #i #ltib #ltim @ext /2/
 296 qed.
 297
 298 theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
 299 min n b g ≤ min n b f.
 300 #f #g #n (elim n) //
 301 #m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq
 302   [>ext //
 303   |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi
 304     @ext /2/
 305   ]
 306 qed.
 307
 308 theorem f_min_true : ∀ f.∀n,b.
 309 (∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true.
 310 #f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
 311 #Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
 312 qed.