Ignore:
Timestamp:
Jun 16, 2011, 4:50:23 PM (9 years ago)
Author:
sacerdot
Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r782 r985  
    128128  ]
    129129qed.
     130
     131lemma BitVectorTrie_O:
     132 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
     133 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
     134  [ #w #_ %1 %[@w] %
     135  | #n #l #r #abs @⊥ //
     136  | #n #EQ %2 >EQ %]
     137qed.
     138
     139lemma BitVectorTrie_Sn:
     140 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
     141 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
     142  [ #m #abs @⊥ //
     143  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
     144  | #m #EQ %2 // ]
     145qed.
     146
     147lemma lookup_prepare_trie_for_insertion_hit:
     148 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
     149  lookup … b (prepare_trie_for_insertion … b v) a = v.
     150 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
     151qed.
     152 
     153lemma lookup_insert_hit:
     154 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
     155  lookup … b (insert … b v t) a = v.
     156 #A #a #v #n #b elim b -b -n //
     157 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
     158  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
     159  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
     160qed.
     161
     162lemma lookup_prepare_trie_for_insertion_miss:
     163 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
     164  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
     165 #A #a #v #n #c elim c
     166  [ #b >(BitVector_O … b) normalize #abs @⊥ //
     167  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     168    cases hd cases hd' normalize
     169    [2,3: #_ cases tl' //
     170    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
     171qed.
     172 
     173lemma lookup_insert_miss:
     174 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     175  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
     176 #A #a #v #n #c elim c -c -n
     177  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     178  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     179    #t cases(BitVectorTrie_Sn … t)
     180    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     181     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     182    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     183     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     184     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
     185qed.
Note: See TracChangeset for help on using the changeset viewer.