Changeset 869


Ignore:
Timestamp:
May 31, 2011, 5:28:21 PM (8 years ago)
Author:
sacerdot
Message:

More progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r868 r869  
    544544   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
    545545    → False.
     546
     547lemma BitVectorTrie_O:
     548 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
     549 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
     550  [ #w #_ %1 %[@w] %
     551  | #n #l #r #abs @⊥ //
     552  | #n #EQ %2 >EQ %]
     553qed.
     554
     555lemma BitVectorTrie_Sn:
     556 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
     557 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
     558  [ #m #abs @⊥ //
     559  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
     560  | #m #EQ %2 // ]
     561qed.
     562
     563lemma lookup_prepare_trie_for_insertion_hit:
     564 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
     565  lookup … b (prepare_trie_for_insertion … b v) a = v.
     566 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
     567qed.
     568 
     569lemma lookup_insert_hit:
     570 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
     571  lookup … b (insert … b v t) a = v.
     572 #A #a #v #n #b elim b -b -n //
     573 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
     574  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
     575  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
     576qed.
     577
     578lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
     579 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     580 #n #hd #tl #abs @⊥ //
     581qed.
     582
     583lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
     584 ∃hd.∃tl.v ≃ VCons bool n hd tl.
     585 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     586 [ #abs @⊥ //
     587 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     588qed.
     589
     590lemma lookup_insert_miss:
     591 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     592  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
     593 #A #a #v #n #c elim c -c -n
     594  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     595  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     596    #t cases(BitVectorTrie_Sn … t)
     597    [ * #l * #r #JMEQ >JMEQ cases hd #H CSC
     598     normalize in H;
     599     
     600      normalize //
     601    | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
     602qed.
    546603
    547604definition build_maps' ≝
Note: See TracChangeset for help on using the changeset viewer.