Changeset 1882 for src/utilities/lists.ma
 Timestamp:
 Apr 6, 2012, 8:02:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/lists.ma
r1647 r1882 1 1 include "basics/lists/list.ma". 2 include "ASM/Util.ma". (* coercion from bool to Prop *) 3 4 lemma All_map : ∀A,B,P,Q,f,l. 5 All A P l → 6 (∀a.P a → Q (f a)) → 7 All B Q (map A B f l). 8 #A #B #P #Q #f #l elim l // 9 #h #t #IH * #Ph #Pt #F % [@(F ? Ph)  @(IH Pt F)] qed. 10 11 lemma Exists_map : ∀A,B,P,Q,f,l. 12 Exists A P l → 13 (∀a.P a → Q (f a)) → 14 Exists B Q (map A B f l). 15 #A #B #P #Q #f #l elim l // 16 #h #t #IH * #H #F 17 [ %1 @(F ? H)  %2 @(IH H F) ] 18 qed. 2 19 3 20 lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r). … … 32 49 ] qed. 33 50 51 lemma All_split : ∀A,P,l. All A P l → ∀pre,x,post.l = pre @ x :: post → P x. 52 #A #P #l elim l 53 [ * * normalize [2: #y #pre'] #x #post #ABS destruct(ABS) 54  #hd #tl #IH * #Phd #Ptl * normalize [2: #y #pre'] #x #post #EQ destruct(EQ) 55 [ @(IH Ptl … (refl …)) 56  @Phd 57 ] 58 ] 59 qed. 60 34 61 let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝ 35 62 match la with … … 57 84 ] H. 58 85 86 lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l). 87 #A#P#l elim l // 88 #h #t #Hi * #Ph #Pt normalize 89 >rev_append_def 90 @All_append 91 [ @(Hi Pt) 92  %{Ph I} 93 ] 94 qed. 95 96 lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l). 97 #A#P#l elim l // 98 #h #t #Hi normalize >rev_append_def 99 * [ #Ph @Exists_append_r %{Ph}  #Pt @Exists_append_l @(Hi Pt)] 100 qed. 101 102 include "utilities/option.ma". 103 104 lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) → 105 ∀l. All ? P l → opt_All ? Q (find … f l). 106 #A#B#P#Q#f#H#l elim l [#_%] 107 #x #l' #Hi 108 * #Px #AllPl' 109 whd in ⊢ (???%); 110 lapply (H x Px) 111 lapply (refl ? (f x)) 112 generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//] 113 #_ whd in ⊢ (???%); @(Hi AllPl') 114 qed. 115 59 116 include "utilities/monad.ma". 60 117 … … 65 122 list 66 123 (λX,x.[x]) 67 (λX,Y,l,f. \fold [append ?, [ ]]_{x ∈ l} (f x))68 ??? . normalize124 (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l) 125 ????. normalize 69 126 [ / by / 70 127  #X#m elim m normalize // 71 128  #X#Y#Z #m #f#g 72 129 elim m normalize [//] 73 #x#l' #Hi 74 <(fold_sum ?? (f x) ? [ ] (Append ?)) 75 >Hi // 130 #x#l' #Hi elim (f x) 131 [@Hi] normalize #hd #tl #IH >associative_append >IH % 132 #X#Y#m #f #g #H elim m normalize [//] 133 #hd #tl #IH >H >IH % 76 134 ] qed. 77 135 78 136 unification hint 0 ≔ X ; 79 N ≟ max_def List , M ≟ m_def N137 N ≟ max_def List 80 138 (**)⊢ 81 list X ≡ monad M X. 139 list X ≡ monad N X. 140 141 definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l. 142 143 lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x. 144 #A#P#l#x #Pl #xl elim (Exists_All … xl Pl) 145 #x' * #EQx' >EQx' // 146 qed. 147 148 lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l. 149 #A#P#l elim l 150 [#_ % 151 #x #l' #IH #H % 152 [ @H % % 153  @IH #y #G @H %2 @G 154 ] 155 ] 156 qed. 157 158 159 lemma nth_opt_append_l : ∀A,l1,l2,n.l1 > n → nth_opt A n (l1 @ l2) = nth_opt A n l1. 160 #A#l1 elim l1 normalize 161 [ #l2 #n #ABS elim (absurd ? ABS ?) // 162  #x #l' #IH #l2 #n cases n normalize 163 [// 164  #n #H @IH @le_S_S_to_le assumption 165 ] 166 ] 167 qed. 168 169 lemma nth_opt_append_r : ∀A,l1,l2,n.l1 ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n  l1) l2. 170 #A#l1 elim l1 171 [#l2 #n #_ <minus_n_O % 172 #x #l' #IH #l2 #n normalize in match (?); whd in match (nth_opt ???); 173 cases n n 174 [ #ABS elim (absurd ? ABS ?) // 175  #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption 176 ] 177 ] 178 qed. 179 180 lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x → 181 nth_opt A n (l1 @ l2) = Some ? x. 182 #A #l1 elim l1 normalize 183 [ #l2 #n #x #ABS destruct 184  #hd #tl #IH #l2 * [2: #n] #x normalize /2 by / 185 ] 186 qed. 187 188 lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? → 189 nth_opt A n (l1 @ l2) = nth_opt A (n  l1) l2. 190 #A #l1 elim l1 normalize 191 [ #l2 #n #_ <minus_n_O % 192  #hd #tl #IH #l2 * [2: #n] normalize 193 [ @IH 194  #ABS destruct(ABS) 195 ] 196 ] 197 qed. 198 199 200 (* count occurrences satisfying a test *) 201 let rec count A (f : A → bool) (l : list A) on l : ℕ ≝ 202 match l with 203 [ nil ⇒ 0 204  cons x l' ⇒ (if f x then 1 else 0) + count A f l' 205 ]. 206 207 theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2. 208 #A #f #l1 elim l1 209 [ #l2 % 210  #hd #tl #IH #l2 normalize elim (f hd) normalize >IH % 211 ] 212 qed. 213 214 215 include "utilities/option.ma". 216 217 lemma position_of_from_aux : ∀A,test,l,n. 218 position_of_aux A test l n = !n' ← position_of A test l; return n + n'. 219 #A #test #l elim l 220 [ normalize #_ % 221  #hd #tl #IH #n 222 normalize in ⊢ (??%?); >IH 223 normalize elim (test hd) normalize 224 [ <plus_n_O % 225  >(IH 1) whd in match (position_of ???); 226 elim (position_of_aux ??? 0) normalize 227 [ %  #x <plus_n_Sm % ] 228 ] 229 ] 230 qed. 231 232 definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1. 233 opt_safe ? (position_of A test l) ?. 234 lapply prf prf elim l normalize 235 [ #ABS elim (absurd ? ABS (not_le_Sn_O 0)) 236 #hd #tl #IH elim (test hd) normalize 237 [2: >position_of_from_aux #H 238 change with (position_of_aux ????) in match (position_of ???); 239 >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x] 240 #_ % #ABS destruct(ABS) 241 qed. 242 243 definition index_of ≝ 244 λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?. 245 lapply prf prf @eqb_elim #EQ * >EQ % 246 qed. 247 248 lemma position_of_append_hit : ∀A,test,l1,l2,x. 249 position_of A test (l1@l2) = Some ? x → 250 position_of A test l1 = Some ? x ∨ 251 (position_of A test l1 = None ? ∧ 252 ! p ← position_of A test l2 ; return (l1 + p) = Some ? x). 253 #A#test#l1 elim l1 254 [ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2 255 % % 256  #hd #tl #IH #l2 #x 257 normalize elim (test hd) normalize 258 [#H %{H} 259  >position_of_from_aux 260 lapply (refl … (position_of A test (tl@l2))) 261 generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq 262 normalize #EQ destruct(EQ) 263 elim (IH … Heq) IH 264 [ #G % 265  * #G #H 266 lapply (refl … (position_of A test l2)) 267 generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize 268 #EQ destruct (EQ) %2 %] 269 >position_of_from_aux 270 [1,2: >G %  >H' %] 271 ] 272 ] 273 qed. 274 275 lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x → 276 count A test l ≥ 1. 277 #A#test#l elim l normalize 278 [#x #ABS destruct(ABS) 279 #hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //] 280 >position_of_from_aux 281 lapply (refl … (position_of ? test tl)) 282 generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize 283 #EQ destruct(EQ) @(IH … Heq) 284 ] 285 qed. 286 287 lemma position_of_miss : ∀A,test,l.position_of A test l = None ? → 288 count A test l = 0. 289 #A#test#l elim l normalize 290 [ #_ % 291 #hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)] 292 >position_of_from_aux 293 lapply (refl … (position_of ? test tl)) 294 generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize 295 #EQ destruct(EQ) @(IH … Heq) 296 ] 297 qed. 298 299 300 lemma position_of_append_miss : ∀A,test,l1,l2. 301 position_of A test (l1@l2) = None ? → 302 position_of A test l1 = None ? ∧ position_of A test l2 = None ?. 303 #A#test#l1 elim l1 304 [ #l2 change with l2 in match (? @ l2); #EQ >EQ % % 305  #hd #tl #IH #l2 306 normalize elim (test hd) normalize 307 [#H destruct(H) 308  >position_of_from_aux 309 lapply (refl … (position_of A test (tl@l2))) 310 generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq 311 normalize #EQ destruct(EQ) 312 elim (IH … Heq) #H1 #H2 313 >position_of_from_aux 314 >position_of_from_aux 315 >H1 >H2 normalize % % 316 ] 317 ] 318 qed. 319 320
Note: See TracChangeset
for help on using the changeset viewer.