matita/contribs/library_auto/auto/nat/minimization.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/library_autobatch/nat/minimization".
  16
  17 include "auto/nat/minus.ma".
  18
  19 let rec max i f \def
  20   match (f i) with
  21   [ true \Rightarrow i
  22   | false \Rightarrow
  23       match i with
  24       [ O \Rightarrow O
  25       | (S j) \Rightarrow max j f ]].
  26
  27 theorem max_O_f : \forall f: nat \to bool. max O f = O.
  28 intro. simplify.
  29 elim (f O); autobatch.
  30 (*[ simplify.
  31   reflexivity
  32 | simplify.
  33   reflexivity
  34 ]*)
  35 qed.
  36
  37 theorem max_S_max : \forall f: nat \to bool. \forall n:nat.
  38 (f (S n) = true \land max (S n) f = (S n)) \lor
  39 (f (S n) = false \land max (S n) f = max n f).
  40 intros.simplify.elim (f (S n));autobatch.
  41 (*[ simplify.
  42   left.
  43   split;reflexivity
  44 | simplify.
  45   right.
  46   split;reflexivity.
  47 ]*)
  48 qed.
  49
  50 theorem le_max_n : \forall f: nat \to bool. \forall n:nat.
  51 max n f \le n.
  52 intros.
  53 elim n
  54 [ rewrite > max_O_f.
  55   apply le_n
  56 | simplify.
  57   elim (f (S n1));simplify;autobatch.
  58   (*[ simplify.
  59     apply le_n
  60   | simplify.
  61     apply le_S.
  62     assumption
  63   ]*)
  64 ]
  65 qed.
  66
  67 theorem le_to_le_max : \forall f: nat \to bool. \forall n,m:nat.
  68 n\le m  \to max n f \le max m f.
  69 intros.
  70 elim H
  71 [ apply le_n
  72 | apply (trans_le ? (max n1 f))
  73   [ apply H2
  74   | cut ((f (S n1) = true \land max (S n1) f = (S n1)) \lor
  75     (f (S n1) = false \land max (S n1) f = max n1 f))
  76     [ elim Hcut;elim H3;rewrite > H5;autobatch
  77       (*[ elim H3.
  78         rewrite > H5.
  79         apply le_S.
  80         apply le_max_n.
  81       | elim H3.
  82         rewrite > H5.
  83         apply le_n.
  84       ]*)
  85     | apply max_S_max.
  86     ]
  87   ]
  88 ]
  89 qed.
  90
  91 theorem f_m_to_le_max: \forall f: nat \to bool. \forall n,m:nat.
  92 m\le n \to f m = true \to m \le max n f.
  93 intros 3.
  94 elim n
  95 [ autobatch.
  96   (*apply (le_n_O_elim m H).
  97   apply le_O_n.*)
  98 | apply (le_n_Sm_elim m n1 H1);intro
  99   [ apply (trans_le ? (max n1 f)); autobatch
 100     (*[ apply H
 101       [apply le_S_S_to_le.
 102         assumption
 103       | assumption
 104       ]
 105     | apply le_to_le_max.
 106       apply le_n_Sn.
 107     ]*)
 108   | simplify.
 109     rewrite < H3.
 110     rewrite > H2.
 111     autobatch
 112     (*simplify.
 113     apply le_n.*)
 114   ]
 115 ]
 116 qed.
 117
 118
 119 definition max_spec \def \lambda f:nat \to bool.\lambda n: nat.
 120 \exists i. (le i n) \land (f i = true) \to
 121 (f n) = true \land (\forall i. i < n \to (f i = false)).
 122
 123 theorem f_max_true : \forall f:nat \to bool. \forall n:nat.
 124 (\exists i:nat. le i n \land f i = true) \to f (max n f) = true.
 125 intros 2.
 126 elim n
 127 [ elim H.
 128   elim H1.
 129   generalize in match H3.
 130   apply (le_n_O_elim a H2).
 131   autobatch
 132   (*intro.
 133   simplify.
 134   rewrite > H4.
 135   simplify.
 136   assumption.*)
 137 | simplify.
 138   apply (bool_ind (\lambda b:bool.
 139   (f (S n1) = b) \to (f (match b in bool with
 140   [ true \Rightarrow (S n1)
 141   | false  \Rightarrow (max n1 f)])) = true))
 142
 143   [ autobatch
 144     (*simplify.
 145     intro.
 146     assumption.*)
 147   | simplify.
 148     intro.
 149     apply H.
 150     elim H1.
 151     elim H3.
 152     generalize in match H5.
 153     apply (le_n_Sm_elim a n1 H4)
 154     [ intros.
 155       apply (ex_intro nat ? a).
 156       autobatch
 157       (*split
 158       [ apply le_S_S_to_le.
 159         assumption.
 160       | assumption.
 161       ]*)
 162     | intros.
 163       (* una chiamata di autobatch in questo punto genera segmentation fault*)
 164       apply False_ind.
 165       (* una chiamata di autobatch in questo punto genera segmentation fault*)
 166       apply not_eq_true_false.
 167       (* una chiamata di autobatch in questo punto genera segmentation fault*)
 168       rewrite < H2.
 169       (* una chiamata di autobatch in questo punto genera segmentation fault*)
 170       rewrite < H7.
 171       (* una chiamata di autobatch in questo punto genera segmentation fault*)
 172       rewrite > H6.
 173       reflexivity.
 174     ]
 175   | reflexivity.
 176   ]
 177 ]
 178 qed.
 179
 180 theorem lt_max_to_false : \forall f:nat \to bool.
 181 \forall n,m:nat. (max n f) < m \to m \leq n \to f m = false.
 182 intros 2.
 183 elim n
 184 [ absurd (le m O);autobatch
 185   (*[ assumption
 186   | cut (O < m)
 187     [ apply (lt_O_n_elim m Hcut).
 188       exact not_le_Sn_O.
 189     | rewrite < (max_O_f f).
 190       assumption.
 191     ]
 192   ]*)
 193 | generalize in match H1.
 194   elim (max_S_max f n1)
 195   [ elim H3.
 196     absurd (m \le S n1)
 197     [ assumption
 198     | apply lt_to_not_le.
 199       rewrite < H6.
 200       assumption
 201     ]
 202   | elim H3.
 203     apply (le_n_Sm_elim m n1 H2)
 204     [ intro.
 205       apply H;autobatch
 206       (*[ rewrite < H6.
 207         assumption
 208       | apply le_S_S_to_le.
 209         assumption
 210       ]*)
 211     | intro.
 212       autobatch
 213       (*rewrite > H7.
 214       assumption*)
 215     ]
 216   ]
 217 ]qed.
 218
 219 let rec min_aux off n f \def
 220   match f (n-off) with
 221   [ true \Rightarrow (n-off)
 222   | false \Rightarrow
 223       match off with
 224       [ O \Rightarrow n
 225       | (S p) \Rightarrow min_aux p n f]].
 226
 227 definition min : nat \to (nat \to bool) \to nat \def
 228 \lambda n.\lambda f. min_aux n n f.
 229
 230 theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat.
 231 min_aux O i f = i.
 232 intros.simplify.
 233 (*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
 234   in loop): dopo circa 3 minuti non era ancora terminata.
 235  *)
 236 rewrite < minus_n_O.
 237 (*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
 238   in loop): dopo circa 3 minuti non era ancora terminata.
 239  *)
 240 elim (f i); autobatch.
 241 (*[ reflexivity.
 242   simplify
 243 | reflexivity
 244 ]*)
 245 qed.
 246
 247 theorem min_O_f : \forall f:nat \to bool.
 248 min O f = O.
 249 intro.
 250 (* una chiamata di autobatch a questo punto NON conclude la dimostrazione*)
 251 apply (min_aux_O_f f O).
 252 qed.
 253
 254 theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
 255 (f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor
 256 (f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f).
 257 intros.simplify.elim (f (n - (S i)));autobatch.
 258 (*[ simplify.
 259   left.
 260   split;reflexivity.
 261 | simplify.
 262   right.
 263   split;reflexivity.
 264 ]*)
 265 qed.
 266
 267 theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat.
 268 (\exists i. le (m-off) i \land le i m \land f i = true) \to
 269 f (min_aux off m f) = true.
 270 intros 2.
 271 elim off
 272 [ elim H.
 273   elim H1.
 274   elim H2.
 275   cut (a = m)
 276   [ autobatch.
 277     (*rewrite > (min_aux_O_f f).
 278     rewrite < Hcut.
 279     assumption*)
 280   | apply (antisym_le a m)
 281     [ assumption
 282     | rewrite > (minus_n_O m).
 283       assumption
 284     ]
 285   ]
 286 | simplify.
 287   apply (bool_ind (\lambda b:bool.
 288   (f (m-(S n)) = b) \to (f (match b in bool with
 289   [ true \Rightarrow m-(S n)
 290   | false  \Rightarrow (min_aux n m f)])) = true))
 291   [ autobatch
 292     (*simplify.
 293     intro.
 294     assumption.*)
 295   | simplify.
 296     intro.
 297     apply H.
 298     elim H1.
 299     elim H3.
 300     elim H4.
 301     elim (le_to_or_lt_eq (m-(S n)) a H6)
 302     [ apply (ex_intro nat ? a).
 303       split;autobatch
 304       (*[ autobatch.split
 305         [ apply lt_minus_S_n_to_le_minus_n.
 306           assumption
 307         | assumption
 308         ]
 309       | assumption
 310       ]*)
 311     | absurd (f a = false)
 312       [ (* una chiamata di autobatch in questo punto genera segmentation fault*)
 313         rewrite < H8.
 314         assumption.
 315       | rewrite > H5.
 316         apply not_eq_true_false
 317       ]
 318     ]
 319   | reflexivity.
 320   ]
 321 ]
 322 qed.
 323
 324 theorem lt_min_aux_to_false : \forall f:nat \to bool.
 325 \forall n,off,m:nat. (n-off) \leq m \to m < (min_aux off n f) \to f m = false.
 326 intros 3.
 327 elim off
 328 [absurd (le n m)
 329   [ rewrite > minus_n_O.
 330     assumption
 331   | apply lt_to_not_le.
 332     rewrite < (min_aux_O_f f n).
 333     assumption
 334   ]
 335 | generalize in match H1.
 336   elim (min_aux_S f n1 n)
 337   [ elim H3.
 338     absurd (n - S n1 \le m)
 339     [ assumption
 340     | apply lt_to_not_le.
 341       rewrite < H6.
 342       assumption
 343     ]
 344   | elim H3.
 345     elim (le_to_or_lt_eq (n -(S n1)) m)
 346     [ apply H
 347       [ autobatch
 348         (*apply lt_minus_S_n_to_le_minus_n.
 349         assumption*)
 350       | rewrite < H6.
 351         assumption
 352       ]
 353     | rewrite < H7.
 354       assumption
 355     | assumption
 356     ]
 357   ]
 358 ]
 359 qed.
 360
 361 theorem le_min_aux : \forall f:nat \to bool.
 362 \forall n,off:nat. (n-off) \leq (min_aux off n f).
 363 intros 3.
 364 elim off
 365 [ rewrite < minus_n_O.
 366   autobatch
 367   (*rewrite > (min_aux_O_f f n).
 368   apply le_n.*)
 369 | elim (min_aux_S f n1 n)
 370   [ elim H1.
 371     autobatch
 372     (*rewrite > H3.
 373     apply le_n.*)
 374   | elim H1.
 375     rewrite > H3.
 376     autobatch
 377     (*apply (trans_le (n-(S n1)) (n-n1))
 378     [ apply monotonic_le_minus_r.
 379       apply le_n_Sn.
 380     | assumption.
 381     ]*)
 382   ]
 383 ]
 384 qed.
 385
 386 theorem le_min_aux_r : \forall f:nat \to bool.
 387 \forall n,off:nat. (min_aux off n f) \le n.
 388 intros.
 389 elim off
 390 [ simplify.
 391   rewrite < minus_n_O.
 392   elim (f n);autobatch
 393   (*[simplify.
 394     apply le_n.
 395   | simplify.
 396     apply le_n.
 397   ]*)
 398 | simplify.
 399   elim (f (n -(S n1)));simplify;autobatch
 400   (*[ apply le_plus_to_minus.
 401     rewrite < sym_plus.
 402     apply le_plus_n
 403   | assumption
 404   ]*)
 405 ]
 406 qed.