Ignore:
Timestamp:
Oct 17, 2011, 3:50:50 PM (8 years ago)
Author:
boender
Message:
  • added invariant for policy trie to assembly
  • change (syntax only) to status in order to make it compile
  • added lemma + renaming to bitvectortrie
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1316 r1393  
    338338qed.   
    339339
    340 lemma lookup_opt_lookup:
     340lemma lookup_opt_lookup_miss:
     341  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
     342  lookup_opt A n b t = None A → ∀x.lookup A n b t x = x.
     343 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)
     344 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct
     345 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb
     346   >Hb >Hb in H; cases hd
     347   [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup
     348   | normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup
     349   ]
     350 | #n #B #_ #H #x @lookup_stub
     351 ]
     352qed.
     353
     354lemma lookup_opt_lookup_hit:
    341355  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
    342356  lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a.
    343357 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)
    344358 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl
    345  | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X; -X; #tl #Hb
     359 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb
    346360   >Hb >Hb in H; cases hd
    347361   [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup
     
    352366qed.
    353367
    354 lemma lookup_lookup_opt:
     368lemma lookup_lookup_opt_hit:
    355369  ∀A.∀n.∀b.∀t.∀x,a.
    356370  lookup A n b t x = a → x ≠ a → lookup_opt A n b t = Some A a.
     
    368382qed.
    369383
    370  
    371  
    372384lemma lookup_opt_prepare_trie_for_insertion_hit:
    373385 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.
     
    453465   ]
    454466 | #n #b #_ #P #Hlookup #Hf normalize // ]
    455 qed. 
     467qed.
    456468
    457469lemma forall_insert_inv2b:
     
    523535   ]
    524536 ]
    525 qed.   
     537qed.
    526538
    527539lemma update_fail : ∀A,n,b,a,t.
Note: See TracChangeset for help on using the changeset viewer.