1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "arithmetics/nat.ma".
20 | (S n) ⇒ match f i with
24 ntheorem max_O_f : ∀f: nat → bool. max O f = O.
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/;
33 ntheorem le_max_n : ∀f: nat → bool. ∀n:nat.
36 #n; #Hind; nnormalize; ncases (f (S n)); nnormalize; /2/;
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/; ##| //; ##]
46 ntheorem f_m_to_le_max: ∀f.∀ n,m:nat.
47 m ≤n → f m = true → m ≤ max n f.
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/;##]
54 ntheorem max_f_g: ∀f,g,n. (∀i. i ≤ n → f i = g i) →
56 #f; #g; #n; nelim n;//;
57 #a; #Hind; #eqfg; nnormalize;
58 nrewrite > (eqfg …);//;
59 nrewrite > (Hind ?);/3/;
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.
67 ntheorem le_max_f_max_g: ∀f,g,n. (∀i. i ≤ n → f i = true → g i =true) →
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/;
77 ntheorem max_O : ∀f:nat → bool. ∀n:nat.
78 (∀i:nat. le i n → f i = false) → max n f = O.
80 #a; #Hind; #ffalse; nnormalize;
81 nrewrite > (ffalse ??);//; napply Hind; /3/;
84 ntheorem f_max_true : ∀f:nat → bool. ∀n:nat.
85 (∃i:nat. i ≤ n ∧ f i = true) → f (max n f) = true.
87 ##[*;#x;*; #lexO; napply (le_n_O_elim … lexO);//;
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/;##]
97 ntheorem exists_forall_le:∀f,n.
98 (∃i. i ≤ n ∧ f i = true) ∨ (∀i. i ≤ n → f i = false).
100 ##[napply (bool_elim ? (f O)); #f0;
102 ##|@2; #i; #lei; napply (le_n_O_elim ? lei); //; ##]
104 ##[*;#x;*;#lex;#fx;@1;@x;/3/;
105 ##|#H; napply (bool_elim ? (f (S a)));#fSa;
107 ##|@2;#i;#lei; napply (le_n_Sm_elim …lei);/3/;
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/;
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/;
127 ntheorem lt_max_to_false : ∀f:nat → bool. ∀n,m:nat.
128 max n f < m → m ≤ n → f m = false.
130 ##[#m; #H; #H1; napply False_ind; /3/;
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/;
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); (* ? *)
146 ndefinition max_spec ≝ λf:nat → bool.λn,m: nat.
147 m ≤ n ∧ f m =true ∧ ∀i. m < i → i ≤ n → f i = false.
149 ntheorem max_spec_to_max: ∀f:nat → bool.∀n,m:nat.
150 max_spec f n m → max n f = m.
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;//;
161 ##[@; //; ncases (le_to_or_lt_eq … lea); #Ha;
163 ##|napply False_ind;/2/;
170 (************************ minimization ************************)
172 nlet rec min_aux off n f ≝
175 | S p ⇒ match f n with
177 | false ⇒ min_aux p (S n) f]].
179 ndefinition min : nat → (nat → bool) → nat ≝
182 ntheorem min_aux_O_f: ∀f:nat → bool. ∀i :nat.
184 #f; #i; ncases i; //; nqed.
186 ntheorem min_O_f : ∀f:nat → bool.
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/;
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.
200 ##[#m; *; #a; *; *; #leam; #lema; ncut (a = m);/2/;
201 ##|#n; #Hind; #m; #exi; nnormalize;
202 napply (bool_elim … (f m)); nnormalize; //;
204 ncases exi; #x; *; *; #lemx; #lex; #fx;
206 ncases (le_to_or_lt_eq …lemx); #eqx; //;
207 napply False_ind; /2/;
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/;
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.
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/;
228 nlemma le_min_aux : ∀f:nat → bool. ∀off,n:nat.
230 #f; #off; nelim off;//;
231 #n; #Hind; #a; nelim (min_aux_S f n a); *; /2/;
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/;