Ignore:
Timestamp:
Jun 23, 2011, 5:40:43 PM (8 years ago)
Author:
boender
Message:
  • some more BVT improvements
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1034 r1038  
    393393   ]
    394394 | #n #b #_ #P #Hlookup #Hf normalize // ]
    395 qed.
    396    
     395qed.
     396
     397lemma 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 ]
     405qed.
     406
     407lemma 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 ]
     437qed.   
Note: See TracChangeset for help on using the changeset viewer.