helm/software/matita/nlibrary/arithmetics/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 include "arithmetics/nat.ma".
  16
  17 nlet rec max i f ≝
  18   match i with
  19   [ O ⇒ O
  20   | (S n) ⇒ match f i with
  21       [ true ⇒ i
  22       | false ⇒ max n f ]].
  23
  24 ntheorem max_O_f : ∀f: nat → bool. max O f = O.
  25 //; nqed.
  26
  27 ntheorem max_S_max : ∀f: nat → bool.∀n:nat.
  28   (f (S n) = true ∧ max (S n) f = (S n)) ∨
  29   (f (S n) = false ∧ max (S n) f = max n f).
  30 #f; #n; nnormalize; ncases (f (S n)); /3/;
  31 nqed.
  32
  33 ntheorem le_max_n : ∀f: nat → bool. ∀n:nat.
  34   max n f ≤ n.
  35 #f; #n; nelim n;//;
  36 #n; #Hind; nnormalize; ncases (f (S n)); nnormalize; /2/;
  37 nqed.
  38
  39 ntheorem le_to_le_max : ∀f: nat → bool. ∀n,m:nat.
  40 n ≤ m  → max n f ≤ max m f.
  41 #f; #n; #m; #lenm; nelim lenm; //;
  42 #m; #le_n_m; #Hind; ncases (max_S_max f m); *; #_; #maxf;
  43 ##[napplyS le_S; /2/; ##| //; ##]
  44 nqed.
  45
  46 ntheorem f_m_to_le_max: ∀f.∀ n,m:nat.
  47  m ≤n  → f m = true → m ≤ max n f.
  48 #f; #n; nelim n; //;
  49 #m; #Hind; #a; #lea; #fa; ncases (max_S_max f m);*;//;
  50 #fSm; #max; napplyS Hind;//; napply (le_n_Sm_elim … lea);
  51 ##[/2/; ##| #eqa; napply False_ind;/2/;##]
  52 nqed.
  53
  54 ntheorem max_f_g: ∀f,g,n. (∀i. i ≤ n → f i = g i) →
  55   max n f = max n g.
  56 #f; #g; #n; nelim n;//;
  57 #a; #Hind; #eqfg; nnormalize;
  58 nrewrite > (eqfg …);//;
  59 nrewrite > (Hind ?);/3/;
  60 nqed.
  61
  62 (* spostare *)
  63 ntheorem bool_elim: ∀P:bool→Prop.∀b.
  64 (b = true → P true) → ( b = false → P false) → P b.
  65 #P; #b; ncases b;/2/; nqed.
  66
  67 ntheorem le_max_f_max_g: ∀f,g,n. (∀i. i ≤ n → f i = true → g i =true) →
  68   max n f ≤ max n g.
  69 #f; #g; #n; nelim n;//;
  70 #a; #Hind; #eqfg; nnormalize;
  71 napply (bool_elim ? (f (S a)));#fSa;
  72   ##[nrewrite > (eqfg …);//;
  73   ##|ncases (g (S a));nnormalize;
  74     ##[/2/; ##| napply Hind; /3/;
  75 nqed.
  76
  77 ntheorem max_O : ∀f:nat → bool. ∀n:nat.
  78 (∀i:nat. le i n → f i = false) → max n f = O.
  79 #f; #n; nelim n; //;
  80 #a; #Hind; #ffalse; nnormalize;
  81 nrewrite > (ffalse ??);//; napply Hind; /3/;
  82 nqed.
  83
  84 ntheorem f_max_true : ∀f:nat → bool. ∀n:nat.
  85 (∃i:nat. i ≤ n ∧ f i = true) → f (max n f) = true.
  86 #f; #n; nelim n;
  87 ##[*;#x;*; #lexO; napply (le_n_O_elim … lexO);//;
  88 ##|#a; #Hind; #exi;
  89    ncases (max_S_max f a); *; //;
  90    #fSa; #eqmax; napplyS Hind;
  91    ncases exi; #x; *;#lex; #fx; @ x; @;//;
  92    napply (le_n_Sm_elim x a lex);
  93    ##[/2/; ##|#eqx; napply False_ind; /2/;##]
  94 ##]
  95 nqed.
  96
  97 ntheorem exists_forall_le:∀f,n.
  98   (∃i. i ≤ n ∧ f i = true) ∨ (∀i. i ≤ n → f i = false).
  99 #f; #n; nelim n
 100   ##[napply (bool_elim ? (f O)); #f0;
 101     ##[/4/;
 102     ##|@2; #i; #lei; napply (le_n_O_elim ? lei); //; ##]
 103  ##|#a; *;
 104     ##[*;#x;*;#lex;#fx;@1;@x;/3/;
 105     ##|#H; napply (bool_elim ? (f (S a)));#fSa;
 106       ##[@1;@ (S a);/2/;
 107       ##|@2;#i;#lei; napply (le_n_Sm_elim …lei);/3/;
 108       ##]
 109     ##]
 110  ##]
 111 nqed.
 112
 113 ntheorem exists_max_forall_false:∀f,n.
 114  (∃i. i ≤ n ∧ f i = true) ∧ (f (max n f) = true) ∨
 115  (∀i. i ≤ n → f i = false) ∧ (max n f) = O.
 116 #f; #n; ncases (exists_forall_le f n); #H;/5/;
 117 nqed.
 118
 119 ntheorem false_to_lt_max: ∀f,n,m.O < n →
 120 f n = false → max m f ≤ n → max m f < n.
 121 #f; #n; #m; #posn; #fn; #maxf;
 122 nelim (le_to_or_lt_eq ? ? maxf);//;
 123 #maxfn; ncases (exists_max_forall_false f m);*;//;
 124 #_; #fmax; napply False_ind; /2/;
 125 nqed.
 126
 127 ntheorem lt_max_to_false : ∀f:nat → bool. ∀n,m:nat.
 128   max n f < m → m ≤ n → f m = false.
 129 #f; #n; nelim n;
 130   ##[#m; #H; #H1; napply False_ind; /3/;
 131   ##|#a; #Hind; #m;
 132      ncases (max_S_max f a); *;
 133      ##[#_;#eqmax;#H; #nH;napply False_ind;/3/;
 134      ##|#eqf;#eqmax;#lemax;#lem;
 135         napply (le_n_Sm_elim m a lem);/3/;
 136 nqed.
 137
 138 ntheorem f_false_to_le_max: ∀f,n,p. (∃i:nat.i≤n∧f i=true) →
 139 (∀m. p < m → f m = false) → max n f \le p.
 140 #f; #n; #p; #exi; #allm;
 141 napply not_lt_to_le; napply (not_to_not … not_eq_true_false);
 142 #ltp; nrewrite < (allm ? ltp);
 143 napply sym_eq; napply (f_max_true ? n exi); (* ? *)
 144 nqed.
 145
 146 ndefinition max_spec ≝ λf:nat → bool.λn,m: nat.
 147 m ≤ n ∧ f m =true ∧ ∀i. m < i → i ≤ n → f i = false.
 148
 149 ntheorem max_spec_to_max: ∀f:nat → bool.∀n,m:nat.
 150  max_spec f n m → max n f = m.
 151 #f; #n; nelim n
 152   ##[#m; *; *; #lemO; #_; #_; napply (le_n_O_elim ? lemO); //;
 153   ##|#n1; #Hind; #a; *; *; #lea; #fa; #all;
 154      ncases (max_S_max f n1); *; #fSn1; #maxSn1;
 155      ##[ncases (le_to_or_lt_eq … lea); #Ha;
 156       ##[napply False_ind;napply (absurd ?? not_eq_true_false);
 157          nrewrite < fSn1; napply all;//;
 158       ##|//;
 159       ##]
 160      ##|napplyS Hind; @;
 161       ##[@; //; ncases (le_to_or_lt_eq … lea); #Ha;
 162         ##[/2/;
 163         ##|napply False_ind;/2/;
 164         ##]
 165       ##|/3/;
 166       ##]
 167   ##]
 168 nqed.
 169
 170 (************************ minimization ************************)
 171
 172 nlet rec min_aux off n f ≝
 173   match off with
 174   [ O ⇒ n
 175   | S p ⇒ match f n with
 176     [ true ⇒ n
 177     | false ⇒ min_aux p (S n) f]].
 178
 179 ndefinition min : nat → (nat → bool) → nat ≝
 180   λn.λf.min_aux n O f.
 181
 182 ntheorem min_aux_O_f: ∀f:nat → bool. ∀i :nat.
 183   min_aux O i f = i.
 184 #f; #i; ncases i; //; nqed.
 185
 186 ntheorem min_O_f : ∀f:nat → bool.
 187   min O f = O.
 188 //; nqed.
 189
 190 ntheorem min_aux_S : ∀f: nat → bool. ∀i,n:nat.
 191 (f n = true ∧ min_aux (S i) n f = n) ∨
 192 (f n = false ∧ min_aux (S i) n f = min_aux i (S n) f).
 193 #f; #i; #n; nnormalize; ncases (f n); nnormalize;/3/;
 194 nqed.
 195
 196 ntheorem f_min_aux_true: ∀f:nat → bool. ∀off,m:nat.
 197   (∃i. m ≤ i ∧ i ≤ off + m ∧ f i = true) →
 198   f (min_aux off m f) = true.
 199 #f; #off; nelim off;
 200   ##[#m; *; #a; *; *; #leam; #lema; ncut (a = m);/2/;
 201   ##|#n; #Hind; #m; #exi; nnormalize;
 202      napply (bool_elim … (f m)); nnormalize; //;
 203      #fm;  napply Hind;
 204      ncases exi; #x; *; *; #lemx; #lex; #fx;
 205      @ x; @; //; @; //;
 206      ncases (le_to_or_lt_eq …lemx); #eqx; //;
 207      napply False_ind; /2/;
 208   ##]
 209 nqed.
 210
 211 ntheorem f_min_true: ∀f:nat → bool. ∀m:nat.
 212   (∃i. i ≤ m ∧ f i = true) → f (min m f) = true.
 213 #f; #m; *; #x; *; #lexm; #fx;
 214 napply (f_min_aux_true f m 0 ?); /4/;
 215 nqed.
 216
 217 ntheorem lt_min_aux_to_false : ∀f:nat → bool.∀off,n,m:nat.
 218   n ≤ m → m < min_aux off n f → f m = false.
 219 #f; #off; nelim off;
 220   ##[#n; #m; #lenm; #ltmn; napply False_ind;
 221      napply (absurd … lenm);/2/;
 222   ##|#n; #Hind; #a; #m; #leam;
 223      nnormalize; napply (bool_elim ? (f a)); nnormalize;
 224      ##[#fa; #ltm; napply False_ind; napply (absurd  (m < a));/2/;
 225      ##|ncases (le_to_or_lt_eq … leam);/2/;
 226 nqed.
 227
 228 nlemma le_min_aux : ∀f:nat → bool. ∀off,n:nat.
 229   n ≤ min_aux off n f.
 230 #f; #off; nelim off;//;
 231 #n; #Hind; #a; nelim (min_aux_S f n a); *; /2/;
 232 nqed.
 233
 234 ntheorem le_min_aux_r : ∀f:nat → bool.
 235   ∀off,n:nat. min_aux off n f ≤ n+off.
 236 #f; #off; nelim off; //;
 237 #n; #Hind; #a; nelim (min_aux_S f n a); *; /2/;
 238 nqed.