 Timestamp:
 Jun 22, 2011, 4:03:33 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1006 r1034 60 60 qed. 61 61 62 (* definition forall63 ≝64 λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λ_.λa.λacc.(P a) ∧ acc) t True. *)65 66 62 definition forall 67 63 ≝ 68 64 λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True. 69 65 70 (* lemma forall_nodel:71 ∀A:Type[0].72 ∀n:nat.73 ∀l,r.74 ∀P:A → Prop.75 forall A (S n) (Node ? n l r) P → forall A n l P.76 #A #n #l #r #P generalize in match (refl ? n) #_ #Hl77 whd in Hl; whd @(fold_eq A n ? ? (fold A ? n (λx.λa.λacc.P a∧acc) r True) True)78 [ //79  #n #t' #X #Y #HXY #HX %180 [ @(proj1 ? ? HX)  @HXY @(proj2 ? ? HX) ]81  @Hl ]82 qed.83 84 lemma forall_noder:85 ∀A:Type[0].86 ∀n:nat.87 ∀l,r.88 ∀P.89 forall A (S n) (Node ? n l r) P → forall A n r P.90 #A #n #l #r #P generalize in match (refl ? n) #_ #Hr91 whd in Hr; whd @(fold_init A n (λx.λa.λacc.P a∧acc) l)92 [ #n #t' #P #HP @(proj2 ? ? HP)93  @Hr94 ]95 qed. *)96 97 66 lemma forall_nodel: 98 67 ∀A:Type[0]. … … 211 180 ] 212 181 qed. 213 182 214 183 let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝ 215 184 (match b with … … 311 280 [3,4: cases tl' //  *: @lookup_prepare_trie_for_insertion_miss //]]] 312 281 qed. 282 283 lemma lookup_stub: 284 ∀A.∀n.∀b.∀a. 285 lookup A n b (Stub A ?) a = a. 286 #A #n #b #a cases n in b ⊢ (??(??%%%?)?) 287 [ #b >(BitVector_O b) normalize @refl 288  #h #b cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd 289 [ normalize @refl 290  normalize @refl 291 ] 292 ] 293 qed. 294 295 lemma lookup_opt_lookup: 296 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A. 297 lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a. 298 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?) 299 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl 300  #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X; X; #tl #Hb 301 >Hb >Hb in H; cases hd 302 [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup 303  normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup 304 ] 305  #n #B #_ #H #x normalize in H; destruct 306 ] 307 qed. 308 309 lemma lookup_opt_prepare_trie_for_insertion_hit: 310 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n. 311 lookup_opt … b (prepare_trie_for_insertion … b v) = Some A v. 312 #A #v #n #b elim b // #m #hd #tl #IH cases hd normalize // 313 qed. 314 315 lemma lookup_opt_insert_hit: 316 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. 317 lookup_opt … b (insert … b v t) = Some A v. 318 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?) 319 [ #x #b >(BitVector_O b) normalize @refl 320  #h #l #r #Hl #Hr #b cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd 321 [ normalize @Hr 322  normalize @Hl 323 ] 324  #n' #b cases n' in b ⊢ ? 325 [ #b >(BitVector_O b) normalize @refl 326  #m #b cases (BitVector_Sn m b) #hd #X elim X X; #tl #Hb >Hb cases hd 327 normalize @lookup_opt_prepare_trie_for_insertion_hit 328 ] 329 ] 330 qed. 331 332 lemma forall_insert_inv1: 333 ∀A.∀n.∀b.∀a.∀t.∀P. 334 forall A n (insert A n b a t) P → P b a. 335 #A #n #b #a #t #P #H @(forall_lookup ? ? (insert A n b a t)) 336 [ @H 337  >(lookup_opt_insert_hit A ? n b) @(refl ? (Some A a)) 338 ] 339 qed. 340 341 lemma forall_insert_inv2a: 342 ∀A:Type[0].∀n:nat.∀b.∀a.∀t.∀P. 343 lookup_opt A n b t = (None A) → forall A n (insert A n b a t) P → forall A n t P. 344 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%) 345 [ #x #b #_ #P >(BitVector_O b) normalize #H destruct 346  #h #l #r #Hl #Hr #b #_ #P cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd #Hlookup #H 347 [ normalize in H; normalize 348 @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … H) 349 [ #Hfold @(Hr tl (refl ? h) ? Hlookup Hfold) 350  #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP)  @(HXY (proj2 ? ?HP)) ] 351 ] 352  normalize in H; normalize 353 @(fold_eq … True) 354 [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l)) 355 [ #z #t' #X #HX @(proj2 ? ? HX) 356  @H ] 357  #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP)  @(HXY (proj2 ? ? HP)) ] 358  @(Hl tl (refl ? h) ? Hlookup) normalize 359 @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True)) 360 [ // 361  #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP)  @(HXY (proj2 ? ? HP)) ] 362  @H 363 ] 364 ] 365 ] 366  #n #b #_ #P #Hlookup #Hf normalize // ] 367 qed. 368 369 lemma forall_insert_inv2b: 370 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P:(BitVector n → A → Prop). 371 (∀x.(lookup_opt A n b t = Some A x) → P b x) → forall A n (insert A n b a t) P → forall A n t P. 372 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ? → ??%%% → ?) 373 [ #x #b #_ #P >(BitVector_O b) normalize #HP #Hf %1 [ @HP @refl  @(proj2 ? ? Hf) ] 374  #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd #P #HP #Hf 375 [ normalize in Hf; normalize 376 @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … Hf) 377 [ #Hfold @(Hr tl (refl ? h) ? HP Hfold) 378  #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP)  @(HXY (proj2 ? ? HP)) ] 379 ] 380  normalize in H; normalize 381 @(fold_eq … True) 382 [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l)) 383 [ #z #t' #X #HX @(proj2 ? ? HX) 384  @Hf ] 385  #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP)  @(HXY (proj2 ? ? HP)) ] 386  @(Hl tl (refl ? h) ? HP) normalize 387 @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True)) 388 [ // 389  #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP)  @(HXY (proj2 ? ? HP)) ] 390  @Hf 391 ] 392 ] 393 ] 394  #n #b #_ #P #Hlookup #Hf normalize // ] 395 qed. 396
Note: See TracChangeset
for help on using the changeset viewer.