[248] | 1 | include "BitVector.ma". |
---|
| 2 | include "Compare.ma". |
---|
| 3 | include "Bool.ma". |
---|
| 4 | include "Maybe.ma". |
---|
[246] | 5 | |
---|
| 6 | ninductive BitVectorTrie (A: Type[0]): Nat → Type[0] ≝ |
---|
| 7 | Leaf: A → BitVectorTrie A Z |
---|
| 8 | | Node: ∀n: Nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n) |
---|
| 9 | | Stub: ∀n: Nat. BitVectorTrie A n. |
---|
| 10 | |
---|
| 11 | notation "hvbox(t⌈h ↦ o⌉)" |
---|
| 12 | with precedence 45 |
---|
| 13 | for @{ match (? : $o=$h) with [ refl ⇒ $t ] }. |
---|
| 14 | |
---|
| 15 | notation "⊥" with precedence 90 |
---|
| 16 | for @{ match ? in False with [ ] }. |
---|
| 17 | |
---|
| 18 | nlet rec lookup (A: Type[0]) (n: Nat) |
---|
| 19 | (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b |
---|
| 20 | : A ≝ |
---|
| 21 | (match b return λx.λ_. x = n → A with |
---|
| 22 | [ Empty ⇒ |
---|
| 23 | (match t return λx.λ_. Z = x → A with |
---|
| 24 | [ Leaf l ⇒ λ_.l |
---|
| 25 | | Node h l r ⇒ λK.⊥ |
---|
| 26 | | Stub s ⇒ λ_.a |
---|
| 27 | ]) |
---|
| 28 | | Cons o hd tl ⇒ |
---|
| 29 | match t return λx.λ_. (S o) = x → A with |
---|
| 30 | [ Leaf l ⇒ λK.⊥ |
---|
| 31 | | Node h l r ⇒ |
---|
| 32 | match hd with |
---|
| 33 | [ True ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a |
---|
| 34 | | False ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a |
---|
| 35 | ] |
---|
| 36 | | Stub s ⇒ λ_. a |
---|
| 37 | ] |
---|
| 38 | ]) (refl ? n). |
---|
| 39 | ndestruct; //. |
---|
| 40 | nqed. |
---|
| 41 | |
---|
| 42 | nlet rec prepare_trie_for_insertion (A: Type[0]) (n: Nat) |
---|
| 43 | (b: BitVector n) (a:A) on b |
---|
| 44 | : BitVectorTrie A n ≝ |
---|
| 45 | match b with |
---|
| 46 | [ Empty ⇒ Leaf A a |
---|
| 47 | | Cons o hd tl ⇒ |
---|
| 48 | match hd with |
---|
| 49 | [ True ⇒ Node A o (Stub A o) (prepare_trie_for_insertion A o tl a) |
---|
| 50 | | False ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o) |
---|
| 51 | ] |
---|
| 52 | ]. |
---|
| 53 | |
---|
| 54 | nlet rec insert (A: Type[0]) (n: Nat) |
---|
| 55 | (b: BitVector n) (a: A) on b: |
---|
| 56 | BitVectorTrie A n → BitVectorTrie A n ≝ |
---|
| 57 | (match b with |
---|
| 58 | [ Empty ⇒ λ_. Leaf A a |
---|
| 59 | | Cons o hd tl ⇒ λt. |
---|
| 60 | match t return λy.λ_. S o = y → BitVectorTrie A (S o) with |
---|
| 61 | [ Leaf l ⇒ λprf.⊥ |
---|
| 62 | | Node p l r ⇒ λprf. |
---|
| 63 | match hd with |
---|
| 64 | [ True ⇒ Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉)) |
---|
| 65 | | False ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉) |
---|
| 66 | ] |
---|
| 67 | | Stub p ⇒ λprf. ? (prepare_trie_for_insertion A ? b a) |
---|
| 68 | ] (refl ? (S o)) |
---|
| 69 | ]). |
---|
| 70 | ##[ ndestruct; |
---|
| 71 | ##| ndestruct; @; |
---|
| 72 | ##| ndestruct; @; |
---|
| 73 | ##| ndestruct; @; |
---|
| 74 | ##| ndestruct; @; |
---|
| 75 | ##| #H; nassumption; |
---|
| 76 | ##] |
---|
| 77 | nqed. |
---|
| 78 | |
---|
| 79 | nlemma insert_lookup_stub: |
---|
| 80 | ∀A: Type[0]. |
---|
| 81 | ∀n: Nat. |
---|
| 82 | ∀b: BitVector n. |
---|
| 83 | ∀t: BitVectorTrie A n. |
---|
| 84 | ∀a, c: A. |
---|
| 85 | (lookup A n b (insert A n b a (Stub A n)) a) = a. |
---|
| 86 | #A n b t a c. |
---|
| 87 | nelim b. |
---|
| 88 | //. |
---|
| 89 | #N H V H2. |
---|
| 90 | nnormalize. |
---|
| 91 | @. |
---|
| 92 | nqed. |
---|
| 93 | |
---|
| 94 | (* |
---|
| 95 | nlemma test: |
---|
| 96 | ∀n: Nat. |
---|
| 97 | ∀b: BitVector n. |
---|
| 98 | length n b = n. |
---|
| 99 | #n b. |
---|
| 100 | nelim b. |
---|
| 101 | //. |
---|
| 102 | #N H V IH. |
---|
| 103 | ncases H. |
---|
| 104 | |
---|
| 105 | nlemma insert_lookup_leaf: |
---|
| 106 | ∀A: Type[0]. |
---|
| 107 | ∀n: Nat. |
---|
| 108 | ∀b: BitVector n. |
---|
| 109 | ∀a, c: A. |
---|
| 110 | ∀t: BitVectorTrie A n. |
---|
| 111 | lookup A ? b (insert A ? b a t) c = a. |
---|
| 112 | #A n b a c t. |
---|
| 113 | nelim b. |
---|
| 114 | nnormalize. |
---|
| 115 | @. |
---|
[248] | 116 | #N H V IH. |
---|
| 117 | *) |
---|