1 | include "BitVector.ma". |
---|
2 | include "Compare.ma". |
---|
3 | include "Bool.ma". |
---|
4 | include "Maybe.ma". |
---|
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 | @. |
---|
116 | #N H V IH. |
---|
117 | *) |
---|