 Timestamp:
 Jun 23, 2011, 5:40:43 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1034 r1038 393 393 ] 394 394  #n #b #_ #P #Hlookup #Hf normalize // ] 395 qed. 396 395 qed. 396 397 lemma forall_prepare_tree_for_insertion: 398 ∀A:Type[0].∀h:nat.∀b:BitVector h.∀a:A.∀P. 399 P b a → 400 forall A h (prepare_trie_for_insertion A h b a) P. 401 #A #h #b elim b 402 [ #a #P #HP normalize %1 [ @HP  // ] 403  #h #x #tl #Ha #a #P cases x #HP normalize @Ha @HP 404 ] 405 qed. 406 407 lemma forall_insert: 408 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P. 409 forall A n t P → P b a → forall A n (insert A n b a t) P. 410 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%) 411 [ #x #b #_ #P >(BitVector_O b) normalize #H1 #H2 /2/ 412  #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd #P #Hf #HP 413 [ normalize in Hf; normalize 414 @(fold_eq A … (fold A … (λx.λa0.λacc.P (true:::x) a0∧acc) r True) … Hf) 415 [ #Hp @(Hr tl (refl ? h) ? Hp HP) 416  #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP)  @(HXY (proj2 ? ? HP)) ] 417 ] 418  normalize in Hf; normalize 419 @(fold_eq … True) 420 [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0∧acc) l) 421 [ #z #t' #X #HX @(proj2 ? ? HX) 422  @Hf ] 423  #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP)  @(HXY (proj2 ? ? HP)) ] 424  @(Hl tl (refl ? h) ? ? HP) 425 normalize @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True)) 426 [ // 427  #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP)  @(HXY (proj2 ? ? HP)) ] 428  @Hf 429 ] 430 ] 431 ] 432  #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%) 433 [ #b #P #Hf #HP normalize %1 [ @HP  // ] 434  #h #hd #tl #H #b #P #Hf cases hd #HP normalize @(forall_prepare_tree_for_insertion A h tl a ? HP) 435 ] 436 ] 437 qed.
Note: See TracChangeset
for help on using the changeset viewer.